Uniform time step for complete Sobolev energy control

The physical L² energy bound fixes a positive time step on which the complete Sobolev mild estimate can always be absorbed.

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

A time step depending on the physical L² bound and the regularized tensor operator, independent of the current H²ᵏ norm.

Equations

• CKN.Leray.regularisedBesselUniformEnergyStep ρ ε hε k B = (√(2 * Real.exp 1) / (8 * (1 + CKN.Leray.regularisedBesselTensorConstant ρ ε hε k * B))) ^ 2

theorem CKN.Leray.regularisedBesselUniformEnergyStep_pos (ρ : RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) (k : ℕ) (B : ℝ) (hB : 0 ≤ B) : 0 < regularisedBesselUniformEnergyStep ρ ε hε k B

The complete Sobolev energy time step is strictly positive under a nonnegative physical L² bound.

theorem CKN.Leray.regularisedBesselUniformEnergyStep_small (ρ : RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) (k : ℕ) (B : ℝ) (hB : 0 ≤ B) : 2 * (regularisedBesselTensorConstant ρ ε hε k * B / √(2 * Real.exp 1)) * √(regularisedBesselUniformEnergyStep ρ ε hε k B) ≤ 1 / 2

The uniform energy time step makes the Abel coefficient at most one half, independently of the complete Sobolev norm.