Margin cells for the origin pressure-gradient budget of prop:bootstrap

A clipped cell of the origin carrier may have its centre anywhere, and its radius may exceed the margin (1 - R₁)/4 on which the small-cell estimate of prop:bootstrap is available. Two elementary devices repair both defects.

• A cell clipped to the carrier is contained in a cell of twice the radius whose centre lies in the carrier itself: take the space coordinate of any point of the clipped cell and the smaller of the cell's final time and 0.
• The carrier is covered by finitely many lattice cells of radius (1 - R₁)/16. Since R₁ < 3/4 the lattice indices that can occur lie in one absolute box, so the number of cells used is an absolute constant.

Together they reduce every clipped cell to margin cells centred in the carrier, at the cost of one absolute multiplicative constant.

Growth Exponent Arithmetic

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

theorem CKN.Core.Step4.growth_exponent_lower {q τ : ℝ} (hq : 5 / 2 < q) (hτ : 25 / 3 ≤ τ) : 59 / 25 ≤ 5 * (1 - 6 / 5 / min (1 / τ + 8 / 25)⁻¹ q)

Lower bound 59/25 for the growth exponent when q > 5/2 and τ ≥ 25/3.

theorem CKN.Core.Step4.growth_exponent_pos {q τ : ℝ} (hq : 5 / 2 < q) (hτ : 25 / 3 ≤ τ) : 0 < 5 * (1 - 6 / 5 / min (1 / τ + 8 / 25)⁻¹ q)

Positivity of the growth exponent when q > 5/2 and τ ≥ 25/3.

theorem CKN.Core.Step4.growth_exponent_upper {q τ : ℝ} (hτ : 0 < τ) (hτ' : τ ≤ 25) (hq : 0 < q) : 5 * (1 - 6 / 5 / min (1 / τ + 8 / 25)⁻¹ q) ≤ 71 / 25

Upper bound 71/25 for the growth exponent when 0 < τ ≤ 25 and q > 0.

theorem CKN.Core.Step4.rpow_growth_exponent_mono {q τ r R : ℝ} (hq : 5 / 2 < q) (hτ : 25 / 3 ≤ τ) (hr : 0 ≤ r) (hrR : r ≤ R) : r ^ (5 * (1 - 6 / 5 / min (1 / τ + 8 / 25)⁻¹ q)) ≤ R ^ (5 * (1 - 6 / 5 / min (1 / τ + 8 / 25)⁻¹ q))

Monotonicity of r ^ (growth exponent) in the base when the exponent is positive.

The doubled cell centred in the carrier

noncomputable def CKN.Core.Step4.originASlotShiftedCentre (R : ℝ) (z : Foundation.Parabolic.ParabolicPoint) (r : ℝ) : Foundation.Parabolic.ParabolicPoint

A centre in the carrier for the cell parabolicCylinder z.1 z.2 r clipped to the carrier of radius R: the space coordinate of a point of the clipped cell, and the final time of the cell capped at 0. The default value is the carrier centre, which lies in the carrier whenever R is positive.

Equations

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

theorem CKN.Core.Step4.originASlotShiftedCentre_mem {R : ℝ} (hR : 0 < R) (z : Foundation.Parabolic.ParabolicPoint) (r : ℝ) : originASlotShiftedCentre R z r ∈ Foundation.Parabolic.parabolicCylinder 0 0 R

The shifted centre lies in the carrier.

theorem CKN.Core.Step4.originASlotShiftedCentre_subset {R r : ℝ} (hr : 0 < r) (z : Foundation.Parabolic.ParabolicPoint) : Foundation.Parabolic.parabolicCylinder z.1 z.2 r ∩ Foundation.Parabolic.parabolicCylinder 0 0 R ⊆ Foundation.Parabolic.parabolicCylinder (originASlotShiftedCentre R z r).1 (originASlotShiftedCentre R z r).2 (2 * r)

The clipped cell sits inside the cell of twice the radius about the shifted centre.

The absolute index box of the lattice cover

@[irreducible]

def CKN.Core.Step4.originASlotCoverBox : Finset ((Fin 3 → ℤ) × ℤ)

The lattice indices that a cell of radius (1 - R)/16 can carry while meeting the origin carrier of radius R < 3/4.

Equations

• CKN.Core.Step4.originASlotCoverBox = (Fintype.piFinset fun (x : Fin 3) => Finset.Icc (-98) 98) ×ˢ Finset.Icc (-4608) 2

theorem CKN.Core.Step4.originASlotCoverBox_card : originASlotCoverBox.card = 35252814903

The index box has 197³ · 4611 members.

theorem CKN.Core.Step4.originASlotCoverBox_mem {R a : ℝ} (hR : 0 < R) (hRlt : R < 3 / 4) (ha : a = (1 - R) / 16) {k : (Fin 3 → ℤ) × ℤ} {w : Foundation.Parabolic.ParabolicPoint} (hcell : w ∈ Foundation.Parabolic.parabolicCylinder (originLatticeCentre a k).1 (originLatticeCentre a k).2 a) (hcarrier : w ∈ Foundation.Parabolic.parabolicCylinder 0 0 R) : k ∈ originASlotCoverBox

A lattice cell of radius (1 - R)/16 that meets the carrier of radius R has its index in the absolute box.

theorem CKN.Core.Step4.originASlot_carrier_subset_shifted_cells {R a : ℝ} (hR : 0 < R) (hRlt : R < 3 / 4) (ha : a = (1 - R) / 16) : Foundation.Parabolic.parabolicCylinder 0 0 R ⊆ ⋃ k ∈ originASlotCoverBox, Foundation.Parabolic.parabolicCylinder (originASlotShiftedCentre R (originLatticeCentre a k) a).1 (originASlotShiftedCentre R (originLatticeCentre a k) a).2 (2 * a)

The origin carrier is covered by the doubled margin cells attached to the lattice indices of the absolute box. Every centre used lies in the carrier and every radius used is (1 - R)/8.

Two scale inequalities for the growth exponent

theorem CKN.Core.Step4.originASlot_ofReal_two_mul_rpow_le {q τ r : ℝ} (hq : 5 / 2 < q) (hτ : 25 / 3 ≤ τ) (hτhi : τ ≤ 25) (hr : 0 < r) : ENNReal.ofReal ((2 * r) ^ (5 * (1 - 6 / 5 / min (1 / τ + 8 / 25)⁻¹ q))) ≤ 8 * ENNReal.ofReal (r ^ (5 * (1 - 6 / 5 / min (1 / τ + 8 / 25)⁻¹ q)))

Doubling the radius costs at most the factor 8, because the growth exponent of prop:bootstrap is at most 71/25.

theorem CKN.Core.Step4.originASlot_ofReal_rpow_mono {q τ a r : ℝ} (hq : 5 / 2 < q) (hτ : 25 / 3 ≤ τ) (ha : 0 ≤ a) (har : a ≤ r) : ENNReal.ofReal (a ^ (5 * (1 - 6 / 5 / min (1 / τ + 8 / 25)⁻¹ q))) ≤ ENNReal.ofReal (r ^ (5 * (1 - 6 / 5 / min (1 / τ + 8 / 25)⁻¹ q)))

The growth factor is monotone in the radius.

The Calderón–Zygmund threshold absorbs an absolute factor

theorem CKN.Core.Step4.originKPAffineASlot_const_mul_le {q ε : ℝ} {KU KD n : ENNReal} {C₀ C : ℝ} (hn : 1 ≤ n) (h : n * ENNReal.ofReal (|C₀| + 1) ≤ ENNReal.ofReal (|C| + 1)) : n * originKPAffineASlot q C₀ ε KU KD ≤ originKPAffineASlot q C ε KU KD

The affine slot is superhomogeneous in |C| + 1: an absolute factor n ≥ 1 is absorbed by enlarging the Calderón–Zygmund constant by the factor n.