Time scale for the local regularized mild solution

These constants are the lifespan parameters in lem:reg-local-mild.

noncomputable def CKN.Leray.regularizedMildProfileL2Norm (ρ : RegMollifierProfile) : ℝ

The profile's real L² norm, expressed through its Lᵖ seminorm.

Equations

• CKN.Leray.regularizedMildProfileL2Norm ρ = (MeasureTheory.eLpNorm (⇑ρ.rho) 2 MeasureTheory.volume).toReal

noncomputable def CKN.Leray.regularizedMildAeps (ρ : RegMollifierProfile) (ε : ℝ) : ℝ

The Abel-kernel constant for the regularized mild contraction.

Equations

• CKN.Leray.regularizedMildAeps ρ ε = CKN.Leray.regularizedMildProfileL2Norm ρ * ε ^ (-(3 / 2)) / √(2 * Real.exp 1)

noncomputable def CKN.Leray.regularizedMildLocalLifespan (ρ : RegMollifierProfile) (ε : ℝ) (b : ↥RealVectorL2) : ℝ

The lifespan in lem:reg-local-mild.

Equations

• CKN.Leray.regularizedMildLocalLifespan ρ ε b = (16 * CKN.Leray.regularizedMildAeps ρ ε * (1 + ‖b‖))⁻¹ ^ 2

theorem CKN.Leray.regularizedMildMollifierConstant_eq_profile (ρ : RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) : regularizedMildMollifierConstant ρ ε = regularizedMildProfileL2Norm ρ * ε ^ (-(3 / 2))

The parameter in the quadratic tensor bounds is the profile norm times the spatial scale factor.

theorem CKN.Leray.regularizedMildAeps_pos (ρ : RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) : 0 < regularizedMildAeps ρ ε

The Abel constant and local lifespan are positive for every admissible profile and positive regularization scale.

theorem CKN.Leray.regularizedMildLocalLifespan_pos (ρ : RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) (b : ↥RealVectorL2) : 0 < regularizedMildLocalLifespan ρ ε b