Interior Display Bounds

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

noncomputable def CKN.Foundation.Heat.harmonicInteriorDisplayConstant : ℝ

Common coefficient for the displayed harmonic value, gradient and integral estimates.

Equations

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

theorem CKN.Foundation.Heat.harmonicInteriorDisplayConstant_nonneg : 0 ≤ harmonicInteriorDisplayConstant

theorem CKN.Foundation.Heat.convex_euclideanBall {x₀ : Parabolic.Vec3} {R : ℝ} (hR : 0 < R) : Convex ℝ (euclideanBall x₀ R)

theorem CKN.Foundation.Heat.fderiv_norm_le_three_classicalGradient {f : Parabolic.Vec3 → ℝ} (x : Parabolic.Vec3) : ‖fderiv ℝ f x‖ ≤ 3 * Parabolic.vec3EuclideanNorm (classicalGradient f x)

theorem CKN.Foundation.Heat.euclideanBall_subset_closedBall {x : Parabolic.Vec3} {ε : ℝ} (hε : 0 < ε) : euclideanBall x ε ⊆ Metric.closedBall x ε

theorem CKN.Foundation.Heat.tsupport_spatialDeriv_subset {ψ : Parabolic.Vec3 → ℝ} (i : Fin 3) : tsupport (spatialDeriv ψ i) ⊆ tsupport ψ

theorem CKN.Foundation.Heat.spatialLaplacian_zero_off {ψ : Parabolic.Vec3 → ℝ} {U : Set Parabolic.Vec3} (hψU : tsupport ψ ⊆ U) {x : Parabolic.Vec3} (hx : x ∉ U) : spatialLaplacian ψ x = 0

theorem CKN.Foundation.Heat.local_weak_harmonic {h : Parabolic.Vec3 → ℝ} {U V : Set Parabolic.Vec3} (hVU : V ⊆ U) (hweak : WeaklyHarmonicOn U h) : WeaklyHarmonicOn V h

theorem CKN.Foundation.Heat.local_value_bound {h : Parabolic.Vec3 → ℝ} {x₀ x : Parabolic.Vec3} {ρ : ℝ} (hρ : 0 < ρ) (hx : x ∈ euclideanBall x₀ (3 * ρ / 4)) (hmem : MeasureTheory.MemLp h (ENNReal.ofReal (3 / 2)) (MeasureTheory.volume.restrict (euclideanBall x₀ ρ))) (hweak : WeaklyHarmonicOn (euclideanBall x₀ ρ) h) : ∃ (v : ℝ), |v| ≤ 576 * weakHarmonicInteriorSupConstant * (ρ ^ 2)⁻¹ * MeasureTheory.lpNorm h (ENNReal.ofReal (3 / 2)) (MeasureTheory.volume.restrict (euclideanBall x₀ ρ))

theorem CKN.Foundation.Heat.norm_sub_le_gradient_on_euclideanBall {H : Parabolic.Vec3 → ℝ} {x₀ : Parabolic.Vec3} {R G : ℝ} (hR : 0 < R) (hH : ContDiffOn ℝ (↑1) H (euclideanBall x₀ R)) (hgrad : ∀ x ∈ euclideanBall x₀ R, Parabolic.vec3EuclideanNorm (classicalGradient H x) ≤ G) {x y : Parabolic.Vec3} (hx : x ∈ euclideanBall x₀ R) (hy : y ∈ euclideanBall x₀ R) : |H y - H x| ≤ 3 * G * Parabolic.vec3EuclideanNorm (y - x)

theorem CKN.Foundation.Heat.euclideanBall_eq_vec3Ball_display {x₀ : Parabolic.Vec3} {R : ℝ} (hR : 0 < R) : euclideanBall x₀ R = Parabolic.vec3Ball x₀ R

theorem CKN.Foundation.Heat.set_integral_rpow_bound {f : Parabolic.Vec3 → ℝ} {s : Set Parabolic.Vec3} {S : ℝ} (hf : MeasureTheory.MemLp f (ENNReal.ofReal (3 / 2)) (MeasureTheory.volume.restrict s)) (hsvol : MeasureTheory.volume s ≠ ⊤) (hbound : ∀ᵐ (x : Parabolic.Vec3) ∂MeasureTheory.volume.restrict s, |f x| ≤ S) : ∫ (x : Parabolic.Vec3) in s, |f x| ^ (3 / 2) ≤ (MeasureTheory.volume s).toReal * S ^ (3 / 2)

theorem CKN.Foundation.Heat.plain_display_scaling {r ρ K L A : ℝ} (hr : 0 < r) (hρ : 0 < ρ) (hK : 0 ≤ K) (hL : 0 ≤ L) : (r ^ 2)⁻¹ * (A * r ^ 3 * (K * (ρ ^ 2)⁻¹ * L) ^ (3 / 2)) = A * K ^ (3 / 2) * (r / ρ) * (ρ ^ 2)⁻¹ * L ^ (3 / 2)

theorem CKN.Foundation.Heat.oscillation_display_scaling {r ρ G L A : ℝ} (hr : 0 < r) (hρ : 0 < ρ) (hG : 0 ≤ G) (hL : 0 ≤ L) : (r ^ 2)⁻¹ * (A * r ^ 3 * (6 * G * (ρ ^ 3)⁻¹ * L * r) ^ (3 / 2)) = A * (6 * G) ^ (3 / 2) * (r / ρ) ^ (5 / 2) * (ρ ^ 2)⁻¹ * L ^ (3 / 2)

theorem CKN.Foundation.Heat.euclideanBall_pair_distance_le {x₀ x y : Parabolic.Vec3} {r : ℝ} (hr : 0 < r) (hx : x ∈ euclideanBall x₀ r) (hy : y ∈ euclideanBall x₀ r) : Parabolic.vec3EuclideanNorm (y - x) ≤ 2 * r