Reanchoring a Hölder representative by velocity averages #
The absolute value of a representative is controlled by averaging its oscillation against the original velocity. No average of the heat potential outside the region of almost-everywhere agreement is required.
theorem
CKN.Core.Endgame.holder_norm_of_seminorm_of_ae_eq
{S T : Set Foundation.Parabolic.ParabolicPoint}
{u w : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3}
{γ K D : ℝ}
(hS : MeasurableSet S)
(hSpos : 0 < MeasureTheory.volume S)
(hStop : MeasureTheory.volume S < ⊤)
(hγ : 0 ≤ γ)
(hK : 0 ≤ K)
(hD : 0 ≤ D)
(hdist : ∀ x ∈ T, ∀ y ∈ S, Foundation.Parabolic.parabolicDist x y ≤ D)
(hsemi :
∀ (x y : Foundation.Parabolic.ParabolicPoint),
Foundation.Parabolic.vec3EuclideanNorm (w x - w y) ≤ K * Foundation.Parabolic.parabolicDist x y ^ γ)
(hrep : w =ᵐ[MeasureTheory.volume.restrict S] u)
(hu :
MeasureTheory.IntegrableOn
(fun (x : Foundation.Parabolic.ParabolicPoint) => Foundation.Parabolic.vec3EuclideanNorm (u x)) S
MeasureTheory.volume)
(hu3 :
MeasureTheory.IntegrableOn
(fun (x : Foundation.Parabolic.ParabolicPoint) => Foundation.Parabolic.vec3EuclideanNorm (u x) ^ 3) S
MeasureTheory.volume)
:
ParabolicHolderVecNormLE T w γ
(K * D ^ γ + (⨍ (x : Foundation.Parabolic.ParabolicPoint) in S, Foundation.Parabolic.vec3EuclideanNorm (u x) ^ 3) ^ (1 / 3) + K)
A Hölder seminorm and an L³ average on a positive finite-measure set
control the full norm on any set at bounded distance from it.
theorem
CKN.Core.Endgame.halfCylinder_holder_norm_of_seminorm
{u w : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3}
{γ K : ℝ}
(hγ : 0 ≤ γ)
(hK : 0 ≤ K)
(hsemi :
∀ (x y : Foundation.Parabolic.ParabolicPoint),
Foundation.Parabolic.vec3EuclideanNorm (w x - w y) ≤ K * Foundation.Parabolic.parabolicDist x y ^ γ)
(hrep : w =ᵐ[MeasureTheory.volume.restrict (Foundation.Parabolic.parabolicCylinder 0 0 (1 / 2))] u)
(hu :
MeasureTheory.IntegrableOn
(fun (x : Foundation.Parabolic.ParabolicPoint) => Foundation.Parabolic.vec3EuclideanNorm (u x))
(Foundation.Parabolic.parabolicCylinder 0 0 (1 / 2)) MeasureTheory.volume)
(hu3 :
MeasureTheory.IntegrableOn
(fun (x : Foundation.Parabolic.ParabolicPoint) => Foundation.Parabolic.vec3EuclideanNorm (u x) ^ 3)
(Foundation.Parabolic.parabolicCylinder 0 0 (1 / 2)) MeasureTheory.volume)
:
ParabolicHolderVecNormLE (closure (Foundation.Parabolic.parabolicCylinder 0 0 (1 / 2))) w γ
(2 * K + (⨍ (x : Foundation.Parabolic.ParabolicPoint) in Foundation.Parabolic.parabolicCylinder 0 0 (1 / 2), Foundation.Parabolic.vec3EuclideanNorm (u x) ^ 3) ^ (1 / 3))
Reanchoring on the half-cylinder gives the full closed-cylinder norm
2 K + (average |u|³)^(1/3) from the global seminorm K.
theorem
CKN.Core.Endgame.halfCylinder_reanchored_heat_representative
{u F : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3}
{G : Fin 3 → Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3}
{γ θ₀ θ₁ P : ℝ}
(hγ : 0 < γ)
(hγ1 : γ < 1)
(hθ₀ : 1 / θ₀ = (2 - γ) / 5)
(hθ₁ : 1 / θ₁ = (1 - γ) / 5)
(hP : 1 ≤ P)
(hPθ₀ : P ≤ θ₀)
(hPθ₁ : P ≤ θ₁)
(hF : ∀ (i : Fin 3), AEMeasurable (fun (x : Foundation.Parabolic.ParabolicPoint) => F x i) MeasureTheory.volume)
(hG : ∀ (j i : Fin 3), AEMeasurable (fun (x : Foundation.Parabolic.ParabolicPoint) => G j x i) MeasureTheory.volume)
(hNF :
∀ (i : Fin 3),
(Foundation.Parabolic.Morrey.morreyNorm P θ₀ fun (x : Foundation.Parabolic.ParabolicPoint) => F x i) < ⊤)
(hNG :
∀ (j i : Fin 3),
(Foundation.Parabolic.Morrey.morreyNorm P θ₁ fun (x : Foundation.Parabolic.ParabolicPoint) => G j x i) < ⊤)
(hSupportF : ∀ (i : Fin 3), HasCompactSupport fun (x : Foundation.Parabolic.ParabolicPoint) => F x i)
(hSupportG : ∀ (j i : Fin 3), HasCompactSupport fun (x : Foundation.Parabolic.ParabolicPoint) => G j x i)
(hrep :
u =ᵐ[MeasureTheory.volume.restrict (Foundation.Parabolic.parabolicCylinder 0 0 (1 / 2))]
fun (x : Foundation.Parabolic.ParabolicPoint) (i : Fin 3) =>
HeatPotential.heatPotential (fun (y : Foundation.Parabolic.ParabolicPoint) => F y i)
(fun (j : Fin 3) (y : Foundation.Parabolic.ParabolicPoint) => G j y i) x)
(hu :
MeasureTheory.IntegrableOn
(fun (x : Foundation.Parabolic.ParabolicPoint) => Foundation.Parabolic.vec3EuclideanNorm (u x))
(Foundation.Parabolic.parabolicCylinder 0 0 (1 / 2)) MeasureTheory.volume)
(hu3 :
MeasureTheory.IntegrableOn
(fun (x : Foundation.Parabolic.ParabolicPoint) => Foundation.Parabolic.vec3EuclideanNorm (u x) ^ 3)
(Foundation.Parabolic.parabolicCylinder 0 0 (1 / 2)) MeasureTheory.volume)
:
∃ (w : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3),
w =ᵐ[MeasureTheory.volume.restrict (Foundation.Parabolic.parabolicCylinder 0 0 (1 / 2))] u ∧ ParabolicHolderVecNormLE (closure (Foundation.Parabolic.parabolicCylinder 0 0 (1 / 2))) w γ
(2 * vectorHeatHolderCoefficient F G γ θ₀ θ₁ P + (⨍ (x : Foundation.Parabolic.ParabolicPoint) in Foundation.Parabolic.parabolicCylinder 0 0 (1 / 2), Foundation.Parabolic.vec3EuclideanNorm (u x) ^ 3) ^ (1 / 3))
The heat estimate reanchored entirely inside the velocity cylinder. Its
constant depends on the actual source norms and the velocity L³ average,
not on values of the potential at future times.