Interior Sup Three Quarters

Supporting estimates for the Navier–Stokes development.

theorem CKN.Foundation.Heat.weak_harmonic_interior_sup_three_quarters : ∃ (C₁₇ : ℝ), ∀ (h : Parabolic.Vec3 → ℝ) (x₀ : Parabolic.Vec3) (ρ : ℝ), 0 < ρ → MeasureTheory.MemLp h (ENNReal.ofReal (3 / 2)) (MeasureTheory.volume.restrict (euclideanBall x₀ ρ)) → WeaklyHarmonicOn (euclideanBall x₀ ρ) h → MeasureTheory.eLpNorm h ⊤ (MeasureTheory.volume.restrict (euclideanBall x₀ (3 * ρ / 4))) ≤ ENNReal.ofReal (C₁₇ * (ρ ^ 2)⁻¹ * MeasureTheory.lpNorm h (ENNReal.ofReal (3 / 2)) (MeasureTheory.volume.restrict (euclideanBall x₀ ρ)))

The weakly harmonic supremum estimate on the three-quarter ball.