BallAverage

Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.

Averages over balls

The quantities of Section 5.1 are attached to almost-everywhere classes of Sobolev functions, and the only thing known to be measurable in the sample is the integral of the solution over a fixed set. Both gauges are therefore read off the averages

  ⨍_{B(x, 1/(k+1))} u ,     x in a countable dense set,  k : ℕ ,

of which there are countably many. This module collects what those averages need: that open and closed balls agree away from a null set, that the average is continuous in the centre at a fixed radius, that it converges to the value of the function at almost every point (Lebesgue differentiation), and that translating the centre translates the integrand.

Main results

• ball_ae_eq_closedBall, setAverage_ball_eq_closedBall.
• continuous_setIntegral_ball — continuity in the centre.
• ae_tendsto_setAverage_ball — Lebesgue differentiation along 1/(k+1).
• eLpNorm_top_restrict_eq_ballAverageSupNormOn — the L^∞ norm on an open set is the supremum of countably many ball averages.

References

• ABK26, the localized error and regularity quantities of Section 5.1.

1. Open and closed balls

theorem Algsuperdiff.Section5.Support.ball_ae_eq_closedBall {d : ℕ} [NeZero d] (x : HCPolySupport.Vec d) (r : ℝ) : Metric.ball x r =ᵐ[MeasureTheory.volume] Metric.closedBall x r

theorem Algsuperdiff.Section5.Support.setIntegral_ball_eq_closedBall {d : ℕ} [NeZero d] (f : HCPolySupport.Vec d → ℝ) (x : HCPolySupport.Vec d) (r : ℝ) : ∫ (z : HCPolySupport.Vec d) in Metric.ball x r, f z = ∫ (z : HCPolySupport.Vec d) in Metric.closedBall x r, f z

theorem Algsuperdiff.Section5.Support.setAverage_ball_eq_closedBall {d : ℕ} [NeZero d] (f : HCPolySupport.Vec d → ℝ) (x : HCPolySupport.Vec d) (r : ℝ) : ⨍ (z : HCPolySupport.Vec d) in Metric.ball x r, f z = ⨍ (z : HCPolySupport.Vec d) in Metric.closedBall x r, f z

2. Lebesgue differentiation along the radii 1/(k+1)

theorem Algsuperdiff.Section5.Support.tendsto_oneDivSucc_nhdsWithin_pos : Filter.Tendsto (fun (k : ℕ) => 1 / (↑k + 1)) Filter.atTop (nhdsWithin 0 (Set.Ioi 0))

theorem Algsuperdiff.Section5.Support.ae_tendsto_setAverage_ball {d : ℕ} [NeZero d] {f : HCPolySupport.Vec d → ℝ} (hf : MeasureTheory.Integrable f MeasureTheory.volume) : ∀ᵐ (x : HCPolySupport.Vec d), Filter.Tendsto (fun (k : ℕ) => ⨍ (z : HCPolySupport.Vec d) in Metric.ball x (1 / (↑k + 1)), f z) Filter.atTop (nhds (f x))

Lebesgue differentiation along the radii 1/(k+1).

3. Continuity of the average in the centre

theorem Algsuperdiff.Section5.Support.continuous_setIntegral_ball {d : ℕ} [NeZero d] {f : HCPolySupport.Vec d → ℝ} (hf : MeasureTheory.Integrable f MeasureTheory.volume) (r : ℝ) : Continuous fun (x : HCPolySupport.Vec d) => ∫ (z : HCPolySupport.Vec d) in Metric.ball x r, f z

At a fixed radius the integral over a ball is continuous in the centre.

theorem Algsuperdiff.Section5.Support.continuous_setAverage_ball {d : ℕ} [NeZero d] {f : HCPolySupport.Vec d → ℝ} (hf : MeasureTheory.Integrable f MeasureTheory.volume) (r : ℝ) : Continuous fun (x : HCPolySupport.Vec d) => ⨍ (z : HCPolySupport.Vec d) in Metric.ball x r, f z

At a fixed radius the average over a ball is continuous in the centre.

4. The essential supremum as a countable supremum of ball averages

noncomputable def Algsuperdiff.Section5.Support.ballAverageSupNormOn {d : ℕ} (U D : Set (HCPolySupport.Vec d)) (f : HCPolySupport.Vec d → ℝ) : ENNReal

The countable family of ball averages of f: the balls B(x, 1/(k+1)) with x in a set D that fit inside U. With D countable this is a countable supremum.

Equations

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

theorem Algsuperdiff.Section5.Support.le_ballAverageSupNormOn {d : ℕ} {U D : Set (HCPolySupport.Vec d)} {f : HCPolySupport.Vec d → ℝ} {x : HCPolySupport.Vec d} (hx : x ∈ D) (k : ℕ) (hball : Metric.ball x (1 / (↑k + 1)) ⊆ U) : ENNReal.ofReal |⨍ (z : HCPolySupport.Vec d) in Metric.ball x (1 / (↑k + 1)), f z| ≤ ballAverageSupNormOn U D f

theorem Algsuperdiff.Section5.Support.eLpNorm_top_restrict_eq_ballAverageSupNormOn {d : ℕ} [NeZero d] {U D : Set (HCPolySupport.Vec d)} (hU : IsOpen U) (hD : Dense D) {f : HCPolySupport.Vec d → ℝ} (hf : MeasureTheory.IntegrableOn f U MeasureTheory.volume) : MeasureTheory.eLpNorm f ⊤ (MeasureTheory.volume.restrict U) = ballAverageSupNormOn U D f

The L^∞ norm on an open set is the supremum of countably many ball averages. The elementary inequality is that an average never exceeds the essential supremum; the converse is Lebesgue differentiation together with the continuity of the average in the centre, which moves the centre onto the countable set D.