Assembling the pressure-gradient estimate on the origin carrier #

lem:pressure-gradient-morrey produces one measurable weak pressure gradient and estimates it cell by cell. Two independent bounds are available on each doubled source cell: the slice estimate of the selected gradient and the fixed-carrier estimate of the harmonic and annular remainder. On each cell the smaller of the two clipped time integrals may be used, where "clipped" means integrated only over the part of the cell inside the backward carrier, in both space and time, so that the integral is the one produced by the indicator of that carrier.

Finite covers transfer these costs to the two coefficients of the one-sided transfer: the small-cell growth coefficient and the whole-carrier mass. A uniform bound on the covering sums is a genuine quantitative input; finiteness of the local growth coefficients alone does not supply it.

source

noncomputable def CKN.Core.Endgame.theoremAClippedCellCost (R₁ : ℝ) (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) (N : Fin 3 → Foundation.Parabolic.Vec3 → ℝ → ℝ → ℝ → ENNReal) (i : Fin 3) (c : Foundation.Parabolic.ParabolicPoint × { r : ℝ // 0 < r }) :

ENNReal

The smaller of the shared slice cost and the fixed-carrier gauge cost, both integrated only over the clipped backward time window.

Equations

One or more equations did not get rendered due to their size.

Instances For

source

theorem CKN.Core.Endgame.theoremA_integral_le_cover_sum {α : Type u_1} {ι : Type u_2} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {S : Set α} (s : Finset ι) (U : ι → Set α) (F : α → ENNReal) (b : ι → ENNReal) (hcover : S ⊆ ⋃ j ∈ s, U j) (hcell : ∀ j ∈ s, ∫⁻ (x : α) in U j, F x ∂μ ≤ b j) :

∫⁻ (x : α) in S, F x ∂μ ≤ ∑ j ∈ s, b j

Integrals over a finite cover are bounded by the sum of the individual bounds. Overlap costs nothing beyond this sum.

source

The scalar slice clause transfers to one measurable origin gradient. On admissible cells, either the shared majorant or the explicit pressure gauge can pay for its clipped power integral.

source

∃ (Dp : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3), Measurable Dp ∧ (∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict I, ∀ (i : Fin 3), MeasureTheory.LocallyIntegrableOn (fun (y : Foundation.Parabolic.Vec3) => Dp (y, s) i) (Foundation.Parabolic.vec3Ball 0 R₁) MeasureTheory.volume ∧ HasWeakPartialDerivOn (Foundation.Parabolic.vec3Ball 0 R₁) i (fun (y : Vec 3) => p (y, s)) fun (y : Vec 3) => Dp (y, s) i) ∧ (∀ (i : Fin 3), ∀ z ∈ Foundation.Parabolic.parabolicCylinder 0 0 (3 / 4), ∀ (r : ℝ), 0 < r → r ≤ R₁ → ∫⁻ (s : ℝ) in Set.Ioc (z.2 - r ^ 2) z.2 ∩ Set.Ioc (-R₁ ^ 2) 0, MeasureTheory.eLpNorm (fun (y : Foundation.Parabolic.Vec3) => Dp (y, s) i) (ENNReal.ofReal (6 / 5)) (MeasureTheory.volume.restrict (Foundation.Parabolic.vec3Ball z.1 r ∩ Foundation.Parabolic.vec3Ball 0 R₁)) ^ (6 / 5) ≤ A * ENNReal.ofReal (r ^ (5 * (1 - 6 / 5 / min (1 / τ + 8 / 25)⁻¹ q)))) ∧ ∀ (i : Fin 3), ∫⁻ (s : ℝ) in Set.Ioc (-R₁ ^ 2) 0, MeasureTheory.eLpNorm (fun (y : Foundation.Parabolic.Vec3) => Dp (y, s) i) (ENNReal.ofReal (6 / 5)) (MeasureTheory.volume.restrict (Foundation.Parabolic.vec3Ball 0 R₁)) ^ (6 / 5) ≤ B

Uniform finite-cover costs give the two clipped slice budgets on the origin carrier. All numerical constants precede the solution. The only additional analytic input beyond the shared scalar slice clause is the explicit covering-sum bound hCoverBudget; its two parts pay for local cells and for the whole carrier, respectively.

source

theorem CKN.Core.Endgame.theoremA_origin_cell_producer_of_clipped_data {q τ R₀ R₁ : ℝ} {A B KP : ENNReal} (hq : 5 / 2 < q) (hτ : 25 / 3 ≤ τ) (hR₁ : 0 < R₁) (hR₁R₀ : R₁ < R₀) (hR₀ : R₀ < 3 / 4) {Ω : 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} (hsol : IsSuitableWeakSolutionIntegrable Ω I q u Du p f) (hdom : closure (Foundation.Parabolic.parabolicCylinder 0 0 1) ⊆ spaceTimeSet Ω I) (M : Fin 3 → Foundation.Parabolic.Vec3 → ℝ → ℝ → ENNReal) (hdata : (∀ (i : Fin 3) (x : Foundation.Parabolic.Vec3) (r : ℝ), ∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict I, ∃ (g : Foundation.Parabolic.Vec3 → ℝ), MeasureTheory.LocallyIntegrableOn g (Foundation.Parabolic.vec3Ball 0 R₁) MeasureTheory.volume ∧ HasWeakPartialDerivOn (Foundation.Parabolic.vec3Ball 0 R₁) i (fun (y : Vec 3) => p (y, s)) g ∧ MeasureTheory.eLpNorm g (ENNReal.ofReal (6 / 5)) (MeasureTheory.volume.restrict (Foundation.Parabolic.vec3Ball x r ∩ Foundation.Parabolic.vec3Ball 0 R₁)) ≤ M i x r s) ∧ (∀ (i : Fin 3), ∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict I, M i 0 R₁ s ≠ ⊤) ∧ (∀ (i : Fin 3) (T : Set ℝ), IsCompact (closure T) → closure T ⊆ I → MeasureTheory.Integrable (fun (s : ℝ) => (M i 0 R₁ s).toReal) (MeasureTheory.volume.restrict T)) ∧ (∀ (i : Fin 3), ∀ z ∈ Foundation.Parabolic.parabolicCylinder 0 0 (3 / 4), ∀ (r : ℝ), 0 < r → r ≤ R₁ → ∫⁻ (s : ℝ) in Set.Ioc (z.2 - r ^ 2) z.2 ∩ Set.Ioc (-R₁ ^ 2) 0, M i z.1 r s ^ (6 / 5) ≤ A * ENNReal.ofReal (r ^ (5 * (1 - 6 / 5 / min (1 / τ + 8 / 25)⁻¹ q)))) ∧ ∀ (i : Fin 3), ∫⁻ (s : ℝ) in Set.Ioc (-R₁ ^ 2) 0, M i 0 R₁ s ^ (6 / 5) ≤ B) (hcompare : oneSidedMorreyBound (6 / 5) (min (1 / τ + 8 / 25)⁻¹ q) R₁ A B ≤ KP) :

The clipped origin construction with an arbitrary final numerical majorant. Selection, integrability and pairing are the same carrier-radius construction; only the last order comparison is parameterized.

Documentation

LeanPool.CaffarelliKohnNirenberg.Core.Endgame.TheoremABudgetBridge

Assembling the pressure-gradient estimate on the origin carrier #