Linear complete Sobolev mild map with prescribed physical velocity #
The fixed physical L² velocity enters the first tensor factor, while the unknown complete Sobolev trajectory enters the second factor.
noncomputable def
CKN.Leray.regularisedBesselLinearLocalMap
(ρ : RegMollifierProfile)
(ε : ℝ)
(hε : 0 < ε)
(k : ℕ)
(b : BesselPotentialSpace Foundation.Parabolic.L2Vec3 ComplexVec3 (↑(2 * k)) 2)
(T : ℝ)
(hT : 0 ≤ T)
(g : C(↑(RegularizedMildTimeInterval T), ↥ComplexVectorL2))
(B : ℝ)
(hB : 0 ≤ B)
(hg : ∀ (q : ↑(RegularizedMildTimeInterval T)), ‖g q‖ ≤ B)
(v : C(↑(RegularizedMildTimeInterval T), BesselPotentialSpace Foundation.Parabolic.L2Vec3 ComplexVec3 (↑(2 * k)) 2))
:
The local complete Sobolev mild map linearized around a prescribed physical L² trajectory.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
CKN.Leray.regularisedBesselLinearLocalMap_apply
(ρ : RegMollifierProfile)
(ε : ℝ)
(hε : 0 < ε)
(k : ℕ)
(b : BesselPotentialSpace Foundation.Parabolic.L2Vec3 ComplexVec3 (↑(2 * k)) 2)
(T : ℝ)
(hT : 0 ≤ T)
(g : C(↑(RegularizedMildTimeInterval T), ↥ComplexVectorL2))
(B : ℝ)
(hB : 0 ≤ B)
(hg : ∀ (q : ↑(RegularizedMildTimeInterval T)), ‖g q‖ ≤ B)
(v : C(↑(RegularizedMildTimeInterval T), BesselPotentialSpace Foundation.Parabolic.L2Vec3 ComplexVec3 (↑(2 * k)) 2))
(t : ↑(RegularizedMildTimeInterval T))
:
(regularisedBesselLinearLocalMap ρ ε hε k b T hT g B hB hg v) t = regularisedBesselHeat ↑(2 * k) ↑t ⋯ b - ∫ (τ : ℝ) in 0..T, regularisedBesselShiftedStokesIntegrand k (regularisedBesselLinearTensorPath ρ ε hε k T hT g v) (↑t) τ
Evaluation of the linear complete Sobolev mild map.