DensePoints

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

A Hölder seminorm is a countable supremum on dense points

On an open set the Hölder seminorm of a continuous function is already determined by pairs of distinct points in a dense subset.

References

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

1. A sequence in a dense subset of an open set

theorem Algsuperdiff.Section5.Support.exists_seq_mem_inter_tendsto {d : ℕ} {U D : Set (HCPolySupport.Vec d)} (hU : IsOpen U) (hD : Dense D) {x : HCPolySupport.Vec d} (hx : x ∈ U) : ∃ (z : ℕ → HCPolySupport.Vec d), (∀ (k : ℕ), z k ∈ U ∩ D) ∧ Filter.Tendsto z Filter.atTop (nhds x)

2. The Hölder seminorm

theorem Algsuperdiff.Section5.Support.holderSeminormOn_eq_iSup_dense {d : ℕ} {E : Type u_1} [NormedAddCommGroup E] {U D : Set (HCPolySupport.Vec d)} (hU : IsOpen U) (hD : Dense D) {alpha : ℝ} {f : HCPolySupport.Vec d → E} (hf : ContinuousOn f U) : holderSeminormOn U alpha f = ⨆ x ∈ U ∩ D, ⨆ z ∈ U ∩ D, ⨆ (_ : x ≠ z), ENNReal.ofReal (‖f x - f z‖ / ‖x - z‖ ^ alpha)

The Hölder seminorm of a function continuous on an open set is already the supremum over pairs of distinct points of a dense subset.