Oscillation control from small integrals

Let f : ℝ → E be a function into a pseudometric space, S a subset of an interval (a, b), and G an integrable function on (a, b). Suppose that on every subinterval (α, β) some point s' of S ∩ (α, β) has dist (f s) (f s') ^ 2 ≤ ∫_{(α, β)} G for all s ∈ S ∩ (α, β). Since the integral of G over a short interval is small, S is dense in [a, b] and the oscillation of f on S near every point of [a, b] tends to zero. Consequently, when E is complete, f has a limit along S at each point of [a, b], and extends continuously from S to [a, b]. The file proves the density and the vanishing oscillation, which hold in any pseudometric space. This is the step that produces a continuous representative of a function known only almost everywhere, for example for the time-continuity of functions in a Gelfand triple.

Main results

• TauCeti.exists_pos_setIntegral_Ioo_lt: the integral of an integrable function over a short interval is arbitrarily small.
• TauCeti.dense_and_dist_lt_of_oscillation: the density of S and the vanishing oscillation of f on S.

theorem TauCeti.exists_pos_setIntegral_Ioo_lt {a b : ℝ} {g : ℝ → ℝ} (hg : MeasureTheory.IntegrableOn g (Set.Ioo a b) MeasureTheory.volume) (x : ℝ) {η : ℝ} (hη : 0 < η) : ∃ δ > 0, ∫ (r : ℝ) in Set.Ioo (max (x - δ) a) (min (x + δ) b), g r < η

The integral of a function integrable on (a, b) over (a, b) ∩ (x - δ, x + δ) is smaller than any given positive bound once δ is small enough.

theorem TauCeti.dense_and_dist_lt_of_oscillation {E : Type u_1} [PseudoMetricSpace E] {a b : ℝ} {f : ℝ → E} {S : Set ℝ} {G : ℝ → ℝ} (hab : a < b) (hS : S ⊆ Set.Ioo a b) (hG : MeasureTheory.IntegrableOn G (Set.Ioo a b) MeasureTheory.volume) (hosc : ∀ (α β : ℝ), a ≤ α → α < β → β ≤ b → ∃ s' ∈ S ∩ Set.Ioo α β, ∀ s ∈ S ∩ Set.Ioo α β, dist (f s) (f s') ^ 2 ≤ ∫ (r : ℝ) in Set.Ioo α β, G r) : Set.Icc a b ⊆ closure S ∧ ∀ x ∈ Set.Icc a b, ∀ ε > 0, ∃ δ > 0, ∀ s ∈ S, ∀ r ∈ S, dist s x < δ → dist r x < δ → dist (f s) (f r) < ε

Oscillation control along a set. Let a < b, let S ⊆ (a, b), and suppose that on every subinterval (α, β) with a ≤ α < β ≤ b some s' ∈ S ∩ (α, β) satisfies dist (f s) (f s') ^ 2 ≤ ∫_{(α, β)} G for all s ∈ S ∩ (α, β), where G is integrable on (a, b). Then S is dense in [a, b], and for every x ∈ [a, b] the oscillation of f on S near x tends to zero.