Epsilon regularity at a top face

This file proves the one-sided Hölder estimate of lem:thmA-top from the rescaled form of CKN Theorem A.

def ESS.goodPointTopCenter (x₀ : CKN.Foundation.Parabolic.Vec3) (r : ℝ) : Set CKN.Foundation.Parabolic.ParabolicPoint

Centers for the top-time patches, with spatial and positive-time offsets bounded by r.

Equations

• ESS.goodPointTopCenter x₀ r = {c : CKN.Foundation.Parabolic.ParabolicPoint | c.1 ∈ CKN.Foundation.Parabolic.vec3Ball x₀ (r / 2) ∧ c.2 ∈ Set.Ioo 0 (r ^ 2 / 4)}

def ESS.goodPointTopPatch (t₀ r : ℝ) (c : CKN.Foundation.Parabolic.ParabolicPoint) : Set CKN.Foundation.Parabolic.ParabolicPoint

The backward parabolic cylinder used as the patch based at c.

Equations

• ESS.goodPointTopPatch t₀ r c = ESS.goodPointPastCylinder c.1 (t₀ - c.2) (r / 4)

noncomputable def ESS.goodPointTopLocalHolderBound (C₄ r γ : ℝ) : ℝ

The local Hölder seminorm bound at scale r/2 with constant C₄.

Equations

• ESS.goodPointTopLocalHolderBound C₄ r γ = C₄ * ((r / 2)⁻¹ * (r / 2)⁻¹ ^ γ)

noncomputable def ESS.goodPointTopHolderBound (C₄ r γ : ℝ) : ℝ

A uniform Hölder bound obtained by enlarging the local bound to scale r.

Equations

• ESS.goodPointTopHolderBound C₄ r γ = 4 * C₄ * r⁻¹ * (8 * r⁻¹) ^ γ

theorem ESS.epsilonRegularityL3_top : ∃ (ε₀ : ℝ) (γ₀ : ℝ) (C₄ : ℝ), 0 < ε₀ ∧ 0 < γ₀ ∧ γ₀ ≤ 2 / 3 ∧ 0 ≤ C₄ ∧ ∀ (x₀ : CKN.Foundation.Parabolic.Vec3) (t₀ ρ r : ℝ) (u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (Du : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → CKN.Foundation.Parabolic.Vec3) (p : CKN.Foundation.Parabolic.ParabolicPoint → ℝ), 0 < r → r < ρ → (CKN.IsSuitableWeakSolution (CKN.Foundation.Parabolic.vec3Ball x₀ ρ) (Set.Ioo (t₀ - ρ ^ 2) t₀) 3 u Du p fun (x : CKN.Foundation.Parabolic.ParabolicPoint) => 0) → ENNReal.ofReal (r⁻¹ ^ 2) * goodPointEnergy u p x₀ t₀ r < ENNReal.ofReal (ε₀ / 8) → ∃ (w : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3), w =ᵐ[MeasureTheory.volume.restrict (goodPointPastCylinder x₀ t₀ (r / 2))] u ∧ (∀ z ∈ closure (goodPointPastCylinder x₀ t₀ (r / 2)), CKN.Foundation.Parabolic.vec3EuclideanNorm (w z) ≤ 2 * C₄ * r⁻¹) ∧ ∀ z ∈ closure (goodPointPastCylinder x₀ t₀ (r / 2)), ∀ z' ∈ closure (goodPointPastCylinder x₀ t₀ (r / 2)), CKN.Foundation.Parabolic.vec3EuclideanNorm (w z - w z') ≤ goodPointTopHolderBound C₄ r γ₀ * CKN.Foundation.Parabolic.parabolicDist z z' ^ γ₀

Theorem A yields a Hölder representative up to the top face, as in lem:thmA-top.