Local lifespan for the complete Sobolev mild equation

The lifespan is chosen from a positive bound for the tensor map and the initial complete Sobolev norm.

noncomputable def CKN.Leray.regularisedBesselLocalCoefficient (ρ : RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) (k : ℕ) : ℝ

A positive coefficient larger than the complete tensor operator norm.

Equations

• CKN.Leray.regularisedBesselLocalCoefficient ρ ε hε k = 1 + CKN.Leray.regularisedBesselTensorConstant ρ ε hε k

noncomputable def CKN.Leray.regularisedBesselLocalRadius (k : ℕ) (b : BesselPotentialSpace Foundation.Parabolic.L2Vec3 ComplexVec3 (↑(2 * k)) 2) : ℝ

The closed ball radius used for the complete Sobolev contraction.

Equations

• CKN.Leray.regularisedBesselLocalRadius k b = 2 * (1 + ‖b‖)

noncomputable def CKN.Leray.regularisedBesselLocalLifespan (ρ : RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) (k : ℕ) (b : BesselPotentialSpace Foundation.Parabolic.L2Vec3 ComplexVec3 (↑(2 * k)) 2) : ℝ

A strictly positive local lifespan for complete H²ᵏ data.

Equations

• CKN.Leray.regularisedBesselLocalLifespan ρ ε hε k b = (16 * CKN.Leray.regularisedBesselLocalCoefficient ρ ε hε k * (1 + ‖b‖))⁻¹ ^ 2

theorem CKN.Leray.regularisedBesselLocalCoefficient_pos (ρ : RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) (k : ℕ) : 0 < regularisedBesselLocalCoefficient ρ ε hε k

The coefficient defining the complete Sobolev lifespan is positive.

theorem CKN.Leray.regularisedBesselLocalLifespan_pos (ρ : RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) (k : ℕ) (b : BesselPotentialSpace Foundation.Parabolic.L2Vec3 ComplexVec3 (↑(2 * k)) 2) : 0 < regularisedBesselLocalLifespan ρ ε hε k b

The complete Sobolev local lifespan is positive.

theorem CKN.Leray.regularisedBesselLocalLifespan_sqrt (ρ : RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) (k : ℕ) (b : BesselPotentialSpace Foundation.Parabolic.L2Vec3 ComplexVec3 (↑(2 * k)) 2) : √(regularisedBesselLocalLifespan ρ ε hε k b) = (16 * regularisedBesselLocalCoefficient ρ ε hε k * (1 + ‖b‖))⁻¹

The square root of the lifespan equals its positive inverse scale.