Linearized complete Sobolev tensor path #
Fixing the physical L² velocity in the first factor of the regularized tensor leaves a bounded linear map in its complete Sobolev second factor.
noncomputable def
CKN.Leray.regularisedBesselLinearTensorPath
(ρ : RegMollifierProfile)
(ε : ℝ)
(hε : 0 < ε)
(k : ℕ)
(T : ℝ)
(hT : 0 ≤ T)
(g : C(↑(RegularizedMildTimeInterval T), ↥ComplexVectorL2))
(v : C(↑(RegularizedMildTimeInterval T), BesselPotentialSpace Foundation.Parabolic.L2Vec3 ComplexVec3 (↑(2 * k)) 2))
:
ℝ → BesselPotentialSpace Foundation.Parabolic.L2Vec3 ComplexTensor3 (↑(2 * k)) 2
The clamped complete tensor path with a prescribed physical L² first factor and an unknown complete Sobolev second factor.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
CKN.Leray.regularisedBesselLinearTensorPath_continuous
(ρ : RegMollifierProfile)
(ε : ℝ)
(hε : 0 < ε)
(k : ℕ)
(T : ℝ)
(hT : 0 ≤ T)
(g : C(↑(RegularizedMildTimeInterval T), ↥ComplexVectorL2))
(v : C(↑(RegularizedMildTimeInterval T), BesselPotentialSpace Foundation.Parabolic.L2Vec3 ComplexVec3 (↑(2 * k)) 2))
:
Continuous (regularisedBesselLinearTensorPath ρ ε hε k T hT g v)
The prescribed L² path and complete Sobolev path produce a continuous complete tensor path.
theorem
CKN.Leray.regularisedBesselLinearTensorPath_norm_le
(ρ : RegMollifierProfile)
(ε : ℝ)
(hε : 0 < ε)
(k : ℕ)
(T : ℝ)
(hT : 0 ≤ T)
(g : C(↑(RegularizedMildTimeInterval T), ↥ComplexVectorL2))
(v : C(↑(RegularizedMildTimeInterval T), BesselPotentialSpace Foundation.Parabolic.L2Vec3 ComplexVec3 (↑(2 * k)) 2))
(B : ℝ)
(hB : 0 ≤ B)
(hg : ∀ (q : ↑(RegularizedMildTimeInterval T)), ‖g q‖ ≤ B)
(s : ℝ)
:
‖regularisedBesselLinearTensorPath ρ ε hε k T hT g v s‖ ≤ regularisedBesselTensorConstant ρ ε hε k * B * ‖v‖
A uniform physical L² bound makes the linearized tensor path bounded linearly in the complete Sobolev trajectory norm.
theorem
CKN.Leray.regularisedBesselLinearTensorPath_difference_norm_le
(ρ : RegMollifierProfile)
(ε : ℝ)
(hε : 0 < ε)
(k : ℕ)
(T : ℝ)
(hT : 0 ≤ T)
(g : C(↑(RegularizedMildTimeInterval T), ↥ComplexVectorL2))
(v w : C(↑(RegularizedMildTimeInterval T), BesselPotentialSpace Foundation.Parabolic.L2Vec3 ComplexVec3 (↑(2 * k)) 2))
(B : ℝ)
(hB : 0 ≤ B)
(hg : ∀ (q : ↑(RegularizedMildTimeInterval T)), ‖g q‖ ≤ B)
(s : ℝ)
:
‖regularisedBesselLinearTensorPath ρ ε hε k T hT g v s - regularisedBesselLinearTensorPath ρ ε hε k T hT g w s‖ ≤ regularisedBesselTensorConstant ρ ε hε k * B * ‖v - w‖
With the physical coefficient fixed, the complete tensor path is globally Lipschitz in the Sobolev trajectory norm.