Documentation

LeanPool.CaffarelliKohnNirenberg.Core.Endgame.TheoremAAdaptersLin34

Theorem AAdapters Lin34 #

Part of the Caffarelli–Kohn–Nirenberg partial regularity proof.

Theorem A at the constant of prop:lin34 #

The small-data statement thm:A of paper/ckn.tex consumes the oscillation display eq:lin35-force of prop:lin34 with the constant attached to the solution data. This module fixes that constant, theoremALin34Constant q, as the value lin34SolutionForceExponent of prop:lin34 evaluated at the Calderón--Zygmund constant lin34CZConstant of ext:CZ, and records that it is nonnegative.

The adapter theoremA_hLin34_of_sws then restates eq:lin35-force in exactly the shape thm:A expects, with no analytic hypothesis left: the Calderón-- Zygmund bound ext:CZ for the centred leading pressure term is supplied by lin34_hCZ_p1_of_residual_ae_of_sws, whose Liouville decay input is the content of ext:newtonian, itself discharged for suitable weak solutions by lin34_centred_residual_local_growth_ae_of_sws. Both are proved here rather than assumed, so the only inputs of the exported display are the suitable weak solution and the geometric side conditions on the cylinder.

source
noncomputable def CKN.Core.Endgame.theoremALin34Constant (q : ℝ) :
ℝ

The constant of the oscillation display eq:lin35-force of prop:lin34 for the solution data of thm:A, that is, the exponent constant lin34SolutionForceExponent evaluated at the Calderón--Zygmund constant lin34CZConstant of ext:CZ.

Equations
Instances For
    source
    theorem CKN.Core.Endgame.theoremALin34Constant_nonneg (q : ℝ) (hq : 5 / 2 < q) :
    0 ≤ theoremALin34Constant q

    The constant of eq:lin35-force is nonnegative for every q > 5/2, the range of exponents in which prop:lin34 applies.

    source
    theorem CKN.Core.Endgame.theoremA_hLin34_of_sws (q : ℝ) {Ω : Set Foundation.Parabolic.Vec3} {I : Set ℝ} {u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} {Du : Foundation.Parabolic.ParabolicPoint → Fin 3 → Foundation.Parabolic.Vec3} {p : Foundation.Parabolic.ParabolicPoint → ℝ} {f : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} :
    IsSuitableWeakSolutionIntegrable Ω I q u Du p f → ∀ {z : Foundation.Parabolic.ParabolicPoint} {r ρ : ℝ}, 0 < ρ → 0 < r → r ≤ ρ / 2 → closure (Foundation.Parabolic.parabolicCylinder z.1 z.2 ρ) ⊆ spaceTimeSet Ω I → pressureD p z r ≤ theoremALin34Constant q * ((ρ / r) ^ 2 * pressureChat u z ρ + r / ρ * pressureD p z ρ + (r / ρ) ^ (3 / 2) * lambda q f z ρ ^ (3 / 2))

    eq:lin35-force of prop:lin34 in the shape consumed by thm:A. For a suitable weak solution, concentric parabolic cylinders with r ≤ ρ/2, and Q_ρ(z₀) contained in the space-time domain, the inner pressure oscillation is bounded by theoremALin34Constant q times the outer velocity oscillation, the outer pressure oscillation and the force term λ(z₀,ρ)^{3/2}. The Calderón--Zygmund bound ext:CZ is not assumed: it is derived from the Liouville decay of ext:newtonian, so no analytic hypothesis remains.