Physical H¹ traces of the regularized mild path

The Bessel path supplies continuous L² classes for its ordered derivatives. This module identifies those classes with the pointwise derivatives of the regularized velocity on the full closed time interval.

noncomputable def ESS.LPS.regH1InverseWeight (ξ : CKN.Foundation.Parabolic.L2Vec3) : ℂ

The inverse Bessel weight of order four used for the regularized H1 trace.

Equations

• ESS.LPS.regH1InverseWeight ξ = ↑((1 + ‖ξ‖ ^ 2) ^ (-2))

theorem ESS.LPS.regH1InverseWeight_memLp : MeasureTheory.MemLp regH1InverseWeight ⊤ MeasureTheory.volume

noncomputable def ESS.LPS.regH1InverseWeightLp : ↥(MeasureTheory.Lp ℂ ⊤ MeasureTheory.volume)

The inverse Bessel weight represented as an essentially bounded multiplier.

Equations

• ESS.LPS.regH1InverseWeightLp = MeasureTheory.MemLp.toLp ESS.LPS.regH1InverseWeight ESS.LPS.regH1InverseWeight_memLp

noncomputable def ESS.LPS.regH1DerivativeMultiplier (j : Fin 3) (ξ : CKN.Foundation.Parabolic.L2Vec3) : ℂ

The coordinate derivative symbol multiplied by the inverse Bessel weight.

Equations

• ESS.LPS.regH1DerivativeMultiplier j ξ = CKN.Leray.regR12CoordSymbol j ξ * ESS.LPS.regH1InverseWeight ξ

theorem ESS.LPS.lps_regularised_h1_trace (ρ : CKN.Leray.RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) (a : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3) (ha : CKN.IsInJ a) (T : ℝ) (hT : 0 ≤ T) : ∃ (U : C(↑(CKN.Leray.RegularizedMildTimeInterval T), ↥CKN.Leray.RealVectorL2)) (DU : Fin 3 → C(↑(CKN.Leray.RegularizedMildTimeInterval T), ↥CKN.Leray.RealVectorL2)), (∀ (s : ↑(CKN.Leray.RegularizedMildTimeInterval T)), (fun (x : CKN.Foundation.Parabolic.Vec3) => CKN.Leray.regR12Velocity ρ ε hε a ha (x, ↑s)) =ᵐ[MeasureTheory.volume] CKN.Leray.realVectorL2Representative (U s)) ∧ ∀ (s : ↑(CKN.Leray.RegularizedMildTimeInterval T)) (i j : Fin 3), (fun (x : CKN.Foundation.Parabolic.Vec3) => CKN.spatialPartial (fun (y : CKN.Foundation.Parabolic.ParabolicPoint) => CKN.Leray.regR12Velocity ρ ε hε a ha y i) j (x, ↑s)) =ᵐ[MeasureTheory.volume] fun (x : CKN.Foundation.Parabolic.Vec3) => CKN.Leray.realVectorL2Representative ((DU j) s) x i

The regularized velocity and its pointwise first derivatives are the continuous physical L² paths of the Bessel lift, on the full closed interval. This supplies the physical H¹ trace at the initial time.

theorem ESS.LPS.lps_regularised_h1_energy_continuous (ρ : CKN.Leray.RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) (a : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3) (ha : CKN.IsInJ a) (T : ℝ) (hT : 0 ≤ T) : ∃ (U : C(↑(CKN.Leray.RegularizedMildTimeInterval T), ↥CKN.Leray.RealVectorL2)) (DU : Fin 3 → C(↑(CKN.Leray.RegularizedMildTimeInterval T), ↥CKN.Leray.RealVectorL2)), (∀ (s : ↑(CKN.Leray.RegularizedMildTimeInterval T)), (fun (x : CKN.Foundation.Parabolic.Vec3) => CKN.Leray.regR12Velocity ρ ε hε a ha (x, ↑s)) =ᵐ[MeasureTheory.volume] CKN.Leray.realVectorL2Representative (U s)) ∧ (∀ (s : ↑(CKN.Leray.RegularizedMildTimeInterval T)) (i j : Fin 3), (fun (x : CKN.Foundation.Parabolic.Vec3) => CKN.spatialPartial (fun (y : CKN.Foundation.Parabolic.ParabolicPoint) => CKN.Leray.regR12Velocity ρ ε hε a ha y i) j (x, ↑s)) =ᵐ[MeasureTheory.volume] fun (x : CKN.Foundation.Parabolic.Vec3) => CKN.Leray.realVectorL2Representative ((DU j) s) x i) ∧ Continuous fun (s : ↑(CKN.Leray.RegularizedMildTimeInterval T)) => ‖U s‖ ^ 2 + ∑ j : Fin 3, ‖(DU j) s‖ ^ 2

The physical squared H¹ energy of the regularized path is continuous on the closed time interval, including its initial trace (prop:lps-local-strong).