Quantitative vector representatives of heat potentials

The scalar heat estimate is applied to each coordinate. Both the local value bound and the global Hölder constant remain explicit functions of the source norms and the local averages of the potential.

noncomputable def CKN.Core.Endgame.heatHolderCoefficient (F : Foundation.Parabolic.ParabolicPoint → ℝ) (G : Fin 3 → Foundation.Parabolic.ParabolicPoint → ℝ) (γ θ₀ θ₁ P : ℝ) : ℝ

The explicit scalar Hölder coefficient in the heat-potential estimate.

Equations

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

noncomputable def CKN.Core.Endgame.vectorHeatHolderCoefficient (F : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) (G : Fin 3 → Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) (γ θ₀ θ₁ P : ℝ) : ℝ

The sum of the absolute scalar Hölder coefficients.

Equations

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

noncomputable def CKN.Core.Endgame.vectorHeatValueBound (F : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) (G : Fin 3 → Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) (γ θ₀ θ₁ P : ℝ) (z : Foundation.Parabolic.ParabolicPoint) (R : ℝ) : ℝ

An explicit bound for the vector potential on a ball.

Equations

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

theorem CKN.Core.Endgame.vector_heat_representative_and_seminorm_of_morrey {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) : ∃ (v : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3), (v =ᵐ[MeasureTheory.volume] 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) ∧ (∀ (x y : Foundation.Parabolic.ParabolicPoint), Foundation.Parabolic.vec3EuclideanNorm (v x - v y) ≤ vectorHeatHolderCoefficient F G γ θ₀ θ₁ P * Foundation.Parabolic.parabolicDist x y ^ γ) ∧ ∀ (z : Foundation.Parabolic.ParabolicPoint) (R : ℝ), 0 < R → ParabolicHolderVecNormLE (Metric.ball z R) v γ (vectorHeatValueBound F G γ θ₀ θ₁ P z R + vectorHeatHolderCoefficient F G γ θ₀ θ₁ P)

Compactly supported Morrey sources have a common vector representative, with an explicit local norm on every parabolic ball.

theorem CKN.Core.Endgame.vector_heat_representative_of_morrey {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) : ∃ (v : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3), (v =ᵐ[MeasureTheory.volume] 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) ∧ ∀ (z : Foundation.Parabolic.ParabolicPoint) (R : ℝ), 0 < R → ParabolicHolderVecNormLE (Metric.ball z R) v γ (vectorHeatValueBound F G γ θ₀ θ₁ P z R + vectorHeatHolderCoefficient F G γ θ₀ θ₁ P)

The local norm estimate, without separately retaining the global seminorm.