Campanato

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

noncomputable def CKN.Core.HeatPotential.heatPotentialShellValue (F : Foundation.Parabolic.ParabolicPoint → ℝ) (G : Fin 3 → Foundation.Parabolic.ParabolicPoint → ℝ) (S : Set Foundation.Parabolic.ParabolicPoint) (w : Foundation.Parabolic.ParabolicPoint) : ℝ

Contribution of scalar and divergence sources restricted to one integration shell.

Equations

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

theorem CKN.Core.HeatPotential.heatPotential_single_kernel_shell_bound {K : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.ParabolicPoint → ℝ} {f : Foundation.Parabolic.ParabolicPoint → ℝ} {S : Set Foundation.Parabolic.ParabolicPoint} {p p' : Foundation.Parabolic.ParabolicPoint} {C : ℝ} : 0 ≤ C → ∀ (hS : MeasurableSet S) (hwi : MeasureTheory.IntegrableOn (fun (v : Foundation.Parabolic.ParabolicPoint) => K p v * f v) S MeasureTheory.volume) (hwi' : MeasureTheory.IntegrableOn (fun (v : Foundation.Parabolic.ParabolicPoint) => K p' v * f v) S MeasureTheory.volume) (hmajor : MeasureTheory.IntegrableOn (fun (v : Foundation.Parabolic.ParabolicPoint) => C * |f v|) S MeasureTheory.volume) (hpoint : ∀ v ∈ S, |K p v - K p' v| ≤ C), |(∫ (v : Foundation.Parabolic.ParabolicPoint) in S, K p v * f v) - ∫ (v : Foundation.Parabolic.ParabolicPoint) in S, K p' v * f v| ≤ C * ∫ (v : Foundation.Parabolic.ParabolicPoint) in S, |f v|

theorem CKN.Core.HeatPotential.heatPotential_campanato_bound_of_pairwise {h : Foundation.Parabolic.ParabolicPoint → ℝ} {z : Foundation.Parabolic.ParabolicPoint} {r α K p : ℝ} (hr : 0 < r) : 0 ≤ α → ∀ (hp : 1 ≤ p) (hK : 0 ≤ K) (hint : MeasureTheory.IntegrableOn h (Metric.closedBall z r) MeasureTheory.volume) (hfp : 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) (hpair : ∀ w ∈ Metric.closedBall z r, ∀ w' ∈ Metric.closedBall z r, |h w - h w'| ≤ K * r ^ α), Foundation.Parabolic.ParabolicBallLpOscillation h z r p ≤ K * r ^ α

theorem CKN.Core.HeatPotential.heatPotential_far_shell_bound {γ : ℝ} (hγ : γ < 1) {A : ℕ → ℝ} {C r : ℝ} : 0 ≤ C → 0 ≤ r → ∀ (hA : ∀ (j : ℕ), 0 ≤ A j) (hAj : ∀ (j : ℕ), A j ≤ C * 2 ^ (↑j * (γ - 1)) * r ^ γ), ∑' (j : ℕ), A j ≤ C * (1 - 2 ^ (γ - 1))⁻¹ * r ^ γ

theorem CKN.Core.HeatPotential.heatPotential_near_far_sum_bound {γ : ℝ} (hγ : γ < 1) {Anear : ℝ} {A : ℕ → ℝ} {Cnear Cfar r : ℝ} (hnear : Anear ≤ Cnear * r ^ γ) (hA : ∀ (j : ℕ), 0 ≤ A j) (hfar : ∀ (j : ℕ), A j ≤ Cfar * 2 ^ (↑j * (γ - 1)) * r ^ γ) (hCfar : 0 ≤ Cfar) (hr : 0 ≤ r) : Anear + ∑' (j : ℕ), A j ≤ (Cnear + Cfar * (1 - 2 ^ (γ - 1))⁻¹) * r ^ γ

theorem CKN.Core.HeatPotential.heatPotential_far_shell_sum_from_six {γ : ℝ} (hγ : γ < 1) {A : ℕ → ℝ} {C r : ℝ} (hC : 0 ≤ C) (hr : 0 ≤ r) (hA : ∀ (j : ℕ), 0 ≤ A j) (hAj : ∀ (j : ℕ), A (j + 6) ≤ C * 2 ^ (↑(j + 6) * (γ - 1)) * r ^ γ) : ∑' (j : ℕ), A (j + 6) ≤ C * 2 ^ (6 * (γ - 1)) * (1 - 2 ^ (γ - 1))⁻¹ * r ^ γ

theorem CKN.Core.HeatPotential.heatPotential_campanato_bound {h : Foundation.Parabolic.ParabolicPoint → ℝ} {z : Foundation.Parabolic.ParabolicPoint} {r γ p Cnear Cfar Anear : ℝ} {A : ℕ → ℝ} (hγ0 : 0 ≤ γ) (hγ1 : γ < 1) (hr : 0 < r) (hp : 1 ≤ p) (hCnear : 0 ≤ Cnear) (hCfar : 0 ≤ Cfar) (hint : MeasureTheory.IntegrableOn h (Metric.closedBall z r) MeasureTheory.volume) (hfp : 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) (hnear : Anear ≤ Cnear * r ^ γ) (hA : ∀ (j : ℕ), 0 ≤ A j) (hfar : ∀ (j : ℕ), A j ≤ Cfar * 2 ^ (↑j * (γ - 1)) * r ^ γ) (hpair : ∀ w ∈ Metric.closedBall z r, ∀ w' ∈ Metric.closedBall z r, |h w - h w'| ≤ Anear + ∑' (j : ℕ), A j) : Foundation.Parabolic.ParabolicBallLpOscillation h z r p ≤ (Cnear + Cfar * (1 - 2 ^ (γ - 1))⁻¹) * r ^ γ