Metric-energy evolution using a separate actual smooth representative of each L² class.

theorem EulerRepresentativeMetricEvolution.liftedTransport_memLp (period : ℝ) [Fact (0 < period)] (κ : ℝ) (m : EulerLiftedGradientSpace.Vector3) (g : EulerLiftedGradientSpace.LiftDomain period → EulerLiftedGradientSpace.Vector3) (z : ↥(EulerLiftedGradientSpace.LiftL2 period)) (hDe : MeasureTheory.MemLp (fun (x : EulerLiftedGradientSpace.LiftDomain period) => fderiv ℝ (EulerMetricTransport.localFieldLift period g x) 0) 2 (EulerLiftedGradientSpace.liftMeasure period)) (B : NNReal) (hzB : ∀ᵐ (x : EulerLiftedGradientSpace.LiftDomain period) ∂EulerLiftedGradientSpace.liftMeasure period, ‖↑↑z x‖ ≤ ↑B) : MeasureTheory.MemLp (fun (x : EulerLiftedGradientSpace.LiftDomain period) => (fderiv ℝ (EulerMetricTransport.localFieldLift period g x) 0) (EulerMetricTransport.transportDirection κ m (↑↑z x))) 2 (EulerLiftedGradientSpace.liftMeasure period)

The actual directional transport derivative is square integrable under H¹ and bounded velocity.

noncomputable def EulerRepresentativeMetricEvolution.liftedTransport (period : ℝ) [Fact (0 < period)] (κ : ℝ) (m : EulerLiftedGradientSpace.Vector3) (g : EulerLiftedGradientSpace.LiftDomain period → EulerLiftedGradientSpace.Vector3) (z : ↥(EulerLiftedGradientSpace.LiftL2 period)) (hDe : MeasureTheory.MemLp (fun (x : EulerLiftedGradientSpace.LiftDomain period) => fderiv ℝ (EulerMetricTransport.localFieldLift period g x) 0) 2 (EulerLiftedGradientSpace.liftMeasure period)) (B : NNReal) (hzB : ∀ᵐ (x : EulerLiftedGradientSpace.LiftDomain period) ∂EulerLiftedGradientSpace.liftMeasure period, ‖↑↑z x‖ ≤ ↑B) : ↥(EulerLiftedGradientSpace.LiftL2 period)

The genuine L² element represented by the lifted directional transport derivative.

Equations

• One or more equations did not get rendered due to their size.

theorem EulerRepresentativeMetricEvolution.liftedTransport_ae (period : ℝ) [Fact (0 < period)] (κ : ℝ) (m : EulerLiftedGradientSpace.Vector3) (g : EulerLiftedGradientSpace.LiftDomain period → EulerLiftedGradientSpace.Vector3) (z : ↥(EulerLiftedGradientSpace.LiftL2 period)) (hDe : MeasureTheory.MemLp (fun (x : EulerLiftedGradientSpace.LiftDomain period) => fderiv ℝ (EulerMetricTransport.localFieldLift period g x) 0) 2 (EulerLiftedGradientSpace.liftMeasure period)) (B : NNReal) (hzB : ∀ᵐ (x : EulerLiftedGradientSpace.LiftDomain period) ∂EulerLiftedGradientSpace.liftMeasure period, ‖↑↑z x‖ ≤ ↑B) : ↑↑(liftedTransport period κ m g z hDe B hzB) =ᵐ[EulerLiftedGradientSpace.liftMeasure period] fun (x : EulerLiftedGradientSpace.LiftDomain period) => (fderiv ℝ (EulerMetricTransport.localFieldLift period g x) 0) (EulerMetricTransport.transportDirection κ m (↑↑z x))

theorem EulerRepresentativeMetricEvolution.metric_transport_inner_eq (period : ℝ) [Fact (0 < period)] (κ : ℝ) (m : EulerLiftedGradientSpace.Vector3) (K : EulerLiftedGradientSpace.LiftDomain period → EulerLiftedGradientSpace.Vector3 →L[ℝ] EulerLiftedGradientSpace.Vector3) (hKm : MeasureTheory.AEStronglyMeasurable K (EulerLiftedGradientSpace.liftMeasure period)) (C : NNReal) (hC : ∀ (x : EulerLiftedGradientSpace.LiftDomain period), ‖K x‖ ≤ ↑C) (e : ↥(EulerLiftedGradientSpace.LiftL2 period)) (g : EulerLiftedGradientSpace.LiftDomain period → EulerLiftedGradientSpace.Vector3) (z : ↥(EulerLiftedGradientSpace.LiftL2 period)) (hrep : ↑↑e =ᵐ[EulerLiftedGradientSpace.liftMeasure period] g) (hDe : MeasureTheory.MemLp (fun (x : EulerLiftedGradientSpace.LiftDomain period) => fderiv ℝ (EulerMetricTransport.localFieldLift period g x) 0) 2 (EulerLiftedGradientSpace.liftMeasure period)) (B : NNReal) (hzB : ∀ᵐ (x : EulerLiftedGradientSpace.LiftDomain period) ∂EulerLiftedGradientSpace.liftMeasure period, ‖↑↑z x‖ ≤ ↑B) : inner ℝ ((EulerLiftedPressure.coefficientOperator K hKm C hC) e) (liftedTransport period κ m g z hDe B hzB) = ∫ (x : EulerLiftedGradientSpace.LiftDomain period), inner ℝ ((K x) (g x)) ((fderiv ℝ (EulerMetricTransport.localFieldLift period g x) 0) (EulerMetricTransport.transportDirection κ m (↑↑z x))) ∂EulerLiftedGradientSpace.liftMeasure period

The Hilbert metric pairing equals the actual spatial transport integral.

theorem EulerRepresentativeMetricEvolution.metric_transport_inner_bound (period : ℝ) [Fact (0 < period)] (κ : ℝ) (m : EulerLiftedGradientSpace.Vector3) (K : EulerLiftedGradientSpace.LiftDomain period → EulerLiftedGradientSpace.Vector3 →L[ℝ] EulerLiftedGradientSpace.Vector3) (hKm : MeasureTheory.AEStronglyMeasurable K (EulerLiftedGradientSpace.liftMeasure period)) (e : ↥(EulerLiftedGradientSpace.LiftL2 period)) (g : EulerLiftedGradientSpace.LiftDomain period → EulerLiftedGradientSpace.Vector3) (z : ↥(EulerLiftedGradientSpace.LiftL2 period)) (hrep : ↑↑e =ᵐ[EulerLiftedGradientSpace.liftMeasure period] g) (hK : ∀ (x : EulerLiftedGradientSpace.LiftDomain period), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift period K x)) (he : ∀ (x : EulerLiftedGradientSpace.LiftDomain period), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift period g x)) (hDe : MeasureTheory.MemLp (fun (x : EulerLiftedGradientSpace.LiftDomain period) => fderiv ℝ (EulerMetricTransport.localFieldLift period g x) 0) 2 (EulerLiftedGradientSpace.liftMeasure period)) (hsym : ∀ (x : EulerLiftedGradientSpace.LiftDomain period) (v w : EulerLiftedGradientSpace.Vector3), inner ℝ ((K x) v) w = inner ℝ v ((K x) w)) (hz : z ∈ EulerLiftedGradientSpace.divergenceFreeSpace period κ m) (C D B : NNReal) (hC : ∀ (x : EulerLiftedGradientSpace.LiftDomain period), ‖K x‖ ≤ ↑C) (hD : ∀ (x : EulerLiftedGradientSpace.LiftDomain period), ‖fderiv ℝ (EulerMetricTransport.localFieldLift period K x) 0‖ ≤ ↑D) (hzB : ∀ᵐ (x : EulerLiftedGradientSpace.LiftDomain period) ∂EulerLiftedGradientSpace.liftMeasure period, ‖↑↑z x‖ ≤ ↑B) : |inner ℝ ((EulerLiftedPressure.coefficientOperator K hKm C hC) e) (liftedTransport period κ m g z hDe B hzB)| ≤ 1 / 2 * ↑D * ((|κ| + ‖m‖) * ↑B) * ‖e‖ ^ 2

The transport bound required by the Hilbert energy theorem, with genuine spatial fields.

noncomputable def EulerRepresentativeMetricEvolution.metricFamily (period : ℝ) [Fact (0 < period)] (K : ℝ → EulerLiftedGradientSpace.LiftDomain period → EulerLiftedGradientSpace.Vector3 →L[ℝ] EulerLiftedGradientSpace.Vector3) (hKm : ∀ (t : ℝ), MeasureTheory.AEStronglyMeasurable (K t) (EulerLiftedGradientSpace.liftMeasure period)) (C : NNReal) (hC : ∀ (t : ℝ) (x : EulerLiftedGradientSpace.LiftDomain period), ‖K t x‖ ≤ ↑C) : ℝ → ↥(EulerLiftedGradientSpace.LiftL2 period) →L[ℝ] ↥(EulerLiftedGradientSpace.LiftL2 period)

A pointwise matrix family acting on the actual lifted L² space.

Equations

• EulerRepresentativeMetricEvolution.metricFamily period K hKm C hC t = EulerLiftedPressure.coefficientOperator (K t) ⋯ C ⋯

theorem EulerRepresentativeMetricEvolution.lifted_regularized_energy_evolution (period : ℝ) [Fact (0 < period)] (κ : ℝ) (m : EulerLiftedGradientSpace.Vector3) (K : ℝ → EulerLiftedGradientSpace.LiftDomain period → EulerLiftedGradientSpace.Vector3 →L[ℝ] EulerLiftedGradientSpace.Vector3) (hKm : ∀ (t : ℝ), MeasureTheory.AEStronglyMeasurable (K t) (EulerLiftedGradientSpace.liftMeasure period)) (C : NNReal) (hC : ∀ (t : ℝ) (x : EulerLiftedGradientSpace.LiftDomain period), ‖K t x‖ ≤ ↑C) (e : ℝ → ↥(EulerLiftedGradientSpace.LiftL2 period)) (t δ c : ℝ) (K' : ↥(EulerLiftedGradientSpace.LiftL2 period) →L[ℝ] ↥(EulerLiftedGradientSpace.LiftL2 period)) (e' z p forcing : ↥(EulerLiftedGradientSpace.LiftL2 period)) (hδ : 0 < δ) (hc : 0 < c) (hKt : HasDerivAt (metricFamily period K hKm C hC) K' t) (het : HasDerivAt e e' t) (hKs : ∀ (x : EulerLiftedGradientSpace.LiftDomain period), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift period (K t) x)) (g : EulerLiftedGradientSpace.LiftDomain period → EulerLiftedGradientSpace.Vector3) (hrep : ↑↑(e t) =ᵐ[EulerLiftedGradientSpace.liftMeasure period] g) (hes : ∀ (x : EulerLiftedGradientSpace.LiftDomain period), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift period g x)) (hDe : MeasureTheory.MemLp (fun (x : EulerLiftedGradientSpace.LiftDomain period) => fderiv ℝ (EulerMetricTransport.localFieldLift period g x) 0) 2 (EulerLiftedGradientSpace.liftMeasure period)) (hsym : ∀ (x : EulerLiftedGradientSpace.LiftDomain period) (v w : EulerLiftedGradientSpace.Vector3), inner ℝ ((K t x) v) w = inner ℝ v ((K t x) w)) (hpos : ∀ (x : EulerLiftedGradientSpace.LiftDomain period) (v : EulerLiftedGradientSpace.Vector3), c ^ 2 * ‖v‖ ^ 2 ≤ inner ℝ ((K t x) v) v) (G : EulerLiftedGradientSpace.LiftDomain period → EulerLiftedGradientSpace.Vector3 →L[ℝ] EulerLiftedGradientSpace.Vector3) (hGm : MeasureTheory.AEStronglyMeasurable G (EulerLiftedGradientSpace.liftMeasure period)) (E : NNReal) (hG : ∀ (x : EulerLiftedGradientSpace.LiftDomain period), ‖G x‖ ≤ ↑E) (hKG : ∀ (x : EulerLiftedGradientSpace.LiftDomain period) (v : EulerLiftedGradientSpace.Vector3), (K t x) ((G x) v) = v) (hep : e t ∈ EulerLiftedGradientSpace.divergenceFreeSpace period κ m) (hp : p ∈ EulerLiftedGradientSpace.gradientSpace period κ m) (hz : z ∈ EulerLiftedGradientSpace.divergenceFreeSpace period κ m) (D B : NNReal) (hD : ∀ (x : EulerLiftedGradientSpace.LiftDomain period), ‖fderiv ℝ (EulerMetricTransport.localFieldLift period (K t) x) 0‖ ≤ ↑D) (hzB : ∀ᵐ (x : EulerLiftedGradientSpace.LiftDomain period) ∂EulerLiftedGradientSpace.liftMeasure period, ‖↑↑z x‖ ≤ ↑B) (heq : e' + liftedTransport period κ m g z hDe B hzB + (EulerLiftedPressure.coefficientOperator G hGm E hG) p = forcing) : deriv (fun (s : ℝ) => √(inner ℝ ((metricFamily period K hKm C hC s) (e s)) (e s) + δ ^ 2)) t ≤ (‖K'‖ + ↑D * ((|κ| + ‖m‖) * ↑B)) / (2 * c ^ 2) * √(inner ℝ ((metricFamily period K hKm C hC t) (e t)) (e t) + δ ^ 2) + ↑C / c * ‖forcing‖

The metric norm estimate for the actual lifted transport-pressure equation.