Quantitative bootstrap from past-time sources

The global bootstrap is applied to the truncated potential itself. Its agreement with velocity is needed only on the target cylinder. Consequently no bound or representation for the truncated velocity at future times is used.

theorem CKN.Core.Endgame.causal_bootstrap_morrey_le_of_local_representation (KF KG : ENNReal) (hKF : KF < ⊤) (hKG : KG < ⊤) {u F : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} {H : Fin 3 → Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} (hF : ∀ (i : Fin 3), AEMeasurable ({z : Foundation.Parabolic.ParabolicPoint | z.2 ≤ 0}.indicator fun (z : Foundation.Parabolic.ParabolicPoint) => F z i) MeasureTheory.volume) (hH : ∀ (j i : Fin 3), AEMeasurable ({z : Foundation.Parabolic.ParabolicPoint | z.2 ≤ 0}.indicator fun (z : Foundation.Parabolic.ParabolicPoint) => H j z i) MeasureTheory.volume) (hNF : ∀ (i : Fin 3), Foundation.Parabolic.Morrey.morreyNorm (6 / 5) (25 / 11) ({z : Foundation.Parabolic.ParabolicPoint | z.2 ≤ 0}.indicator fun (z : Foundation.Parabolic.ParabolicPoint) => F z i) ≤ KF) (hNH : ∀ (j i : Fin 3), Foundation.Parabolic.Morrey.morreyNorm 3 (25 / 6) ({z : Foundation.Parabolic.ParabolicPoint | z.2 ≤ 0}.indicator fun (z : Foundation.Parabolic.ParabolicPoint) => H j z i) ≤ KG) (hFsupp : ∀ (z : Foundation.Parabolic.ParabolicPoint), z.2 ≤ 0 → z ∉ Foundation.Parabolic.parabolicCylinder 0 0 (21 / 32) → F z = 0) (hHsupp : ∀ (j : Fin 3) (z : Foundation.Parabolic.ParabolicPoint), z.2 ≤ 0 → z ∉ Foundation.Parabolic.parabolicCylinder 0 0 (21 / 32) → H j z = 0) (hrep : u =ᵐ[MeasureTheory.volume.restrict (Foundation.Parabolic.parabolicCylinder 0 0 (5 / 8))] Step4.vectorHeatPotential F H) (i : Fin 3) : Foundation.Parabolic.Morrey.morreyNorm 3 25 ((Foundation.Parabolic.parabolicCylinder 0 0 (5 / 8)).indicator fun (z : Foundation.Parabolic.ParabolicPoint) => u z i) ≤ bootstrapSourceMorreyBound (3 * KF) (3 * KG)

Past component bounds and a local literal heat representation imply the improved velocity bound on the target cylinder.

theorem CKN.Core.Endgame.localizedVelocity_heat_representation_on_plateau {φ : Foundation.Parabolic.ParabolicPoint → ℝ} {u F : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} {H : Fin 3 → Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} {S : Set Foundation.Parabolic.ParabolicPoint} (hS : MeasurableSet S) (hφ : ∀ z ∈ S, φ z = 1) (hrep : Step3.localizedVelocity φ u =ᵐ[MeasureTheory.volume] Step4.vectorHeatPotential F H) : u =ᵐ[MeasureTheory.volume.restrict S] Step4.vectorHeatPotential F H

A global literal representation of the localized velocity supplies the restricted representation required by the causal bootstrap.

theorem CKN.Core.Endgame.causal_bootstrap_morrey_le_of_localized_representation (KF KG : ENNReal) (hKF : KF < ⊤) (hKG : KG < ⊤) {φ : Foundation.Parabolic.ParabolicPoint → ℝ} {u F : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} {H : Fin 3 → Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} (hF : ∀ (i : Fin 3), AEMeasurable ({z : Foundation.Parabolic.ParabolicPoint | z.2 ≤ 0}.indicator fun (z : Foundation.Parabolic.ParabolicPoint) => F z i) MeasureTheory.volume) (hH : ∀ (j i : Fin 3), AEMeasurable ({z : Foundation.Parabolic.ParabolicPoint | z.2 ≤ 0}.indicator fun (z : Foundation.Parabolic.ParabolicPoint) => H j z i) MeasureTheory.volume) (hNF : ∀ (i : Fin 3), Foundation.Parabolic.Morrey.morreyNorm (6 / 5) (25 / 11) ({z : Foundation.Parabolic.ParabolicPoint | z.2 ≤ 0}.indicator fun (z : Foundation.Parabolic.ParabolicPoint) => F z i) ≤ KF) (hNH : ∀ (j i : Fin 3), Foundation.Parabolic.Morrey.morreyNorm 3 (25 / 6) ({z : Foundation.Parabolic.ParabolicPoint | z.2 ≤ 0}.indicator fun (z : Foundation.Parabolic.ParabolicPoint) => H j z i) ≤ KG) (hFsupp : ∀ (z : Foundation.Parabolic.ParabolicPoint), z.2 ≤ 0 → z ∉ Foundation.Parabolic.parabolicCylinder 0 0 (21 / 32) → F z = 0) (hHsupp : ∀ (j : Fin 3) (z : Foundation.Parabolic.ParabolicPoint), z.2 ≤ 0 → z ∉ Foundation.Parabolic.parabolicCylinder 0 0 (21 / 32) → H j z = 0) (hφ : ∀ z ∈ Foundation.Parabolic.parabolicCylinder 0 0 (5 / 8), φ z = 1) (hrep : Step3.localizedVelocity φ u =ᵐ[MeasureTheory.volume] Step4.vectorHeatPotential F H) (i : Fin 3) : Foundation.Parabolic.Morrey.morreyNorm 3 25 ((Foundation.Parabolic.parabolicCylinder 0 0 (5 / 8)).indicator fun (z : Foundation.Parabolic.ParabolicPoint) => u z i) ≤ bootstrapSourceMorreyBound (3 * KF) (3 * KG)

A cutoff plateau and its global literal heat representation give the quantitative improvement using only the past source bounds.