The actual Gaussian heat and Volterra integrals preserve the lifted divergence constraint.
theorem
EulerDivergenceFreeHeat.gradientProjection_lineHeat
(period : ℝ)
[Fact (0 < period)]
(κ : ℝ)
(m : EulerLiftedGradientSpace.Vector3)
(a : EulerLiftedGradientSpace.LiftTangent)
(v : NNReal)
(f : ↥(EulerLiftedGradientSpace.LiftL2 period))
:
(EulerLiftedGradientSpace.gradientProjection period κ m) (EulerGaussianCylinderHeat.lineHeat period a v f) = EulerGaussianCylinderHeat.lineHeat period a v ((EulerLiftedGradientSpace.gradientProjection period κ m) f)
The actual lifted gradient projection commutes with each Gaussian directional heat average.
theorem
EulerDivergenceFreeHeat.gradientProjection_heatList
(period : ℝ)
[Fact (0 < period)]
(κ : ℝ)
(m : EulerLiftedGradientSpace.Vector3)
(directions : List EulerLiftedGradientSpace.LiftTangent)
(v : NNReal)
(f : ↥(EulerLiftedGradientSpace.LiftL2 period))
:
(EulerLiftedGradientSpace.gradientProjection period κ m) (EulerGaussianCylinderHeat.heatList period directions v f) = EulerGaussianCylinderHeat.heatList period directions v ((EulerLiftedGradientSpace.gradientProjection period κ m) f)
The lifted gradient projection commutes with every finite product of Gaussian heat averages.
theorem
EulerDivergenceFreeHeat.gradientProjection_cylinderHeat
(period : ℝ)
[Fact (0 < period)]
(κ : ℝ)
(m : EulerLiftedGradientSpace.Vector3)
(v : NNReal)
(f : ↥(EulerLiftedGradientSpace.LiftL2 period))
:
(EulerLiftedGradientSpace.gradientProjection period κ m) ((EulerGaussianCylinderHeat.cylinderHeat period v) f) = (EulerGaussianCylinderHeat.cylinderHeat period v) ((EulerLiftedGradientSpace.gradientProjection period κ m) f)
The actual cylinder heat semigroup preserves the lifted gradient projection exactly.
noncomputable def
EulerDivergenceFreeHeat.gradientEvaluation
(period : ℝ)
[Fact (0 < period)]
(q : ℕ)
(κ : ℝ)
(m : EulerLiftedGradientSpace.Vector3)
:
The continuous constraint map on an actual complete Sobolev space.
Equations
- EulerDivergenceFreeHeat.gradientEvaluation period q κ m = EulerLiftedGradientSpace.gradientProjection period κ m ∘SL EulerCylinderSobolevSpace.valueOperator period q
Instances For
@[simp]
theorem
EulerDivergenceFreeHeat.gradientEvaluation_apply
(period : ℝ)
[Fact (0 < period)]
{q : ℕ}
(κ : ℝ)
(m : EulerLiftedGradientSpace.Vector3)
(u : ↥(EulerCylinderSobolevSpace.SobolevSpace period q))
:
(gradientEvaluation period q κ m) u = (EulerLiftedGradientSpace.gradientProjection period κ m) (EulerCylinderSobolevSpace.value period u)
The Sobolev constraint is exactly the underlying lifted L² gradient projection.
theorem
EulerDivergenceFreeHeat.gradientEvaluation_zero_iff
(period : ℝ)
[Fact (0 < period)]
{q : ℕ}
(κ : ℝ)
(m : EulerLiftedGradientSpace.Vector3)
(u : ↥(EulerCylinderSobolevSpace.SobolevSpace period q))
:
(gradientEvaluation period q κ m) u = 0 ↔ EulerCylinderSobolevSpace.value period u ∈ EulerLiftedGradientSpace.divergenceFreeSpace period κ m
Vanishing of the continuous constraint map is exactly membership in the genuine divergence-free subspace.
theorem
EulerDivergenceFreeHeat.gradientEvaluation_heat
(period : ℝ)
[Fact (0 < period)]
{q : ℕ}
(κ : ℝ)
(m : EulerLiftedGradientSpace.Vector3)
(v : NNReal)
(u : ↥(EulerCylinderSobolevSpace.SobolevSpace period q))
:
(gradientEvaluation period q κ m) ((EulerSobolevHeat.heatOperator period q v) u) = (EulerGaussianCylinderHeat.cylinderHeat period v) ((gradientEvaluation period q κ m) u)
The Sobolev heat flow evolves the divergence constraint by the same genuine L² heat semigroup.
theorem
EulerDivergenceFreeHeat.heatGain_preserves_gradient_zero
(period : ℝ)
[Fact (0 < period)]
{q : ℕ}
(κ : ℝ)
(m : EulerLiftedGradientSpace.Vector3)
(v : NNReal)
(hv : 0 < v)
(u : ↥(EulerCylinderSobolevSpace.SobolevSpace period q))
(hu : (gradientEvaluation period q κ m) u = 0)
:
The derivative-gaining heat operator preserves vanishing lifted divergence.
theorem
EulerDivergenceFreeHeat.heatKernel_preserves_gradient_zero
(period : ℝ)
[Fact (0 < period)]
{q : ℕ}
(κ : ℝ)
(m : EulerLiftedGradientSpace.Vector3)
(ν : ℝ)
(hν : 0 < ν)
(r : ℝ)
(u : ↥(EulerCylinderSobolevSpace.SobolevSpace period q))
(hu : (gradientEvaluation period q κ m) u = 0)
:
The actual viscosity-scaled heat kernel preserves zero lifted divergence at every real time.
theorem
EulerDivergenceFreeHeat.heatConvolution_preserves_gradient_zero
(period : ℝ)
[Fact (0 < period)]
{q : ℕ}
(κ : ℝ)
(m : EulerLiftedGradientSpace.Vector3)
(ν : ℝ)
(hν : 0 < ν)
(T : ℝ)
(hT : 0 ≤ T)
(f : C(↑(Set.Icc 0 T), ↥(EulerCylinderSobolevSpace.SobolevSpace period q)))
(hf : ∀ (t : ↑(Set.Icc 0 T)), (gradientEvaluation period q κ m) (f t) = 0)
(t : ↑(Set.Icc 0 T))
:
(gradientEvaluation period (q + 1) κ m)
((EulerVolterraConvolution.convolution T hT (EulerSobolevHeat.heatKernel period q ν hν)
(EulerSobolevHeat.parabolicKernelBound ν) ⋯ ⋯ ⋯ ⋯ f)
t) = 0
The actual Bochner Volterra convolution of divergence-free forcing remains divergence-free.
theorem
EulerDivergenceFreeHeat.mild_solution_preserves_gradient_zero
(period : ℝ)
[Fact (0 < period)]
{q : ℕ}
(κ : ℝ)
(m : EulerLiftedGradientSpace.Vector3)
(ν : ℝ)
(hν : 0 < ν)
(T : ℝ)
(hT : 0 ≤ T)
(u₀ : ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 1)))
(hu₀ : (gradientEvaluation period (q + 1) κ m) u₀ = 0)
(F :
↑(Set.Icc 0 T) →
↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 1)) → ↥(EulerCylinderSobolevSpace.SobolevSpace period q))
(hF : Continuous fun (p : ↑(Set.Icc 0 T) × ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 1))) => F p.1 p.2)
(hFzero :
∀ (t : ↑(Set.Icc 0 T)) (u : ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 1))),
(gradientEvaluation period q κ m) (F t u) = 0)
(u : C(↑(Set.Icc 0 T), ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 1))))
(hsol :
∀ (t : ↑(Set.Icc 0 T)),
u t = (EulerSobolevHeat.heatOperator period (q + 1) (2 * ν * ↑t).toNNReal) u₀ + ∫ (r : ℝ) in 0..↑t, (EulerSobolevHeat.heatKernel period q ν hν r)
(F (Set.projIcc 0 T hT (↑t - r)) (u (Set.projIcc 0 T hT (↑t - r)))))
(t : ↑(Set.Icc 0 T))
:
Every actual heat mild solution with projected forcing preserves the initial lifted divergence constraint.