BallAverageRepresentative

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

A finite ball-average Hölder gauge produces a continuous representative

The converse half of the identification of the localized regularity. If the countable supremum of difference quotients of ball averages is finite, then the almost-everywhere class has a representative continuous on the open set — so the gauge is ⊤ exactly when no continuous representative exists, which is the reading the infimum convention of the localized regularity asks for.

Three steps. The bound over the countable set of centres extends to all centres, by continuity of the average in the centre, at the price of asking the doubled ball to fit inside the open set. The ball averages then form a Cauchy sequence at every point of the open set: comparing with a nearby point where Lebesgue differentiation applies controls the tail. The limit is Hölder on the open set, hence continuous there, and agrees with the function at every point where Lebesgue differentiation applies, hence almost everywhere.

Main results

• continuousOn_of_holderSeminormBoundOn — a Hölder bound is continuity.
• abs_setAverage_ball_sub_le_toReal — the bound at arbitrary centres.
• ballAverageLimit — the candidate representative.
• exists_continuousOn_of_ballAverageHolderOn_lt_top.

References

• ABK26, the localized regularity of Section 5.1.

1. A Hölder bound is continuity

theorem Algsuperdiff.Section5.Support.continuousOn_of_holderSeminormBoundOn {d : ℕ} {E : Type u_1} [NormedAddCommGroup E] {U : Set (HCPolySupport.Vec d)} {alpha K : ℝ} (hK : 0 ≤ K) (halpha : 0 < alpha) {f : HCPolySupport.Vec d → E} (hf : Section4.Support.HolderSeminormBoundOn U alpha K f) : ContinuousOn f U

2. The gauges do not see the values outside the open set

theorem Algsuperdiff.Section5.Support.ballAverageHolderOn_indicator {d : ℕ} {U D : Set (HCPolySupport.Vec d)} (f : HCPolySupport.Vec d → ℝ) : ballAverageHolderOn U D (U.indicator f) = ballAverageHolderOn U D f

3. The bound at arbitrary centres

theorem Algsuperdiff.Section5.Support.abs_setAverage_ball_sub_le_toReal {d : ℕ} [NeZero d] {U D : Set (HCPolySupport.Vec d)} (hD : Dense D) {f : HCPolySupport.Vec d → ℝ} (hf : MeasureTheory.Integrable f MeasureTheory.volume) (hS : ballAverageHolderOn U D f < ⊤) {p q : HCPolySupport.Vec d} {k : ℕ} (hp : Metric.ball p (2 * (1 / (↑k + 1))) ⊆ U) (hq : Metric.ball q (2 * (1 / (↑k + 1))) ⊆ U) : |(⨍ (w : HCPolySupport.Vec d) in Metric.ball p (1 / (↑k + 1)), f w) - ⨍ (w : HCPolySupport.Vec d) in Metric.ball q (1 / (↑k + 1)), f w| ≤ (ballAverageHolderOn U D f).toReal * ‖p - q‖ ^ (1 / 2)

The difference quotient bound holds at every pair of centres whose doubled balls fit inside the open set, not only at the centres of the countable family: the average is continuous in the centre, and a centre of the countable family within one radius of a given centre has its ball inside the doubled ball.

4. The candidate representative

noncomputable def Algsuperdiff.Section5.Support.ballAverageLimit {d : ℕ} (f : HCPolySupport.Vec d → ℝ) (x : HCPolySupport.Vec d) : ℝ

The limit of the ball averages, where it exists. On an open set where the ball-average Hölder gauge is finite this is a representative continuous there.

Equations

• Algsuperdiff.Section5.Support.ballAverageLimit f x = Filter.atTop.limUnder fun (k : ℕ) => ⨍ (w : HCPolySupport.Vec d) in Metric.ball x (1 / (↑k + 1)), f w

theorem Algsuperdiff.Section5.Support.exists_continuousOn_of_ballAverageHolderOn_lt_top {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) (hS : ballAverageHolderOn U D f < ⊤) : ∃ (g : HCPolySupport.Vec d → ℝ), g =ᵐ[MeasureTheory.volume.restrict U] f ∧ ContinuousOn g U

A finite ball-average Hölder gauge produces a representative continuous on the open set. In particular the gauge is ⊤ whenever no continuous representative exists.