Subordinated End

Part of the Caffarelli–Kohn–Nirenberg partial regularity proof.

theorem CKN.Core.HeatPotential.heatPotential_series_representation_of_morrey {F : Foundation.Parabolic.ParabolicPoint → ℝ} {G : Fin 3 → Foundation.Parabolic.ParabolicPoint → ℝ} {z q : Foundation.Parabolic.ParabolicPoint} {r P θ₀ θ₁ : ℝ} (hr : 0 < r) (hP : 1 ≤ P) (hPθ₀ : P ≤ θ₀) (hPθ₁ : P ≤ θ₁) (hF : AEMeasurable F MeasureTheory.volume) (hG : ∀ (i : Fin 3), AEMeasurable (G i) MeasureTheory.volume) (hNF : Foundation.Parabolic.Morrey.morreyNorm P θ₀ F < ⊤) (hNG : ∀ (i : Fin 3), Foundation.Parabolic.Morrey.morreyNorm P θ₁ (G i) < ⊤) (hSupportF : HasCompactSupport F) (hSupportG : ∀ (i : Fin 3), HasCompactSupport (G i)) (hδ₀ : 0 < 2 - 5 / θ₀) (hδ₁ : 0 < 1 - 5 / θ₁) (hq : q ∈ Metric.closedBall z r) : heatPotential F G q = heatPotentialShellValue F G (heatPotentialNearSet z r) q + ∑' (j : ℕ), heatPotentialShellValue F G (heatPotentialFarShellSet z r j) q ∧ Summable fun (j : ℕ) => heatPotentialShellValue F G (heatPotentialFarShellSet z r j) q

theorem CKN.Core.HeatPotential.heatPotential_pairwise_oscillation_bound_of_morrey {F : Foundation.Parabolic.ParabolicPoint → ℝ} {G : Fin 3 → Foundation.Parabolic.ParabolicPoint → ℝ} {z p p' : Foundation.Parabolic.ParabolicPoint} {r γ θ₀ θ₁ P : ℝ} (hr : 0 < r) (hγ : 0 < γ) (hγ1 : γ < 1) (hθ₀ : 1 / θ₀ = (2 - γ) / 5) (hθ₁ : 1 / θ₁ = (1 - γ) / 5) (hP : 1 ≤ P) (hPθ₀ : P ≤ θ₀) (hPθ₁ : P ≤ θ₁) (hF : AEMeasurable F MeasureTheory.volume) (hG : ∀ (i : Fin 3), AEMeasurable (G i) MeasureTheory.volume) (hNF : Foundation.Parabolic.Morrey.morreyNorm P θ₀ F < ⊤) (hNG : ∀ (i : Fin 3), Foundation.Parabolic.Morrey.morreyNorm P θ₁ (G i) < ⊤) (hSupportF : HasCompactSupport F) (hSupportG : ∀ (i : Fin 3), HasCompactSupport (G i)) (hp : p ∈ Metric.closedBall z r) (hp' : p' ∈ Metric.closedBall z r) : have V := (MeasureTheory.volume (Foundation.Parabolic.parabolicCylinder 0 0 1)).toReal; have BF := V ^ (1 - 1 / P) * (Foundation.Parabolic.Morrey.morreyNorm P θ₀ F).toReal; have BG := fun (i : Fin 3) => V ^ (1 - 1 / P) * (Foundation.Parabolic.Morrey.morreyNorm P θ₁ (G i)).toReal; have Cnear := 2 * 1000 * 2 ^ (8 - 5 / θ₀) * (1 - 2 ^ (-γ))⁻¹ * 256 ^ γ * BF + ∑ i : Fin 3, 2 * 300000 * 2 ^ (10 - 1 - 5 / θ₁) * (1 - 2 ^ (-γ))⁻¹ * 256 ^ γ * BG i; have A := fun (j : ℕ) => 2 * r * (900000 / (2 ^ (↑j + 4) * r) ^ 4 + 2 * r * (10000000 / (2 ^ (↑j + 4) * r) ^ 5)) * ((2 * (2 ^ (↑(↑j + 6) + 1) * r)) ^ (5 * (1 - 1 / θ₀)) * BF) + ∑ i : Fin 3, 2 * r * (60000000 / (2 ^ (↑j + 4) * r) ^ 5 + 2 * r * (30000000000 / (2 ^ (↑j + 4) * r) ^ 6)) * ((2 * (2 ^ (↑(↑j + 6) + 1) * r)) ^ (5 * (1 - 1 / θ₁)) * BG i); |heatPotential F G p - heatPotential F G p'| ≤ Cnear * r ^ γ + ∑' (j : ℕ), A j

theorem CKN.Core.HeatPotential.heatPotential_aemeasurable_of_sources {F : Foundation.Parabolic.ParabolicPoint → ℝ} {G : Fin 3 → Foundation.Parabolic.ParabolicPoint → ℝ} (hF : AEMeasurable F MeasureTheory.volume) (hG : ∀ (i : Fin 3), AEMeasurable (G i) MeasureTheory.volume) : AEMeasurable (heatPotential F G) MeasureTheory.volume

theorem CKN.Core.HeatPotential.heatPotential_local_data_of_pairwise {h : Foundation.Parabolic.ParabolicPoint → ℝ} {z : Foundation.Parabolic.ParabolicPoint} {r p K : ℝ} (hr : 0 < r) (hp : 1 ≤ p) : 0 ≤ K → ∀ (hAEM : AEMeasurable h MeasureTheory.volume) (hpair : ∀ w ∈ Metric.closedBall z r, ∀ w' ∈ Metric.closedBall z r, |h w - h w'| ≤ K), MeasureTheory.IntegrableOn h (Metric.closedBall z r) MeasureTheory.volume ∧ MeasureTheory.IntegrableOn (fun (q : Foundation.Parabolic.ParabolicPoint) => |h q - ⨍ (x : Foundation.Parabolic.ParabolicPoint) in Metric.closedBall z r, h x| ^ p) (Metric.closedBall z r) MeasureTheory.volume

Explicit subordinated heat potentials

The paper writes the pressure part as a degree-one multiplier applied to the forward heat kernel. The explicit dictionary used here is

• ∂ₖ W₊ is heatPotentialSpatialKernel k;
• σ(D) W₊ is represented by subordinatedHeatPotentialKernel j l m, whose value is -∫ s in Ioi t, ∂ₘ∂ⱼ∂ₗ W(x,s).

Thus the coordinate branch is the kernel already used by heatPotential, while the pressure branch is a finite collection of the explicit kernels K^m_jl. The multiplier symbol itself is not used as an additional assumption.