Complete Sobolev tensor paths on a closed time interval #
Clamping a Sobolev velocity path to its lifespan gives a continuous quadratic tensor path with a uniform bound and a local Lipschitz estimate.
noncomputable def
CKN.Leray.regularisedBesselClampedTensorPath
(ρ : RegMollifierProfile)
(ε : ℝ)
(hε : 0 < ε)
(k : ℕ)
(T : ℝ)
(hT : 0 ≤ T)
(u : C(↑(RegularizedMildTimeInterval T), BesselPotentialSpace Foundation.Parabolic.L2Vec3 ComplexVec3 (↑(2 * k)) 2))
:
ℝ → BesselPotentialSpace Foundation.Parabolic.L2Vec3 ComplexTensor3 (↑(2 * k)) 2
The complete H²ᵏ tensor path, extended to real time by clamping.
Equations
- CKN.Leray.regularisedBesselClampedTensorPath ρ ε hε k T hT u s = CKN.Leray.regularisedBesselTensorQuadratic ρ ε hε k (u (CKN.Leray.regularizedMildTimeClamp T hT s))
Instances For
theorem
CKN.Leray.regularisedBesselClampedTensorPath_continuous
(ρ : RegMollifierProfile)
(ε : ℝ)
(hε : 0 < ε)
(k : ℕ)
(T : ℝ)
(hT : 0 ≤ T)
(u : C(↑(RegularizedMildTimeInterval T), BesselPotentialSpace Foundation.Parabolic.L2Vec3 ComplexVec3 (↑(2 * k)) 2))
:
Continuous (regularisedBesselClampedTensorPath ρ ε hε k T hT u)
The clamped complete tensor path is continuous.
theorem
CKN.Leray.regularisedBesselClampedTensorPath_norm_le
(ρ : RegMollifierProfile)
(ε : ℝ)
(hε : 0 < ε)
(k : ℕ)
(T : ℝ)
(hT : 0 ≤ T)
(u : C(↑(RegularizedMildTimeInterval T), BesselPotentialSpace Foundation.Parabolic.L2Vec3 ComplexVec3 (↑(2 * k)) 2))
(R : ℝ)
(hR : 0 ≤ R)
(hu : ∀ (t : ↑(RegularizedMildTimeInterval T)), ‖u t‖ ≤ R)
(s : ℝ)
:
‖regularisedBesselClampedTensorPath ρ ε hε k T hT u s‖ ≤ regularisedBesselTensorConstant ρ ε hε k * R ^ 2
A uniform velocity bound gives a quadratic bound for the clamped complete tensor path.
theorem
CKN.Leray.regularisedBesselClampedTensorPath_difference_norm_le
(ρ : RegMollifierProfile)
(ε : ℝ)
(hε : 0 < ε)
(k : ℕ)
(T : ℝ)
(hT : 0 ≤ T)
(u v : C(↑(RegularizedMildTimeInterval T), BesselPotentialSpace Foundation.Parabolic.L2Vec3 ComplexVec3 (↑(2 * k)) 2))
(R : ℝ)
(hu : ∀ (t : ↑(RegularizedMildTimeInterval T)), ‖u t‖ ≤ R)
(hv : ∀ (t : ↑(RegularizedMildTimeInterval T)), ‖v t‖ ≤ R)
(s : ℝ)
:
‖regularisedBesselClampedTensorPath ρ ε hε k T hT u s - regularisedBesselClampedTensorPath ρ ε hε k T hT v s‖ ≤ regularisedBesselTensorConstant ρ ε hε k * (2 * R) * ‖u - v‖
On a common bounded ball, the clamped complete tensor path is Lipschitz in the trajectory supremum norm.