The near-force remainder on a margin cell of `prop:bootstrap` #

The spatial pressure gradient of prop:bootstrap splits, about each centre of the origin carrier, into a Riesz part driven by the localized divergence source and a remainder: the gradient of the harmonic pressure part plus the far-force potential. This file bounds the clipped-cell time integral of the 6/5 power of the remainder's spatial L^{6/5} slice norm by the affine A slot originKPAffineASlot, on every margin cell — centre in the closure of the carrier of radius R₁, radius at most (1 - R₁)/4 — above one absolute Calderón–Zygmund threshold.

The collar on which the remainder is estimated is fixed, of radius ρ = (1 - R₁)/2, never proportional to the cell radius: the pointwise derivative estimate for the harmonic part costs ρ⁻⁴, so a collar proportional to r would leave a negative power of r. With a fixed collar the cell contributes its own volume (4π/3) r³ and the clipped time window contributes r² through two Hölder steps, one in space against the collar and one in time against the window. The resulting powers are r^{17/5} for the energy and pressure contributions and r^{5 - 12/(5q)} for the force contribution, both above the growth exponent θ = 5(1 - (6/5)/min ((1/τ + 8/25)⁻¹) q) ≤ 71/25.

The two data powers produced are ε^{4/5} and ε^{6/(5q)}, which are exactly the sizes of the slot's pressure-mass term c·128·ε^{4/5} and of the 6/5 power of its source term (c·3X)^{6/5} ≥ (3c)^{6/5}·ε^{6/(5q)}. No additive absolute constant survives, so the estimate is compatible with a vanishing slot at vanishing data.

Hölder below exponent one and its slice-then-time form #

This module records two measure-theoretic inequalities in ℝ≥0∞ that feed the A-slot pressure-gradient estimate.

originASlot_lintegral_rpow_le is Hölder's inequality for a single exponent t with 0 < t < 1: it compares the t-power integral with the full integral times a power of the total mass.
originASlot_slice_time_rpow_bound combines a spatial Hölder step with a temporal one: it controls the 6/5-power of the space integral, integrated in time, by the product-measure integral of the c-power of the integrand, with the exponents dictated by the two applications of the first inequality.

source

theorem CKN.Core.Step4.originASlot_lintegral_rpow_le {α : Type u_1} [MeasurableSpace α] (μ : MeasureTheory.Measure α) {g : α → ENNReal} (hg : AEMeasurable g μ) {t : ℝ} (ht0 : 0 < t) (ht1 : t < 1) :

∫⁻ (y : α), g y ^ t ∂μ ≤ μ Set.univ ^ (1 - t) * (∫⁻ (y : α), g y ∂μ) ^ t

Hölder's inequality for an exponent t strictly between zero and one: the integral of g ^ t is bounded by a power of the total mass times the t-power of the integral of g.

source

theorem CKN.Core.Step4.originASlot_slice_time_rpow_bound {B : Set Foundation.Parabolic.Vec3} {W : Set ℝ} {G : Foundation.Parabolic.Vec3 × ℝ → ENNReal} (hG : AEMeasurable G ((MeasureTheory.volume.restrict B).prod (MeasureTheory.volume.restrict W))) {a c : ℝ} (ha : 0 < a) (hac : 6 * a < 5 * c) :

∫⁻ (s : ℝ) in W, (∫⁻ (y : Foundation.Parabolic.Vec3) in B, G (y, s) ^ a) ^ (6 / 5) ≤ MeasureTheory.volume B ^ (6 / 5 * (1 - a / c)) * MeasureTheory.volume W ^ (1 - 6 * a / (5 * c)) * (∫⁻ (w : Foundation.Parabolic.Vec3 × ℝ) in B ×ˢ W, G w ^ c) ^ (6 * a / (5 * c))

The slice-then-time Hölder bound: the 6/5-power of the spatial integral of G ^ a, integrated over the time window, is bounded by powers of the spatial and temporal volumes times the 6a/(5c)-power of the product-measure integral of G ^ c.

Exponent and volume arithmetic #

source

theorem CKN.Core.Step4.harmonicRemainder_theta_le_force {q τ : ℝ} (hq : 5 / 2 < q) (hτ : 25 / 3 ≤ τ) :

5 * (1 - 6 / 5 / min (1 / τ + 8 / 25)⁻¹ q) ≤ 5 - 12 / (5 * q)

The growth exponent of prop:bootstrap never exceeds 5 - 12/(5q).

source

theorem CKN.Core.Step4.harmonicRemainder_volume_ball_le_one {x : Foundation.Parabolic.Vec3} {ρ : ℝ} (hρhi : ρ ≤ 1 / 2) :

MeasureTheory.volume (Foundation.Parabolic.vec3Ball x ρ) ≤ 1

The spatial volume of a ball of radius at most 1/2 is at most one.

source

theorem CKN.Core.Step4.harmonicRemainder_one_le_volume_unit :

1 ≤ MeasureTheory.volume (Foundation.Parabolic.parabolicCylinder 0 0 1)

The unit cylinder has volume at least one.

The two data powers against the affine slot #

source

theorem CKN.Core.Step4.harmonicRemainder_data_power_le_forceSource {q ε : ℝ} (hq : 5 / 2 < q) :

ENNReal.ofReal ε ^ (1 / q) ≤ Endgame.forceSourceMorreyBound q ε

The force-source bound of the unit data size dominates the plain data power ε^{1/q}, because the unit cylinder has volume at least one.

source

theorem CKN.Core.Step4.harmonicRemainder_two_terms_le_originKPAffineASlot (q C_CZ ε : ℝ) (KU KD : ENNReal) (hq : 5 / 2 < q) :

(3 * ENNReal.ofReal (|C_CZ| + 1)) ^ (6 / 5) * ENNReal.ofReal ε ^ (6 / (5 * q)) + ENNReal.ofReal (|C_CZ| + 1) * 128 * ENNReal.ofReal ε ^ (4 / 5) ≤ originKPAffineASlot q C_CZ ε KU KD

The remainder's two data powers are paid by two of the three terms of the affine A slot: the pressure-mass term and the 6/5 power of the source term.

The space-then-time Hölder step in the shape used below #

source

theorem CKN.Core.Step4.harmonicRemainder_time_moment_le {B : Set Foundation.Parabolic.Vec3} {W : Set ℝ} {G : Foundation.Parabolic.Vec3 × ℝ → ENNReal} {a c m : ℝ} {D E : ENNReal} (hG : AEMeasurable G ((MeasureTheory.volume.restrict B).prod (MeasureTheory.volume.restrict W))) (ha : 0 < a) (hac : 6 * a < 5 * c) (hm : m = 6 * a / (5 * c)) (hB : MeasureTheory.volume B ≤ 1) (hW : MeasureTheory.volume W ≤ D) (hD : ∫⁻ (w : Foundation.Parabolic.Vec3 × ℝ) in B ×ˢ W, G w ^ c ≤ E) :

∫⁻ (s : ℝ) in W, (∫⁻ (y : Foundation.Parabolic.Vec3) in B, G (y, s) ^ a) ^ (6 / 5) ≤ D ^ (1 - m) * E ^ m

One slice-then-time Hölder estimate in the form used on a margin cell: a collar of volume at most one, a time window of measure at most D, and a space-time mass at most E give the 6/5 time moment of the slice masses of the a-th power with the single data power E^{6a/(5c)}.