Genuine metric transport energy on finite Sobolev fields, obtained by smooth convolution limits.
noncomputable def
EulerSobolevMetricTransport.transportOperator
(period : ℝ)
[Fact (0 < period)]
{q : ℕ}
(hq : 3 ≤ q)
(κ : ℝ)
(m : EulerLiftedGradientSpace.Vector3)
(z : ↥(EulerCylinderSobolevSpace.SobolevSpace period q))
:
Actual lifted transport is a bounded map H¹→L² for each fixed Hq velocity, q≥3.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
EulerSobolevMetricTransport.transportOperator_apply
(period : ℝ)
[Fact (0 < period)]
{q : ℕ}
(hq : 3 ≤ q)
(κ : ℝ)
(m : EulerLiftedGradientSpace.Vector3)
(z : ↥(EulerCylinderSobolevSpace.SobolevSpace period q))
(e : ↥(EulerCylinderSobolevSpace.SobolevSpace period 1))
:
(transportOperator period hq κ m z) e = ∑ i : Fin 4,
EulerSobolevL2Product.scalarProduct period hq (EulerSobolevTransport.velocityComponents κ m i) z
(EulerCylinderSobolevSpace.value period ((EulerCylinderSobolevSpace.derivativeOperator period 0 i) e))
The Sobolev transport operator is the literal sum of coefficient-times-coordinate-derivative products.
theorem
EulerSobolevMetricTransport.representative_fderiv_memLp
(period : ℝ)
[Fact (0 < period)]
(e : ↥(EulerCylinderSobolevSpace.SobolevSpace period 1))
(g : EulerLiftedGradientSpace.LiftDomain period → EulerLiftedGradientSpace.Vector3)
(he : ↑↑(EulerCylinderSobolevSpace.value period e) =ᵐ[EulerLiftedGradientSpace.liftMeasure period] g)
(hg :
∀ (x : EulerLiftedGradientSpace.LiftDomain period), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift period g x))
:
MeasureTheory.MemLp
(fun (x : EulerLiftedGradientSpace.LiftDomain period) => fderiv ℝ (EulerMetricTransport.localFieldLift period g x) 0)
2 (EulerLiftedGradientSpace.liftMeasure period)
A smooth representative of an actual H¹ class has its full classical gradient in L².
theorem
EulerSobolevMetricTransport.transportOperator_eq_representative
(period : ℝ)
[Fact (0 < period)]
{q : ℕ}
(hq : 3 ≤ q)
(κ : ℝ)
(m : EulerLiftedGradientSpace.Vector3)
(z : ↥(EulerCylinderSobolevSpace.SobolevSpace period q))
(e : ↥(EulerCylinderSobolevSpace.SobolevSpace period 1))
(g : EulerLiftedGradientSpace.LiftDomain period → EulerLiftedGradientSpace.Vector3)
(he : ↑↑(EulerCylinderSobolevSpace.value period e) =ᵐ[EulerLiftedGradientSpace.liftMeasure period] g)
(hg :
∀ (x : EulerLiftedGradientSpace.LiftDomain period), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift period g x))
(hDg :
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, ‖↑↑(EulerCylinderSobolevSpace.value period z) x‖ ≤ ↑B)
:
(transportOperator period hq κ m z) e = EulerRepresentativeMetricEvolution.liftedTransport period κ m g (EulerCylinderSobolevSpace.value period z) hDg B hzB
On any actual smooth representative, Sobolev transport equals the genuine classical lifted differential expression.
theorem
EulerSobolevMetricTransport.metric_transport_bound
(period : ℝ)
[Fact (0 < period)]
{q : ℕ}
(hq : 3 ≤ q)
(κ : ℝ)
(m : EulerLiftedGradientSpace.Vector3)
(K : EulerSpatialSobolevInverse.SmoothCoefficient period)
(z : ↥(EulerCylinderSobolevSpace.SobolevSpace period q))
(e : ↥(EulerCylinderSobolevSpace.SobolevSpace period 1))
(hsym :
∀ (x : EulerLiftedGradientSpace.LiftDomain period) (v w : EulerLiftedGradientSpace.Vector3),
inner ℝ ((K.coefficient x) v) w = inner ℝ v ((K.coefficient x) w))
(hz : EulerCylinderSobolevSpace.value period z ∈ EulerLiftedGradientSpace.divergenceFreeSpace period κ m)
(B : NNReal)
(hzB :
∀ᵐ (x : EulerLiftedGradientSpace.LiftDomain period) ∂EulerLiftedGradientSpace.liftMeasure period, ‖↑↑(EulerCylinderSobolevSpace.value period z) x‖ ≤ ↑B)
:
Metric transport cancellation extends from actual smooth convolutions to every H¹ field.