Uniform closed-half-cylinder control from concrete heat sources

Finite numerical bounds on the source Morrey norms control the Hölder seminorm. The original small-data condition controls the velocity average. Together they give a quantitative representative with constants chosen before the solution. Construction of the heat sources is a separate step.

Uniform bounds for heat Hölder coefficients

The scalar coefficient is linear in the source Morrey norms. Factoring its numerical weights and taking absolute values gives a uniform vector bound from finite bounds on the scalar source norms.

noncomputable def CKN.Core.Endgame.heatHolderForceWeight (γ θ₀ P : ℝ) : ℝ

Numerical weight of the scalar heat source in its Hölder coefficient.

Equations

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

noncomputable def CKN.Core.Endgame.heatHolderDivergenceWeight (γ θ₁ P : ℝ) : ℝ

Numerical weight of each differentiated heat source.

Equations

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

theorem CKN.Core.Endgame.heatHolderCoefficient_eq_linear (F : Foundation.Parabolic.ParabolicPoint → ℝ) (G : Fin 3 → Foundation.Parabolic.ParabolicPoint → ℝ) (γ θ₀ θ₁ P : ℝ) : heatHolderCoefficient F G γ θ₀ θ₁ P = heatHolderForceWeight γ θ₀ P * (Foundation.Parabolic.Morrey.morreyNorm P θ₀ F).toReal + heatHolderDivergenceWeight γ θ₁ P * ∑ j : Fin 3, (Foundation.Parabolic.Morrey.morreyNorm P θ₁ (G j)).toReal

The scalar heat Hölder coefficient is linear in the source norm values.

theorem CKN.Core.Endgame.abs_heatHolderCoefficient_le_of_source_bounds (γ θ₀ θ₁ P : ℝ) (KF KG : ENNReal) (hKF : KF < ⊤) (hKG : KG < ⊤) {F : Foundation.Parabolic.ParabolicPoint → ℝ} {G : Fin 3 → Foundation.Parabolic.ParabolicPoint → ℝ} (hF : Foundation.Parabolic.Morrey.morreyNorm P θ₀ F ≤ KF) (hG : ∀ (j : Fin 3), Foundation.Parabolic.Morrey.morreyNorm P θ₁ (G j) ≤ KG) : |heatHolderCoefficient F G γ θ₀ θ₁ P| ≤ |heatHolderForceWeight γ θ₀ P| * KF.toReal + |heatHolderDivergenceWeight γ θ₁ P| * 3 * KG.toReal

Uniform finite source bounds control the absolute scalar coefficient; absolute weights avoid any additional sign assumptions on the exponents.

noncomputable def CKN.Core.Endgame.uniformVectorHeatHolderCoefficient (γ θ₀ θ₁ P : ℝ) (KF KG : ENNReal) : ℝ

A uniform vector Hölder coefficient, expressed only in numerical weights and the bounds on the scalar source norms.

Equations

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

theorem CKN.Core.Endgame.uniformVectorHeatHolderCoefficient_nonneg (γ θ₀ θ₁ P : ℝ) (KF KG : ENNReal) : 0 ≤ uniformVectorHeatHolderCoefficient γ θ₀ θ₁ P KF KG

The uniform coefficient is nonnegative.

theorem CKN.Core.Endgame.vectorHeatHolderCoefficient_le_of_source_bounds (γ θ₀ θ₁ P : ℝ) (KF KG : ENNReal) (hKF : KF < ⊤) (hKG : KG < ⊤) {F : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} {G : Fin 3 → Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} (hF : ∀ (i : Fin 3), (Foundation.Parabolic.Morrey.morreyNorm P θ₀ fun (x : Foundation.Parabolic.ParabolicPoint) => F x i) ≤ KF) (hG : ∀ (j i : Fin 3), (Foundation.Parabolic.Morrey.morreyNorm P θ₁ fun (x : Foundation.Parabolic.ParabolicPoint) => G j x i) ≤ KG) : vectorHeatHolderCoefficient F G γ θ₀ θ₁ P ≤ uniformVectorHeatHolderCoefficient γ θ₀ θ₁ P KF KG

Componentwise finite Morrey bounds give a solution-independent upper bound for the vector heat Hölder coefficient.

noncomputable def CKN.Core.Endgame.uniformHalfCylinderHolderBound (q ε₀ : ℝ) (KF KG : ENNReal) : ℝ

The uniform half-cylinder norm bound determined by the source norm bounds and the small-data threshold.

Equations

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

theorem CKN.Core.Endgame.uniformHalfCylinderHolderBound_nonneg (q ε₀ : ℝ) (KF KG : ENNReal) (hε₀ : 0 ≤ ε₀) : 0 ≤ uniformHalfCylinderHolderBound q ε₀ KF KG

The numerical half-cylinder bound is nonnegative.

theorem CKN.Core.Endgame.uniform_halfCylinder_representative_of_heat_sources (q ε₀ : ℝ) (KF KG : ENNReal) (hq : 5 / 2 < q) (hε₀ : 0 ≤ ε₀) (hKF : KF < ⊤) (hKG : KG < ⊤) {Ω : Set Foundation.Parabolic.Vec3} {I : Set ℝ} {u F : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} {Du : Foundation.Parabolic.ParabolicPoint → Fin 3 → Foundation.Parabolic.Vec3} {p : Foundation.Parabolic.ParabolicPoint → ℝ} {f : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} {G : Fin 3 → Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} (hsol : IsSuitableWeakSolutionIntegrable Ω I q u Du p f) (hdom : closure (Foundation.Parabolic.parabolicCylinder 0 0 1) ⊆ spaceTimeSet Ω I) (hsmall : ∫⁻ (z : Foundation.Parabolic.ParabolicPoint) in Foundation.Parabolic.parabolicCylinder 0 0 1, ENNReal.ofReal (Foundation.Parabolic.vec3EuclideanNorm (u z)) ^ 3 + ENNReal.ofReal |p z| ^ (3 / 2) + ENNReal.ofReal (Foundation.Parabolic.vec3EuclideanNorm (f z)) ^ q ≤ ENNReal.ofReal ε₀) (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 (6 / 5) (stepTheta₀ (stepGamma₀ q)) fun (x : Foundation.Parabolic.ParabolicPoint) => F x i) ≤ KF) (hNG : ∀ (j i : Fin 3), (Foundation.Parabolic.Morrey.morreyNorm (6 / 5) (stepTheta₁ (stepGamma₀ q)) fun (x : Foundation.Parabolic.ParabolicPoint) => G j x i) ≤ KG) (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) : ∃ (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 (stepGamma₀ q) (uniformHalfCylinderHolderBound q ε₀ KF KG) ∧ ∀ z ∈ Foundation.Parabolic.vec3Ball 0 (1 / 2) ×ˢ Set.Ioo (-(1 / 4)) 0, IsRegularPoint Ω I u z

Concrete heat sources with uniform finite Morrey bounds, an a.e. representation on the half-cylinder, and the original small-data hypothesis give the quantitative closed-half-cylinder representative and its interior regular points. All numerical bounds are fixed before the solution.

theorem CKN.Core.Endgame.uniform_halfCylinder_representative_of_paper_source_bounds (q ε₀ : ℝ) (KF KG : ENNReal) (hq : 5 / 2 < q) (hε₀ : 0 ≤ ε₀) (hKF : KF < ⊤) (hKG : KG < ⊤) {Ω : Set Foundation.Parabolic.Vec3} {I : Set ℝ} {u F : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} {Du : Foundation.Parabolic.ParabolicPoint → Fin 3 → Foundation.Parabolic.Vec3} {p : Foundation.Parabolic.ParabolicPoint → ℝ} {f : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} {G : Fin 3 → Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} (hsol : IsSuitableWeakSolutionIntegrable Ω I q u Du p f) (hdom : closure (Foundation.Parabolic.parabolicCylinder 0 0 1) ⊆ spaceTimeSet Ω I) (hsmall : ∫⁻ (z : Foundation.Parabolic.ParabolicPoint) in Foundation.Parabolic.parabolicCylinder 0 0 1, ENNReal.ofReal (Foundation.Parabolic.vec3EuclideanNorm (u z)) ^ 3 + ENNReal.ofReal |p z| ^ (3 / 2) + ENNReal.ofReal (Foundation.Parabolic.vec3EuclideanNorm (f z)) ^ q ≤ ENNReal.ofReal ε₀) (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 (6 / 5) (min q (25 / 9)) fun (x : Foundation.Parabolic.ParabolicPoint) => F x i) ≤ KF) (hNG : ∀ (j i : Fin 3), (Foundation.Parabolic.Morrey.morreyNorm (6 / 5) (25 / 3) fun (x : Foundation.Parabolic.ParabolicPoint) => G j x i) ≤ KG) (hSupportF : ∀ (i : Fin 3), ∀ x ∉ Foundation.Parabolic.parabolicCylinder 0 0 1, F x i = 0) (hSupportG : ∀ (j i : Fin 3), ∀ x ∉ Foundation.Parabolic.parabolicCylinder 0 0 1, G j x i = 0) (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) : ∃ (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 (stepGamma₀ q) (uniformHalfCylinderHolderBound q ε₀ KF KG) ∧ ∀ z ∈ Foundation.Parabolic.vec3Ball 0 (1 / 2) ×ˢ Set.Ioo (-(1 / 4)) 0, IsRegularPoint Ω I u z

Unit-cylinder-supported sources at the paper's exponents give the same uniform closed-half-cylinder norm. Compact support and the heat exponents are derived without increasing the numerical source bounds.