BallAverageHolder #

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

The Hölder seminorm as a countable supremum of ball averages #

The 1/2-Hölder seminorm of Section 5.1 is a pointwise quantity, so it is attached to a continuous representative and is ⊤ when there is none. Both readings are captured by one countable supremum of difference quotients of ball averages,

  S(f) = sup { |⨍_{B(x,1/(k+1))} f - ⨍_{B(z,1/(k+1))} f| / |x - z|^{1/2} } ,

the supremum running over distinct centres in a countable dense set and over the radii 1/(k+1) for which both balls fit inside the open set.

This module proves one half of the identification: where a continuous representative exists, S is exactly its Hölder seminorm. Averaging the pointwise Hölder bound over a ball gives one inequality — the two balls are translates of each other, so the two averages pair up — and letting the radius shrink at a pair of points of the dense set gives the other.

Main results #

setAverage_ball_sub — the difference of two ball averages as one integral.
abs_setAverage_ball_sub_le — a Hölder bound survives averaging.
ballAverageHolderOn_eq_holderSeminormOn.

References #

ABK26, the localized regularity of Section 5.1.

1. Translating the centre of a ball #

source

theorem Algsuperdiff.Section5.Support.setIntegral_ball_eq_setIntegral_ball_zero {d : ℕ} (f : HCPolySupport.Vec d → ℝ) (x : HCPolySupport.Vec d) (r : ℝ) :

∫ (w : HCPolySupport.Vec d) in Metric.ball x r, f w = ∫ (w : HCPolySupport.Vec d) in Metric.ball 0 r, f (x + w)

source

theorem Algsuperdiff.Section5.Support.mem_ball_zero_iff_add_mem_ball {d : ℕ} {x w : HCPolySupport.Vec d} {r : ℝ} :

w ∈ Metric.ball 0 r ↔ x + w ∈ Metric.ball x r

source

theorem Algsuperdiff.Section5.Support.setAverage_ball_sub {d : ℕ} {f : HCPolySupport.Vec d → ℝ} (hf : MeasureTheory.Integrable f MeasureTheory.volume) (x z : HCPolySupport.Vec d) (r : ℝ) :

(⨍ (w : HCPolySupport.Vec d) in Metric.ball x r, f w) - ⨍ (w : HCPolySupport.Vec d) in Metric.ball z r, f w = (MeasureTheory.volume.real (Metric.ball 0 r))⁻¹ * ∫ (w : HCPolySupport.Vec d) in Metric.ball 0 r, f (x + w) - f (z + w)

The difference of two ball averages of the same radius is one integral over the ball at the origin.

source

theorem Algsuperdiff.Section5.Support.abs_setAverage_ball_sub_le {d : ℕ} {U : Set (HCPolySupport.Vec d)} {f : HCPolySupport.Vec d → ℝ} (hf : MeasureTheory.Integrable f MeasureTheory.volume) {H : ℝ} (hH : Section4.Support.HolderSeminormBoundOn U (1 / 2) H f) {x z : HCPolySupport.Vec d} {r : ℝ} (hr : 0 < r) (hbx : Metric.ball x r ⊆ U) (hbz : Metric.ball z r ⊆ U) :

|(⨍ (w : HCPolySupport.Vec d) in Metric.ball x r, f w) - ⨍ (w : HCPolySupport.Vec d) in Metric.ball z r, f w| ≤ H * ‖x - z‖ ^ (1 / 2)

A Hölder bound survives averaging. Two balls of the same radius are translates of each other, so the difference of the averages pairs the values of f at points a fixed distance apart.