Transport integration by parts on the actual lifted cylinder. Compactly supported smooth energy fields are tested against the concrete weak-divergence condition; boundary terms are eliminated by that proved weak formulation.

def EulerMetricTransport.localFieldLift (period : ℝ) {W : Type u_1} (f : EulerLiftedGradientSpace.LiftDomain period → W) (x : EulerLiftedGradientSpace.LiftDomain period) : EulerLiftedGradientSpace.LiftTangent → W

A field pulled back to real covering coordinates centered at a cylinder point.

Equations

• EulerMetricTransport.localFieldLift period f x h = f (x.1 + h.1, x.2 + ↑h.2)

theorem EulerMetricTransport.localFieldLift_cover (period : ℝ) {W : Type u_1} (f : EulerLiftedGradientSpace.LiftDomain period → W) (z : EulerLiftedGradientSpace.LiftTangent) : localFieldLift period f (EulerLiftedGradientSpace.coveringMap period z) = fun (h : EulerLiftedGradientSpace.LiftTangent) => localFieldLift period f 0 (z + h)

theorem EulerMetricTransport.fderiv_localFieldLift_cover (period : ℝ) {W : Type u_1} [NormedAddCommGroup W] [NormedSpace ℝ W] (f : EulerLiftedGradientSpace.LiftDomain period → W) (z : EulerLiftedGradientSpace.LiftTangent) : fderiv ℝ (localFieldLift period f (EulerLiftedGradientSpace.coveringMap period z)) 0 = fderiv ℝ (localFieldLift period f 0) z

theorem EulerMetricTransport.smoothField_continuous (period : ℝ) {W : Type u_1} [NormedAddCommGroup W] [NormedSpace ℝ W] (f : EulerLiftedGradientSpace.LiftDomain period → W) (hf : ∀ (x : EulerLiftedGradientSpace.LiftDomain period), ContDiff ℝ (↑⊤) (localFieldLift period f x)) : Continuous f

theorem EulerMetricTransport.localFDeriv_continuous (period : ℝ) {W : Type u_1} [NormedAddCommGroup W] [NormedSpace ℝ W] (f : EulerLiftedGradientSpace.LiftDomain period → W) (hf : ∀ (x : EulerLiftedGradientSpace.LiftDomain period), ContDiff ℝ (↑⊤) (localFieldLift period f x)) : Continuous fun (x : EulerLiftedGradientSpace.LiftDomain period) => fderiv ℝ (localFieldLift period f x) 0

noncomputable def EulerMetricTransport.coordinateDirection (κ : ℝ) (m : EulerLiftedGradientSpace.Vector3) (i : Fin 3) : EulerLiftedGradientSpace.LiftTangent

The covering-space direction corresponding to one lifted gradient component.

Equations

• EulerMetricTransport.coordinateDirection κ m i = (κ • EuclideanSpace.single i 1, m.ofLp i)

noncomputable def EulerMetricTransport.transportDirection (κ : ℝ) (m v : EulerLiftedGradientSpace.Vector3) : EulerLiftedGradientSpace.LiftTangent

The actual four dimensional transport vector associated with a lifted velocity.

Equations

• EulerMetricTransport.transportDirection κ m v = (κ • v, inner ℝ m v)

noncomputable def EulerMetricTransport.vectorOfLinear (κ : ℝ) (m : EulerLiftedGradientSpace.Vector3) (L : EulerLiftedGradientSpace.LiftTangent →L[ℝ] ℝ) : EulerLiftedGradientSpace.Vector3

The vector of a scalar differential evaluated on the lifted coordinate directions.

Equations

• EulerMetricTransport.vectorOfLinear κ m L = WithLp.toLp 2 fun (i : Fin 3) => L (EulerMetricTransport.coordinateDirection κ m i)

theorem EulerMetricTransport.coordinateDirections_sum (κ : ℝ) (m v : EulerLiftedGradientSpace.Vector3) : ∑ i : Fin 3, v.ofLp i • coordinateDirection κ m i = transportDirection κ m v

theorem EulerMetricTransport.vectorOfLinear_inner (κ : ℝ) (m v : EulerLiftedGradientSpace.Vector3) (L : EulerLiftedGradientSpace.LiftTangent →L[ℝ] ℝ) : inner ℝ (vectorOfLinear κ m L) v = L (transportDirection κ m v)

theorem EulerMetricTransport.liftedGradient_eq_vectorOfLinear (period κ : ℝ) (m : EulerLiftedGradientSpace.Vector3) (φ : EulerLiftedGradientSpace.LiftDomain period → ℝ) (x : EulerLiftedGradientSpace.LiftDomain period) : EulerLiftedGradientSpace.liftedGradient period κ m φ x = vectorOfLinear κ m (fderiv ℝ (EulerLiftedGradientSpace.localLift period φ x) 0)

noncomputable def EulerMetricTransport.metricEnergy (period : ℝ) (K : EulerLiftedGradientSpace.LiftDomain period → EulerLiftedGradientSpace.Vector3 →L[ℝ] EulerLiftedGradientSpace.Vector3) (e : EulerLiftedGradientSpace.LiftDomain period → EulerLiftedGradientSpace.Vector3) (x : EulerLiftedGradientSpace.LiftDomain period) : ℝ

The pointwise quadratic metric energy of a vector field.

Equations

• EulerMetricTransport.metricEnergy period K e x = 1 / 2 * inner ℝ ((K x) (e x)) (e x)

theorem EulerMetricTransport.metricEnergy_compact (period : ℝ) (K : EulerLiftedGradientSpace.LiftDomain period → EulerLiftedGradientSpace.Vector3 →L[ℝ] EulerLiftedGradientSpace.Vector3) (e : EulerLiftedGradientSpace.LiftDomain period → EulerLiftedGradientSpace.Vector3) (he : HasCompactSupport e) : HasCompactSupport (metricEnergy period K e)

theorem EulerMetricTransport.metricEnergy_smooth (period : ℝ) (K : EulerLiftedGradientSpace.LiftDomain period → EulerLiftedGradientSpace.Vector3 →L[ℝ] EulerLiftedGradientSpace.Vector3) (e : EulerLiftedGradientSpace.LiftDomain period → EulerLiftedGradientSpace.Vector3) (hK : ∀ (x : EulerLiftedGradientSpace.LiftDomain period), ContDiff ℝ (↑⊤) (localFieldLift period K x)) (he : ∀ (x : EulerLiftedGradientSpace.LiftDomain period), ContDiff ℝ (↑⊤) (localFieldLift period e x)) (x : EulerLiftedGradientSpace.LiftDomain period) : ContDiff ℝ (↑⊤) (EulerLiftedGradientSpace.localLift period (metricEnergy period K e) x)

theorem EulerMetricTransport.metricEnergy_fderiv (period : ℝ) (K : EulerLiftedGradientSpace.LiftDomain period → EulerLiftedGradientSpace.Vector3 →L[ℝ] EulerLiftedGradientSpace.Vector3) (e : EulerLiftedGradientSpace.LiftDomain period → EulerLiftedGradientSpace.Vector3) (hK : ∀ (x : EulerLiftedGradientSpace.LiftDomain period), ContDiff ℝ (↑⊤) (localFieldLift period K x)) (he : ∀ (x : EulerLiftedGradientSpace.LiftDomain period), ContDiff ℝ (↑⊤) (localFieldLift period e x)) (hsym : ∀ (x : EulerLiftedGradientSpace.LiftDomain period) (v w : EulerLiftedGradientSpace.Vector3), inner ℝ ((K x) v) w = inner ℝ v ((K x) w)) (x : EulerLiftedGradientSpace.LiftDomain period) (v : EulerLiftedGradientSpace.LiftTangent) : (fderiv ℝ (EulerLiftedGradientSpace.localLift period (metricEnergy period K e) x) 0) v = inner ℝ ((K x) (e x)) ((fderiv ℝ (localFieldLift period e x) 0) v) + 1 / 2 * inner ℝ (((fderiv ℝ (localFieldLift period K x) 0) v) (e x)) (e x)

theorem EulerMetricTransport.metricEnergy_gradient_transport (period κ : ℝ) (m : EulerLiftedGradientSpace.Vector3) (K : EulerLiftedGradientSpace.LiftDomain period → EulerLiftedGradientSpace.Vector3 →L[ℝ] EulerLiftedGradientSpace.Vector3) (e : EulerLiftedGradientSpace.LiftDomain period → EulerLiftedGradientSpace.Vector3) (hK : ∀ (x : EulerLiftedGradientSpace.LiftDomain period), ContDiff ℝ (↑⊤) (localFieldLift period K x)) (he : ∀ (x : EulerLiftedGradientSpace.LiftDomain period), ContDiff ℝ (↑⊤) (localFieldLift period e x)) (hsym : ∀ (x : EulerLiftedGradientSpace.LiftDomain period) (v w : EulerLiftedGradientSpace.Vector3), inner ℝ ((K x) v) w = inner ℝ v ((K x) w)) (x : EulerLiftedGradientSpace.LiftDomain period) (z : EulerLiftedGradientSpace.Vector3) : inner ℝ (EulerLiftedGradientSpace.liftedGradient period κ m (metricEnergy period K e) x) z = inner ℝ ((K x) (e x)) ((fderiv ℝ (localFieldLift period e x) 0) (transportDirection κ m z)) + 1 / 2 * inner ℝ (((fderiv ℝ (localFieldLift period K x) 0) (transportDirection κ m z)) (e x)) (e x)

theorem EulerMetricTransport.metric_transport_zero (period : ℝ) [Fact (0 < period)] (κ : ℝ) (m : EulerLiftedGradientSpace.Vector3) (K : EulerLiftedGradientSpace.LiftDomain period → EulerLiftedGradientSpace.Vector3 →L[ℝ] EulerLiftedGradientSpace.Vector3) (e : EulerLiftedGradientSpace.LiftDomain period → EulerLiftedGradientSpace.Vector3) (hec : HasCompactSupport e) (hK : ∀ (x : EulerLiftedGradientSpace.LiftDomain period), ContDiff ℝ (↑⊤) (localFieldLift period K x)) (he : ∀ (x : EulerLiftedGradientSpace.LiftDomain period), ContDiff ℝ (↑⊤) (localFieldLift period e x)) (hsym : ∀ (x : EulerLiftedGradientSpace.LiftDomain period) (v w : EulerLiftedGradientSpace.Vector3), inner ℝ ((K x) v) w = inner ℝ v ((K x) w)) {z : ↥(EulerLiftedGradientSpace.LiftL2 period)} (hz : z ∈ EulerLiftedGradientSpace.divergenceFreeSpace period κ m) : ∫ (x : EulerLiftedGradientSpace.LiftDomain period), inner ℝ ((K x) (e x)) ((fderiv ℝ (localFieldLift period e x) 0) (transportDirection κ m (↑↑z x))) + 1 / 2 * inner ℝ (((fderiv ℝ (localFieldLift period K x) 0) (transportDirection κ m (↑↑z x))) (e x)) (e x) ∂EulerLiftedGradientSpace.liftMeasure period = 0

noncomputable def EulerMetricTransport.transportFlux (period κ : ℝ) (m : EulerLiftedGradientSpace.Vector3) (K : EulerLiftedGradientSpace.LiftDomain period → EulerLiftedGradientSpace.Vector3 →L[ℝ] EulerLiftedGradientSpace.Vector3) (e : EulerLiftedGradientSpace.LiftDomain period → EulerLiftedGradientSpace.Vector3) (x : EulerLiftedGradientSpace.LiftDomain period) : EulerLiftedGradientSpace.Vector3

The compact vector coefficient whose pairing with velocity is the metric transport term.

Equations

• EulerMetricTransport.transportFlux period κ m K e x = EulerMetricTransport.vectorOfLinear κ m ((innerSL ℝ) ((K x) (e x)) ∘SL fderiv ℝ (EulerMetricTransport.localFieldLift period e x) 0)

theorem EulerMetricTransport.transportFlux_inner (period κ : ℝ) (m : EulerLiftedGradientSpace.Vector3) (K : EulerLiftedGradientSpace.LiftDomain period → EulerLiftedGradientSpace.Vector3 →L[ℝ] EulerLiftedGradientSpace.Vector3) (e : EulerLiftedGradientSpace.LiftDomain period → EulerLiftedGradientSpace.Vector3) (x : EulerLiftedGradientSpace.LiftDomain period) (z : EulerLiftedGradientSpace.Vector3) : inner ℝ (transportFlux period κ m K e x) z = inner ℝ ((K x) (e x)) ((fderiv ℝ (localFieldLift period e x) 0) (transportDirection κ m z))

theorem EulerMetricTransport.transportFlux_continuous (period κ : ℝ) (m : EulerLiftedGradientSpace.Vector3) (K : EulerLiftedGradientSpace.LiftDomain period → EulerLiftedGradientSpace.Vector3 →L[ℝ] EulerLiftedGradientSpace.Vector3) (e : EulerLiftedGradientSpace.LiftDomain period → EulerLiftedGradientSpace.Vector3) (hK : ∀ (x : EulerLiftedGradientSpace.LiftDomain period), ContDiff ℝ (↑⊤) (localFieldLift period K x)) (he : ∀ (x : EulerLiftedGradientSpace.LiftDomain period), ContDiff ℝ (↑⊤) (localFieldLift period e x)) : Continuous (transportFlux period κ m K e)

theorem EulerMetricTransport.transportFlux_compact (period κ : ℝ) (m : EulerLiftedGradientSpace.Vector3) (K : EulerLiftedGradientSpace.LiftDomain period → EulerLiftedGradientSpace.Vector3 →L[ℝ] EulerLiftedGradientSpace.Vector3) (e : EulerLiftedGradientSpace.LiftDomain period → EulerLiftedGradientSpace.Vector3) (he : HasCompactSupport e) : HasCompactSupport (transportFlux period κ m K e)

theorem EulerMetricTransport.compact_pairing_integrable (period : ℝ) [Fact (0 < period)] (f : EulerLiftedGradientSpace.LiftDomain period → EulerLiftedGradientSpace.Vector3) (hf : Continuous f) (hfc : HasCompactSupport f) (z : ↥(EulerLiftedGradientSpace.LiftL2 period)) : MeasureTheory.Integrable (fun (x : EulerLiftedGradientSpace.LiftDomain period) => inner ℝ (f x) (↑↑z x)) (EulerLiftedGradientSpace.liftMeasure period)

theorem EulerMetricTransport.metric_transport_integrable (period : ℝ) [Fact (0 < period)] (κ : ℝ) (m : EulerLiftedGradientSpace.Vector3) (K : EulerLiftedGradientSpace.LiftDomain period → EulerLiftedGradientSpace.Vector3 →L[ℝ] EulerLiftedGradientSpace.Vector3) (e : EulerLiftedGradientSpace.LiftDomain period → EulerLiftedGradientSpace.Vector3) (hec : HasCompactSupport e) (hK : ∀ (x : EulerLiftedGradientSpace.LiftDomain period), ContDiff ℝ (↑⊤) (localFieldLift period K x)) (he : ∀ (x : EulerLiftedGradientSpace.LiftDomain period), ContDiff ℝ (↑⊤) (localFieldLift period e x)) (z : ↥(EulerLiftedGradientSpace.LiftL2 period)) : MeasureTheory.Integrable (fun (x : EulerLiftedGradientSpace.LiftDomain period) => inner ℝ ((K x) (e x)) ((fderiv ℝ (localFieldLift period e x) 0) (transportDirection κ m (↑↑z x)))) (EulerLiftedGradientSpace.liftMeasure period)

theorem EulerMetricTransport.metric_transport_by_parts (period : ℝ) [Fact (0 < period)] (κ : ℝ) (m : EulerLiftedGradientSpace.Vector3) (K : EulerLiftedGradientSpace.LiftDomain period → EulerLiftedGradientSpace.Vector3 →L[ℝ] EulerLiftedGradientSpace.Vector3) (e : EulerLiftedGradientSpace.LiftDomain period → EulerLiftedGradientSpace.Vector3) (hec : HasCompactSupport e) (hK : ∀ (x : EulerLiftedGradientSpace.LiftDomain period), ContDiff ℝ (↑⊤) (localFieldLift period K x)) (he : ∀ (x : EulerLiftedGradientSpace.LiftDomain period), ContDiff ℝ (↑⊤) (localFieldLift period e x)) (hsym : ∀ (x : EulerLiftedGradientSpace.LiftDomain period) (v w : EulerLiftedGradientSpace.Vector3), inner ℝ ((K x) v) w = inner ℝ v ((K x) w)) {z : ↥(EulerLiftedGradientSpace.LiftL2 period)} (hz : z ∈ EulerLiftedGradientSpace.divergenceFreeSpace period κ m) : ∫ (x : EulerLiftedGradientSpace.LiftDomain period), inner ℝ ((K x) (e x)) ((fderiv ℝ (localFieldLift period e x) 0) (transportDirection κ m (↑↑z x))) ∂EulerLiftedGradientSpace.liftMeasure period = -∫ (x : EulerLiftedGradientSpace.LiftDomain period), 1 / 2 * inner ℝ (((fderiv ℝ (localFieldLift period K x) 0) (transportDirection κ m (↑↑z x))) (e x)) (e x) ∂EulerLiftedGradientSpace.liftMeasure period

theorem EulerMetricTransport.transportDirection_norm_le (κ : ℝ) (m v : EulerLiftedGradientSpace.Vector3) : ‖transportDirection κ m v‖ ≤ (|κ| + ‖m‖) * ‖v‖

theorem EulerMetricTransport.metric_transport_bound (period : ℝ) [Fact (0 < period)] (κ : ℝ) (m : EulerLiftedGradientSpace.Vector3) (K : EulerLiftedGradientSpace.LiftDomain period → EulerLiftedGradientSpace.Vector3 →L[ℝ] EulerLiftedGradientSpace.Vector3) (e : EulerLiftedGradientSpace.LiftDomain period → EulerLiftedGradientSpace.Vector3) (hec : HasCompactSupport e) (hK : ∀ (x : EulerLiftedGradientSpace.LiftDomain period), ContDiff ℝ (↑⊤) (localFieldLift period K x)) (he : ∀ (x : EulerLiftedGradientSpace.LiftDomain period), ContDiff ℝ (↑⊤) (localFieldLift period e x)) (hsym : ∀ (x : EulerLiftedGradientSpace.LiftDomain period) (v w : EulerLiftedGradientSpace.Vector3), inner ℝ ((K x) v) w = inner ℝ v ((K x) w)) {z : ↥(EulerLiftedGradientSpace.LiftL2 period)} (hz : z ∈ EulerLiftedGradientSpace.divergenceFreeSpace period κ m) (C B : NNReal) (hDK : ∀ (x : EulerLiftedGradientSpace.LiftDomain period), ‖fderiv ℝ (localFieldLift period K x) 0‖ ≤ ↑C) (hb : ∀ᵐ (x : EulerLiftedGradientSpace.LiftDomain period) ∂EulerLiftedGradientSpace.liftMeasure period, ‖transportDirection κ m (↑↑z x)‖ ≤ ↑B) : |∫ (x : EulerLiftedGradientSpace.LiftDomain period), inner ℝ ((K x) (e x)) ((fderiv ℝ (localFieldLift period e x) 0) (transportDirection κ m (↑↑z x))) ∂EulerLiftedGradientSpace.liftMeasure period| ≤ 1 / 2 * ↑C * ↑B * ∫ (x : EulerLiftedGradientSpace.LiftDomain period), ‖e x‖ ^ 2 ∂EulerLiftedGradientSpace.liftMeasure period

theorem EulerMetricTransport.metric_transport_L2_bound (period : ℝ) [Fact (0 < period)] (κ : ℝ) (m : EulerLiftedGradientSpace.Vector3) (K : EulerLiftedGradientSpace.LiftDomain period → EulerLiftedGradientSpace.Vector3 →L[ℝ] EulerLiftedGradientSpace.Vector3) (e : ↥(EulerLiftedGradientSpace.LiftL2 period)) (hec : HasCompactSupport fun (x : EulerLiftedGradientSpace.LiftDomain period) => ↑↑e x) (hK : ∀ (x : EulerLiftedGradientSpace.LiftDomain period), ContDiff ℝ (↑⊤) (localFieldLift period K x)) (he : ∀ (x : EulerLiftedGradientSpace.LiftDomain period), ContDiff ℝ (↑⊤) (localFieldLift period (fun (y : EulerLiftedGradientSpace.LiftDomain period) => ↑↑e y) x)) (hsym : ∀ (x : EulerLiftedGradientSpace.LiftDomain period) (v w : EulerLiftedGradientSpace.Vector3), inner ℝ ((K x) v) w = inner ℝ v ((K x) w)) {z : ↥(EulerLiftedGradientSpace.LiftL2 period)} (hz : z ∈ EulerLiftedGradientSpace.divergenceFreeSpace period κ m) (C B : NNReal) (hDK : ∀ (x : EulerLiftedGradientSpace.LiftDomain period), ‖fderiv ℝ (localFieldLift period K x) 0‖ ≤ ↑C) (hb : ∀ᵐ (x : EulerLiftedGradientSpace.LiftDomain period) ∂EulerLiftedGradientSpace.liftMeasure period, ‖transportDirection κ m (↑↑z x)‖ ≤ ↑B) : |∫ (x : EulerLiftedGradientSpace.LiftDomain period), inner ℝ ((K x) (↑↑e x)) ((fderiv ℝ (localFieldLift period (fun (y : EulerLiftedGradientSpace.LiftDomain period) => ↑↑e y) x) 0) (transportDirection κ m (↑↑z x))) ∂EulerLiftedGradientSpace.liftMeasure period| ≤ 1 / 2 * ↑C * ↑B * ‖e‖ ^ 2