Rescaled epsilon regularity

This is the radius-r form of CKN Theorem A used in lem:thmA-rescaled.

noncomputable def ESS.goodPointRescaleHomeomorph (x₀ : CKN.Foundation.Parabolic.Vec3) (t₀ r : ℝ) (hr : 0 < r) : CKN.Foundation.Parabolic.ParabolicPoint ≃ₜ CKN.Foundation.Parabolic.ParabolicPoint

The translation and parabolic rescaling homeomorphism centered at the given point.

Equations

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

theorem ESS.epsilonRegularityL3_rescaled (q : ℝ) (hq : 5 / 2 < q) : ∃ (ε₀ : ℝ) (γ₀ : ℝ) (C₄ : ℝ), 0 < ε₀ ∧ 0 < γ₀ ∧ γ₀ ≤ 2 / 3 ∧ 0 ≤ C₄ ∧ ∀ (Ω : Set CKN.Foundation.Parabolic.Vec3) (I : Set ℝ) (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 → ℝ), (CKN.IsSuitableWeakSolution Ω I q u Du p fun (x : CKN.Foundation.Parabolic.ParabolicPoint) => 0) → ∀ (x₀ : CKN.Foundation.Parabolic.Vec3) (t₀ r : ℝ), 0 < r → closure (CKN.Foundation.Parabolic.parabolicCylinder x₀ t₀ r) ⊆ CKN.spaceTimeSet Ω I → goodPointEnergy u p x₀ t₀ r * ENNReal.ofReal (r⁻¹ ^ 2) < ENNReal.ofReal ε₀ → ∃ (w : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3), w =ᵐ[MeasureTheory.volume.restrict (CKN.Foundation.Parabolic.parabolicCylinder x₀ t₀ (r / 2))] u ∧ (∀ z ∈ closure (CKN.Foundation.Parabolic.parabolicCylinder x₀ t₀ (r / 2)), CKN.Foundation.Parabolic.vec3EuclideanNorm (w z) ≤ C₄ * r⁻¹) ∧ ∀ z ∈ closure (CKN.Foundation.Parabolic.parabolicCylinder x₀ t₀ (r / 2)), ∀ z' ∈ closure (CKN.Foundation.Parabolic.parabolicCylinder x₀ t₀ (r / 2)), CKN.Foundation.Parabolic.vec3EuclideanNorm (w z - w z') ≤ C₄ * (r⁻¹ * r⁻¹ ^ γ₀) * CKN.Foundation.Parabolic.parabolicDist z z' ^ γ₀

CKN Theorem A transports from the unit cylinder to every positive radius, with the velocity and pressure normalization used in lem:thmA-rescaled.