The local complete Sobolev mild map #
Heat evolution and the translated nonlinear Stokes integral define a continuous complete H²ᵏ trajectory on every closed local interval.
noncomputable def
CKN.Leray.regularisedBesselLocalMap
(ρ : RegMollifierProfile)
(ε : ℝ)
(hε : 0 < ε)
(k : ℕ)
(b : BesselPotentialSpace Foundation.Parabolic.L2Vec3 ComplexVec3 (↑(2 * k)) 2)
(T : ℝ)
(hT : 0 ≤ T)
(u : C(↑(RegularizedMildTimeInterval T), BesselPotentialSpace Foundation.Parabolic.L2Vec3 ComplexVec3 (↑(2 * k)) 2))
:
The complete Sobolev mild map on a closed local time interval.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
CKN.Leray.regularisedBesselLocalMap_apply
(ρ : RegMollifierProfile)
(ε : ℝ)
(hε : 0 < ε)
(k : ℕ)
(b : BesselPotentialSpace Foundation.Parabolic.L2Vec3 ComplexVec3 (↑(2 * k)) 2)
(T : ℝ)
(hT : 0 ≤ T)
(u : C(↑(RegularizedMildTimeInterval T), BesselPotentialSpace Foundation.Parabolic.L2Vec3 ComplexVec3 (↑(2 * k)) 2))
(t : ↑(RegularizedMildTimeInterval T))
:
(regularisedBesselLocalMap ρ ε hε k b T hT u) t = regularisedBesselHeat ↑(2 * k) ↑t ⋯ b - ∫ (τ : ℝ) in 0..T, regularisedBesselShiftedStokesIntegrand k (regularisedBesselClampedTensorPath ρ ε hε k T hT u) (↑t) τ
Evaluation of the local complete Sobolev map is heat minus the translated complete nonlinear Stokes integral.