Finite one-sided coverings and total integral estimates

A finite metric-ball cover of the closed intermediate cylinder gives a finite backward-cylinder cover after truncating the forward time shifts. All centers and the number of cylinders are chosen before the integrand.

theorem CKN.Core.Endgame.exists_finite_one_sided_cylinder_cover_on_cylinder (a ρ₀ : ℝ) (ha : 0 < a) (ha34 : a < 3 / 4) (hρ₀ : 0 < ρ₀) : ∃ (s : Finset Foundation.Parabolic.ParabolicPoint), (∀ z ∈ s, z ∈ Foundation.Parabolic.parabolicCylinder 0 0 (3 / 4)) ∧ Foundation.Parabolic.parabolicCylinder 0 0 a ⊆ ⋃ z ∈ s, Foundation.Parabolic.parabolicCylinder z.1 z.2 (ρ₀ / 2)

At every prescribed positive scale, finitely many cylinders of half that radius, with admissible centers, cover the intermediate cylinder. The selected centers depend only on the scale and the fixed geometry.

theorem CKN.Core.Endgame.exists_one_sided_integral_constant_on_cylinder (a ρ₀ : ℝ) (ha : 0 < a) (ha34 : a < 3 / 4) (hρ₀ : 0 < ρ₀) : ∃ (N : ℕ), ∀ (F : Foundation.Parabolic.ParabolicPoint → ENNReal) (B : ENNReal), (∀ z ∈ Foundation.Parabolic.parabolicCylinder 0 0 (3 / 4), ∫⁻ (w : Foundation.Parabolic.ParabolicPoint) in Foundation.Parabolic.parabolicCylinder z.1 z.2 (ρ₀ / 2), F w ≤ B) → ∫⁻ (w : Foundation.Parabolic.ParabolicPoint) in Foundation.Parabolic.parabolicCylinder 0 0 a, F w ≤ ↑N * B

A finite geometric multiplicity turns uniform small-cylinder integral bounds into a total bound on the intermediate cylinder. The integer is chosen before the integrand or its bound, so its dependence is only on the fixed geometry and ρ₀.

theorem CKN.Core.Endgame.exists_one_sided_integral_constant (ρ₀ : ℝ) (hρ₀ : 0 < ρ₀) : ∃ (N : ℕ), ∀ (F : Foundation.Parabolic.ParabolicPoint → ENNReal) (B : ENNReal), (∀ z ∈ Foundation.Parabolic.parabolicCylinder 0 0 (3 / 4), ∫⁻ (w : Foundation.Parabolic.ParabolicPoint) in Foundation.Parabolic.parabolicCylinder z.1 z.2 (ρ₀ / 2), F w ≤ B) → ∫⁻ (w : Foundation.Parabolic.ParabolicPoint) in Foundation.Parabolic.parabolicCylinder 0 0 (5 / 8), F w ≤ ↑N * B

A geometric multiplicity bounds the total integral on the fixed cylinder.