Start #

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

Route.lean integration contract. The exact local statements exported by this file and consumed by the final route are:

hstart : ∀ z ∈ vec3Ball 0 (3 / 4) ×ˢ Ioc (-(9 / 16 : ℝ)) 0,
  theta κ u Du p z (κ / 4) ≤ η ∧ lambda q f z (κ / 4) ≤ Λ₀

hiteration : ∀ z ∈ vec3Ball 0 (3 / 4) ×ˢ Ioc (-(9 / 16 : ℝ)) 0,
  ∀ r : ℝ, 0 < r → r ≤ κ / 4 →
    max (max (alpha u z r) (beta u Du z r)) (delta p z r ^ (2 : ℕ)) ≤
      M * r ^ (2 / 5 : ℝ)

thmA_scaling_step :
  theta κ (rescaleVelocity μ z₀ u) (rescaleGradient μ z₀ Du)
      (rescalePressure μ z₀ p) ((0 : Vec3), (0 : ℝ)) (1 / 4) ≤ η ∧
    lambda q (rescaleForce μ z₀ f) ((0 : Vec3), (0 : ℝ)) (1 / 4) ≤ Λ₀ →
    theta κ u Du p z₀ (μ / 4) ≤ η ∧ lambda q f z₀ (μ / 4) ≤ Λ₀

The public thmA_start_of_inputs first returns a positive ε₀ chosen from iterationKappa, iterationEta, and iterationLambda₀; after the solution, domain, and initial-data hypotheses are supplied, its only named analytic inputs are hCaccGamma and hLin34, and it returns the displayed hstart.

The endgame input must consume the neighbourhood decay display produced from these two statements: for a centre z₀, a positive r₂, and M ≥ 1, it must use the containment and decay hypotheses at r₂ and return, for every 0 < r₃ < r₂ / 4, an a.e. representative on the parabolic ball of radius r₃ with exponent stepGamma₀ q. It must not bind the closed half-cylinder representative, its uniform C₄ bound, or the full regular-point conclusion as an input. The quantitative gluing and closure extension belong to Route.lean.

The public start theorem chooses ε₀ by exists_theoremA_start_smallness from the numerical conventions. Its named analytic estimates are therefore only hCaccGamma and hLin34; the force and scalar start inequalities are local consequences of that convention choice.

source

z ∈ Foundation.Parabolic.vec3Ball 0 (3 / 4) ×ˢ Set.Ioc (-(9 / 16)) 0 → gamma u z (1 / 4) ^ 3 ≤ 16 * ε₀ ∧ delta p z (1 / 4) ^ 3 ≤ 16 * ε₀ ∧ lambda q f z (1 / 4) ≤ ε₀ ^ (1 / q)

The quarter-cylinder data read directly from eq:thmA-hyp.

The start lemma keeps the two remaining analytic displays visible at its interface. The excess comparison is discharged by the established pressureChat_le_eight_gamma_cube theorem.

source

theorem CKN.thmA_start_of_inputs (q C₂₅ C₂₆ C₂₇ C₂₈ C₃₂ : ℝ) (hq : 5 / 2 < q) (hC₂₇ : 0 < C₂₇) (hC₂₈ : 0 < C₂₈) (hC₂₅ : 0 ≤ C₂₅) (hC₂₆ : 0 ≤ C₂₆) (hC₃₂ : 0 ≤ C₃₂) :

∃ (ε₀ : ℝ), 0 < ε₀ ∧ ∀ {Ω : 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 → closure (Foundation.Parabolic.parabolicCylinder 0 0 1) ⊆ spaceTimeSet Ω I → ∫⁻ (z : Foundation.Parabolic.ParabolicPoint) in Foundation.Parabolic.parabolicCylinder 0 0 1, ENNReal.ofReal (Foundation.Parabolic.vec3EuclideanNorm (u z)) ^ 3 + ENNReal.ofReal |p z| ^ (3 / 2) + ENNReal.ofReal (Foundation.Parabolic.vec3EuclideanNorm (f z)) ^ q ≤ ENNReal.ofReal ε₀ → (∀ {z : Foundation.Parabolic.ParabolicPoint} {r ρ : ℝ}, 0 < ρ → 0 < r → r ≤ ρ / 2 → closure (Foundation.Parabolic.parabolicCylinder z.1 z.2 ρ) ⊆ spaceTimeSet Ω I → alpha u z r + beta u Du z r ≤ C₂₅ * (r / ρ * gamma u z ρ + (r / ρ) ^ (-1) * gamma u z ρ ^ (3 / 2) + (r / ρ) ^ (-1) * delta p z ρ * gamma u z ρ ^ (1 / 2)) + C₂₆ * (r / ρ) ^ (-1 / 2) * gamma u z ρ ^ (1 / 2) * lambda q f z ρ ^ (1 / 2)) → (∀ {z : Foundation.Parabolic.ParabolicPoint} {r ρ : ℝ}, 0 < ρ → 0 < r → r ≤ ρ / 2 → closure (Foundation.Parabolic.parabolicCylinder z.1 z.2 ρ) ⊆ spaceTimeSet Ω I → pressureD p z r ≤ C₃₂ * ((ρ / r) ^ 2 * pressureChat u z ρ + r / ρ * pressureD p z ρ + (r / ρ) ^ (3 / 2) * lambda q f z ρ ^ (3 / 2))) → ∀ z ∈ Foundation.Parabolic.vec3Ball 0 (3 / 4) ×ˢ Set.Ioc (-(9 / 16)) 0, theta (iterationKappa C₂₇) u Du p z (iterationKappa C₂₇ / 4) ≤ iterationEta C₂₇ ∧ lambda q f z (iterationKappa C₂₇ / 4) ≤ iterationLambda₀ C₂₇ C₂₈

The convention-driven form of lem:thmA-start.

The small-data threshold is chosen before the domain and the solution. After that choice, the only named analytic estimates needed by the start step are the gamma-form Caccioppoli estimate and the pressure oscillation estimate.

Documentation

LeanPool.CaffarelliKohnNirenberg.Core.TheoremA.Start

Start #