Campanato Holder

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

noncomputable def CKN.Foundation.Parabolic.ParabolicBallLpOscillation (f : ParabolicPoint → ℝ) (z : ParabolicPoint) (r p : ℝ) : ℝ

Normalized Lᵖ oscillation about the mean on a closed parabolic ball.

Equations

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

def CKN.Foundation.Parabolic.ParabolicBallCampanatoBoundOn (f : ParabolicPoint → ℝ) (U : Set ParabolicPoint) (R α K p : ℝ) : Prop

Uniform Campanato oscillation bound for balls centered in a given set.

Equations

• CKN.Foundation.Parabolic.ParabolicBallCampanatoBoundOn f U R α K p = ∀ z ∈ U, ∀ {r : ℝ}, 0 < r → r ≤ R → CKN.Foundation.Parabolic.ParabolicBallLpOscillation f z r p ≤ K * r ^ α

def CKN.Foundation.Parabolic.GlobalParabolicBallCampanatoBound (f : ParabolicPoint → ℝ) (α K p : ℝ) : Prop

Campanato oscillation bound at every point and positive radius.

Equations

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

def CKN.Foundation.Parabolic.ParabolicBallLpDataOn (f : ParabolicPoint → ℝ) (U : Set ParabolicPoint) (R p : ℝ) : Prop

Local integrability data needed to use ball averages and Lᵖ oscillations.

Equations

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

noncomputable def CKN.Foundation.Parabolic.ParabolicBallMeanSeq (f : ParabolicPoint → ℝ) (R : ℝ) (z : ParabolicPoint) (n : ℕ) : ℝ

Averages over a dyadically shrinking sequence of closed parabolic balls.

Equations

• CKN.Foundation.Parabolic.ParabolicBallMeanSeq f R z n = ⨍ (y : CKN.Foundation.Parabolic.ParabolicPoint) in Metric.closedBall z (R / 2 ^ n), f y

noncomputable def CKN.Foundation.Parabolic.parabolicBallRepresentative (f : ParabolicPoint → ℝ) (R : ℝ) (z : ParabolicPoint) : ℝ

Candidate regular representative obtained as the limit of shrinking-ball averages.

Equations

• CKN.Foundation.Parabolic.parabolicBallRepresentative f R z = Filter.atTop.limUnder (CKN.Foundation.Parabolic.ParabolicBallMeanSeq f R z)

def CKN.Foundation.Parabolic.vec3ClosedBall (x : Vec3) (r : ℝ) : Set Vec3

Closed Euclidean ball in native spatial coordinates.

Equations

• CKN.Foundation.Parabolic.vec3ClosedBall x r = {y : CKN.Foundation.Parabolic.Vec3 | CKN.Foundation.Parabolic.vec3EuclideanNorm (y - x) ≤ r}

def CKN.Foundation.Parabolic.campanatoHolderVec3ScaleLinear (a : ℝ) : Vec3 →ₗ[ℝ] Vec3

Linear spatial dilation used to compute the volumes of scaled balls.

Equations

• CKN.Foundation.Parabolic.campanatoHolderVec3ScaleLinear a = a • LinearMap.id

theorem CKN.Foundation.Parabolic.parabolicBall_volume_ratio_two {z w : ParabolicPoint} {r : ℝ} (hr : 0 < r) : (MeasureTheory.volume (Metric.closedBall z (2 * r))).toReal / (MeasureTheory.volume (Metric.closedBall w r)).toReal = 2 ^ 5

theorem CKN.Foundation.Parabolic.parabolicBall_volume_ratio_le_two {z : ParabolicPoint} {r s : ℝ} (hr : 0 < r) (hs : 0 < s) (hsr : s ≤ 2 * r) : (MeasureTheory.volume (Metric.closedBall z s)).toReal / (MeasureTheory.volume (Metric.closedBall z r)).toReal ≤ 2 ^ 5

theorem CKN.Foundation.Parabolic.parabolicBall_closedBall_pos {z : ParabolicPoint} {r : ℝ} (hr : 0 < r) : 0 < MeasureTheory.volume (Metric.closedBall z r)

theorem CKN.Foundation.Parabolic.parabolicBall_closedBall_top {z : ParabolicPoint} {r : ℝ} (hr : 0 < r) : MeasureTheory.volume (Metric.closedBall z r) < ⊤

theorem CKN.Foundation.Parabolic.parabolicBall_dyadic_pos {R : ℝ} (hR : 0 < R) (n : ℕ) : 0 < R / 2 ^ n

theorem CKN.Foundation.Parabolic.parabolicBall_dyadic_le {R : ℝ} (hR : 0 < R) (n : ℕ) : R / 2 ^ n ≤ R

theorem CKN.Foundation.Parabolic.parabolicBall_dyadic_rpow {R : ℝ} (hR : 0 ≤ R) (α : ℝ) (n : ℕ) : (R / 2 ^ n) ^ α = R ^ α * (2 ^ (-α)) ^ n

theorem CKN.Foundation.Parabolic.abs_setAverage_sub_setAverage_le {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {f : α → ℝ} {A B : Set α} {p D : ℝ} (hBA : B ⊆ A) (hApos : 0 < μ A) (hAtop : μ A < ⊤) (hBpos : 0 < μ B) (hBtop : μ B < ⊤) (hfA : MeasureTheory.IntegrableOn f A μ) (hfpA : MeasureTheory.IntegrableOn (fun (x : α) => |f x - ⨍ (y : α) in A, f y ∂μ| ^ p) A μ) (hp : 1 ≤ p) (hD : (μ A).toReal / (μ B).toReal ≤ D) : |⨍ (x : α) in B, f x ∂μ - ⨍ (x : α) in A, f x ∂μ| ≤ D ^ (1 / p) * (⨍ (x : α) in A, |f x - ⨍ (y : α) in A, f y ∂μ| ^ p ∂μ) ^ (1 / p)

theorem CKN.Foundation.Parabolic.abs_parabolicBallMean_sub_le_of_subset {f : ParabolicPoint → ℝ} {z z' : ParabolicPoint} {r p : ℝ} (hr : 0 < r) (hp : 1 ≤ p) (hsubset : Metric.closedBall z' r ⊆ Metric.closedBall z (2 * r)) (hf : MeasureTheory.IntegrableOn f (Metric.closedBall z (2 * r)) MeasureTheory.volume) (hfp : MeasureTheory.IntegrableOn (fun (q : ParabolicPoint) => |f q - ⨍ (x : ParabolicPoint) in Metric.closedBall z (2 * r), f x| ^ p) (Metric.closedBall z (2 * r)) MeasureTheory.volume) : |(⨍ (x : ParabolicPoint) in Metric.closedBall z' r, f x) - ⨍ (x : ParabolicPoint) in Metric.closedBall z (2 * r), f x| ≤ 2 ^ (5 / p) * (⨍ (x : ParabolicPoint) in Metric.closedBall z (2 * r), |f x - ⨍ (y : ParabolicPoint) in Metric.closedBall z (2 * r), f y| ^ p) ^ (1 / p)

theorem CKN.Foundation.Parabolic.abs_parabolicBallMeanSeq_succ_le {f : ParabolicPoint → ℝ} {U : Set ParabolicPoint} {R α K p D : ℝ} {z : ParabolicPoint} (hR : 0 < R) (hp : 1 ≤ p) (hD : 0 ≤ D) (hcamp : ParabolicBallCampanatoBoundOn f U R α K p) (hz : z ∈ U) (n : ℕ) (hratio : (MeasureTheory.volume (Metric.closedBall z (R / 2 ^ n))).toReal / (MeasureTheory.volume (Metric.closedBall z (R / 2 ^ (n + 1)))).toReal ≤ D) (hf : MeasureTheory.IntegrableOn f (Metric.closedBall z (R / 2 ^ n)) MeasureTheory.volume) (hfp : MeasureTheory.IntegrableOn (fun (q : ParabolicPoint) => |f q - ⨍ (x : ParabolicPoint) in Metric.closedBall z (R / 2 ^ n), f x| ^ p) (Metric.closedBall z (R / 2 ^ n)) MeasureTheory.volume) : |ParabolicBallMeanSeq f R z n - ParabolicBallMeanSeq f R z (n + 1)| ≤ D ^ (1 / p) * (K * (R / 2 ^ n) ^ α)

theorem CKN.Foundation.Parabolic.abs_parabolicBallRepresentative_sub_meanSeq_le {f : ParabolicPoint → ℝ} {R α C : ℝ} {z : ParabolicPoint} (hα : 0 < α) (hstep : ∀ (n : ℕ), dist (ParabolicBallMeanSeq f R z n) (ParabolicBallMeanSeq f R z (n + 1)) ≤ C * (2 ^ (-α)) ^ n) (n : ℕ) : |parabolicBallRepresentative f R z - ParabolicBallMeanSeq f R z n| ≤ parabolicCampanatoTailConstant α * C * (2 ^ (-α)) ^ n

def CKN.Foundation.Parabolic.GlobalParabolicBallLpData (f : ParabolicPoint → ℝ) (p : ℝ) : Prop

Integrability data for ball averages and oscillations at all points and radii.

Equations

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

noncomputable def CKN.Foundation.Parabolic.parabolicCampanatoHolderConstant (α p : ℝ) : ℝ

Explicit coefficient converting a Campanato bound to a Hölder bound.

Equations

• CKN.Foundation.Parabolic.parabolicCampanatoHolderConstant α p = (2 * CKN.Foundation.Parabolic.parabolicCampanatoTailConstant α + 1) * 2 ^ (5 / p) * 8 ^ α

theorem CKN.Foundation.Parabolic.parabolicBallRepresentative_holder_at_scale {f : ParabolicPoint → ℝ} {U : Set ParabolicPoint} {R α K p : ℝ} (hα : 0 < α) (hR : 0 < R) (hp : 1 ≤ p) (hK : 0 ≤ K) (hcamp : ParabolicBallCampanatoBoundOn f U R α K p) (hdata : ParabolicBallLpDataOn f U R p) (z : ParabolicPoint) : z ∈ U → ∀ z' ∈ U, dist z z' < R / 4 → |parabolicBallRepresentative f R z - parabolicBallRepresentative f R z'| ≤ parabolicCampanatoHolderConstant α p * K * parabolicDist z z' ^ α

theorem CKN.Foundation.Parabolic.ae_tendsto_parabolicBallMeanSeq {f : ParabolicPoint → ℝ} {R : ℝ} (hR : 0 < R) (hf : MeasureTheory.LocallyIntegrable f MeasureTheory.volume) : ∀ᵐ (z : ParabolicPoint), Filter.Tendsto (ParabolicBallMeanSeq f R z) Filter.atTop (nhds (f z))

theorem CKN.Foundation.Parabolic.parabolicBallRepresentative_ae_eq {f : ParabolicPoint → ℝ} {R : ℝ} (hlim : ∀ᵐ (z : ParabolicPoint), Filter.Tendsto (ParabolicBallMeanSeq f R z) Filter.atTop (nhds (f z))) : parabolicBallRepresentative f R =ᵐ[MeasureTheory.volume] f

theorem CKN.Foundation.Parabolic.parabolicBallRepresentative_ae_eq_of_locallyIntegrable {f : ParabolicPoint → ℝ} {R : ℝ} (hR : 0 < R) (hf : MeasureTheory.LocallyIntegrable f MeasureTheory.volume) : parabolicBallRepresentative f R =ᵐ[MeasureTheory.volume] f