Quantitative gluing of parabolic Hölder representatives

Representatives equal almost everywhere on overlapping open sets agree pointwise. A common local Hölder bound then gives a quantitative bound on a region whenever sufficiently close pairs lie in a common member of the cover.

theorem CKN.Core.Endgame.holder_norm_mono {U V : Set Foundation.Parabolic.ParabolicPoint} {g : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} {γ C : ℝ} (h : ParabolicHolderVecNormLE U g γ C) (hVU : V ⊆ U) : ParabolicHolderVecNormLE V g γ C

Restriction preserves a quantitative Hölder bound.

theorem CKN.Core.Endgame.holder_on_of_norm {U : Set Foundation.Parabolic.ParabolicPoint} {g : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} {γ C : ℝ} (h : ParabolicHolderVecNormLE U g γ C) : ParabolicHolderVecOn U g γ

Forgetting the numerical bound gives the qualitative Hölder predicate.

theorem CKN.Core.Endgame.holder_on_continuousOn {U : Set Foundation.Parabolic.ParabolicPoint} {g : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} {γ : ℝ} (hγ : 0 < γ) (h : ParabolicHolderVecOn U g γ) : ContinuousOn g U

Positive-exponent parabolic Hölder representatives are continuous.

theorem CKN.Core.Endgame.holder_representatives_eqOn_overlap {U V : Set Foundation.Parabolic.ParabolicPoint} {u g h : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} {γ δ : ℝ} (hU : IsOpen U) (hV : IsOpen V) (hγ : 0 < γ) (hδ : 0 < δ) (hg : ParabolicHolderVecOn U g γ) (hh : ParabolicHolderVecOn V h δ) (hgu : g =ᵐ[MeasureTheory.volume.restrict U] u) (hhu : h =ᵐ[MeasureTheory.volume.restrict V] u) : Set.EqOn g h (U ∩ V)

Almost-everywhere representatives agree at every point of their open overlap.

theorem CKN.Core.Endgame.regular_point_of_holder_on_open {Ω : Set Foundation.Parabolic.Vec3} {I : Set ℝ} {U : Set Foundation.Parabolic.ParabolicPoint} {u w : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} {z : Foundation.Parabolic.ParabolicPoint} {γ : ℝ} (hU : IsOpen U) (hz : z ∈ U) (hUΩ : U ⊆ spaceTimeSet Ω I) (hγ : 0 < γ) (hγ1 : γ ≤ 1) (hwu : w =ᵐ[MeasureTheory.volume.restrict U] u) (hw : ParabolicHolderVecOn U w γ) : IsRegularPoint Ω I u z

A Hölder representative on an open neighborhood proves regularity there.

theorem CKN.Core.Endgame.regular_point_of_holder_norm {Ω : Set Foundation.Parabolic.Vec3} {I : Set ℝ} {U V : Set Foundation.Parabolic.ParabolicPoint} {u w : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} {z : Foundation.Parabolic.ParabolicPoint} {γ C : ℝ} (hV : IsOpen V) (hz : z ∈ V) (hVU : V ⊆ U) (hVΩ : V ⊆ spaceTimeSet Ω I) (hγ : 0 < γ) (hγ1 : γ ≤ 1) (hwu : w =ᵐ[MeasureTheory.volume.restrict U] u) (hw : ParabolicHolderVecNormLE U w γ C) : IsRegularPoint Ω I u z

Restrict a representative to an open subregion to obtain regular points.

theorem CKN.Core.Endgame.exists_holder_gluing {ι : Type u_1} [Countable ι] (U : ι → Set Foundation.Parabolic.ParabolicPoint) (w : ι → Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) {u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} {γ : ℝ} (hγ : 0 < γ) (hU : ∀ (i : ι), IsOpen (U i)) (hw : ∀ (i : ι), ParabolicHolderVecOn (U i) (w i) γ) (hae : ∀ (i : ι), w i =ᵐ[MeasureTheory.volume.restrict (U i)] u) : ∃ (g : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3), (∀ (i : ι), Set.EqOn g (w i) (U i)) ∧ g =ᵐ[MeasureTheory.volume.restrict (⋃ (i : ι), U i)] u

A countable open cover admits a single representative agreeing with every local positive-exponent Hölder representative pointwise on its domain.

theorem CKN.Core.Endgame.exists_holder_norm_gluing {ι : Type u_1} [Countable ι] (U : ι → Set Foundation.Parabolic.ParabolicPoint) (w : ι → Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) {u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} {V : Set Foundation.Parabolic.ParabolicPoint} {γ C δ : ℝ} (hγ : 0 < γ) (hC : 0 ≤ C) (hδ : 0 < δ) (hU : ∀ (i : ι), IsOpen (U i)) (hw : ∀ (i : ι), ParabolicHolderVecNormLE (U i) (w i) γ C) (hae : ∀ (i : ι), w i =ᵐ[MeasureTheory.volume.restrict (U i)] u) (hVU : V ⊆ ⋃ (i : ι), U i) (hclose : ∀ x ∈ V, ∀ y ∈ V, Foundation.Parabolic.parabolicDist x y < δ → ∃ (i : ι), x ∈ U i ∧ y ∈ U i) : ∃ (g : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3), g =ᵐ[MeasureTheory.volume.restrict V] u ∧ ParabolicHolderVecNormLE V g γ (C + max C (2 * C / δ ^ γ)) ∧ ∀ (i : ι), Set.EqOn g (w i) (U i)

Quantitative gluing with a uniform cover radius. The radius hypothesis is pure geometry: every sufficiently close pair in the target region lies in one common cover member. No global representative or global estimate is assumed.