Scaling the actual Laplacian and harmonic interior estimates on R³.

theorem EulerMeanHarmonic.laplacian_comp_const_smul (f : EulerSmoothLimit.Space → ℝ) (hf : ContDiff ℝ (↑⊤) f) (a : ℝ) (x : EulerSmoothLimit.Space) : Laplacian.laplacian (fun (y : EulerSmoothLimit.Space) => f (a • y)) x = a ^ 2 * Laplacian.laplacian f (a • x)

noncomputable def EulerMeanHarmonic.halfScale (f : EulerSmoothLimit.Space → ℝ) : EulerSmoothLimit.Space → ℝ

Half scale, defined pointwise by f ((1/2 : ℝ) • x).

Equations

• EulerMeanHarmonic.halfScale f x = f ((1 / 2) • x)

theorem EulerMeanHarmonic.halfScale_smooth (f : EulerSmoothLimit.Space → ℝ) (hf : ContDiff ℝ (↑⊤) f) : ContDiff ℝ (↑⊤) (halfScale f)

theorem EulerMeanHarmonic.halfScale_memLp (f : EulerSmoothLimit.Space → ℝ) (hf : ContDiff ℝ (↑⊤) f) (hLp : MeasureTheory.MemLp f 2 MeasureTheory.volume) : MeasureTheory.MemLp (halfScale f) 2 MeasureTheory.volume

theorem EulerMeanHarmonic.halfScale_energy (f : EulerSmoothLimit.Space → ℝ) (hf : ContDiff ℝ (↑⊤) f) (hLp : MeasureTheory.MemLp f 2 MeasureTheory.volume) : MeasureTheory.lpNorm (halfScale f) 2 MeasureTheory.volume ^ 2 = 8 * MeasureTheory.lpNorm f 2 MeasureTheory.volume ^ 2

theorem EulerMeanHarmonic.halfScale_harmonic (f : EulerSmoothLimit.Space → ℝ) (hf : ContDiff ℝ (↑⊤) f) (hharmonic : ∀ x ∈ Metric.ball 0 (1 / 2), Laplacian.laplacian f x = 0) (x : EulerSmoothLimit.Space) : x ∈ Metric.ball 0 1 → Laplacian.laplacian (halfScale f) x = 0

noncomputable def EulerMeanHarmonic.harmonicQuarterBallConstant : ℝ

Harmonic quarter ball constant, given by 8 * harmonicInteriorConstant ^ 2.

Equations

• EulerMeanHarmonic.harmonicQuarterBallConstant = 8 * EulerMeanHarmonic.harmonicInteriorConstant ^ 2

theorem EulerMeanHarmonic.harmonicQuarterBallConstant_nonneg : 0 ≤ harmonicQuarterBallConstant

theorem EulerMeanHarmonic.harmonic_pointwise_quarterBall_sq (f : EulerSmoothLimit.Space → ℝ) (hf : ContDiff ℝ (↑⊤) f) (hLp : MeasureTheory.MemLp f 2 MeasureTheory.volume) (hharmonic : ∀ x ∈ Metric.ball 0 (1 / 2), Laplacian.laplacian f x = 0) (x : EulerSmoothLimit.Space) (hx : x ∈ Metric.closedBall 0 (1 / 4)) : f x ^ 2 ≤ harmonicQuarterBallConstant * MeasureTheory.lpNorm f 2 MeasureTheory.volume ^ 2

A squared pointwise bound with room for a compact mollifier near the boundary.