Documentation

LeanPool.CaffarelliKohnNirenberg.Core.Step4.PressureGradientOriginKPHarmonicCells

Pressure Gradient Origin KPHarmonic Cells #

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

source
noncomputable def CKN.Core.Step4.originHarmonicThresholdA (C : ℝ) :
ℝ

An explicit absolute threshold for the harmonic contribution, as a function of the fixed absolute harmonic derivative coefficient.

Equations
Instances For
    source
    theorem CKN.Core.Step4.originHarmonicAbsoluteMomentConstant_lt_top (C : ℝ) :
    originHarmonicAbsoluteMomentConstant C < ⊤

    The harmonic coefficient is finite.

    source
    theorem CKN.Core.Step4.origin_harmonic_coefficient_le_affine_slot (C C_CZ q ε : ℝ) (KU KD : ENNReal) (hC : originHarmonicThresholdA C ≤ C_CZ) :
    ENNReal.ofReal (Real.pi * 4 / 3) * originHarmonicAbsoluteMomentConstant C ^ (4 / 5) * ENNReal.ofReal ε ^ (4 / 5) ≤ originKPAffineASlot q C_CZ ε KU KD

    The absolute threshold pays for the harmonic cell coefficient.

    source
    theorem CKN.Core.Step4.harmonic_volume_radius_bound (C ε κ r : ℝ) (x : Foundation.Parabolic.Vec3) (S : Set Foundation.Parabolic.Vec3) (hr : 0 < r) (hrhi : r ≤ 1) (hκ : 0 < κ) (hκhi : κ ≤ 25 / 9) (hS : S ⊆ Foundation.Parabolic.vec3Ball x r) :
    MeasureTheory.volume S * originHarmonicAbsoluteMomentConstant C ^ (4 / 5) * ENNReal.ofReal ε ^ (4 / 5) * ENNReal.ofReal r ^ (2 / 5) ≤ ENNReal.ofReal (Real.pi * 4 / 3) * originHarmonicAbsoluteMomentConstant C ^ (4 / 5) * ENNReal.ofReal ε ^ (4 / 5) * ENNReal.ofReal (r ^ (5 * (1 - 6 / 5 / κ)))
    source
    theorem CKN.Core.Step4.exists_origin_harmonic_clipped_coefficient_bound_of_sws :
    ∃ (C : ℝ), 0 ≤ C ∧ ∀ (q ε κ ρ R₁ t r : ℝ) (x : Foundation.Parabolic.Vec3) (z : Foundation.Parabolic.ParabolicPoint) (S : Set Foundation.Parabolic.Vec3), 0 < κ → κ ≤ 25 / 9 → ∀ (hρlo : 1 / 8 ≤ ρ), ρ ≤ 1 → 0 < r → r ≤ 1 → MeasurableSet S → S ⊆ Foundation.Parabolic.vec3Ball x r → S ⊆ Foundation.Parabolic.vec3Ball z.1 (ρ / 2) → Set.Ioc (t - r ^ 2) t ∩ Set.Ioc (-R₁ ^ 2) 0 ⊆ Set.Ioc (z.2 - ρ ^ 2) z.2 → ∀ {Ω : Set Foundation.Parabolic.Vec3} {I : Set ℝ} {u f : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} {Du : Foundation.Parabolic.ParabolicPoint → Fin 3 → Foundation.Parabolic.Vec3} {p : Foundation.Parabolic.ParabolicPoint → ℝ}, IsSuitableWeakSolutionIntegrable Ω I q u Du p f → closure (Foundation.Parabolic.parabolicCylinder 0 0 1) ⊆ spaceTimeSet Ω I → closure (Foundation.Parabolic.parabolicCylinder z.1 z.2 ρ) ⊆ spaceTimeSet Ω I → Foundation.Parabolic.parabolicCylinder z.1 z.2 ρ ⊆ Foundation.Parabolic.parabolicCylinder 0 0 1 → ∫⁻ (w : Foundation.Parabolic.ParabolicPoint) in Foundation.Parabolic.parabolicCylinder 0 0 1, ENNReal.ofReal (Foundation.Parabolic.vec3EuclideanNorm (u w)) ^ 3 + ENNReal.ofReal |p w| ^ (3 / 2) + ENNReal.ofReal (Foundation.Parabolic.vec3EuclideanNorm (f w)) ^ q ≤ ENNReal.ofReal ε → ∀ (i : Fin 3), ∫⁻ (s : ℝ) in Set.Ioc (t - r ^ 2) t ∩ Set.Ioc (-R₁ ^ 2) 0, MeasureTheory.eLpNorm (fun (y : Vec 3) => classicalGradient (harmonicPressurePart (mollifiedBallCutoff z.1 ⋯) u (sourceSliceCentredMean z.1 ρ u) p s) y i) (ENNReal.ofReal (6 / 5)) (MeasureTheory.volume.restrict S) ^ (6 / 5) ≤ ENNReal.ofReal (Real.pi * 4 / 3) * originHarmonicAbsoluteMomentConstant C ^ (4 / 5) * ENNReal.ofReal ε ^ (4 / 5) * ENNReal.ofReal (r ^ (5 * (1 - 6 / 5 / κ)))

    The actual harmonic gradient satisfies the affine A-slot estimate on any clipped cell contained in a fixed source collar. All numerical parameters and the absolute harmonic coefficient precede the suitable solution.

    source
    noncomputable def CKN.Core.Step4.originHarmonicAbsoluteCoefficient :
    ℝ

    The harmonic coefficient is selected once from the absolute derivative estimate, before every numerical parameter, carrier and suitable solution.

    Equations
    Instances For
      source
      noncomputable def CKN.Core.Step4.originHarmonicASlotThreshold :
      ℝ

      A fixed real threshold for the harmonic A slot, independent of all solution data, exponents, radii and cells.

      Equations
      Instances For