Regularity of real paths and dyadic limits

Continuous real paths are determined by almost-everywhere interior equalities and by rational samples. Vanishing dyadic quotients extend to a full one-sided filter for monotone numerators.

theorem BGW.Skorokhod.eqOn_Icc_of_ae_eq_Ioo {a b : ℝ} (hab : a < b) {f g : ℝ → ℝ} (hf : Continuous f) (hg : Continuous g) (h : f =ᵐ[MeasureTheory.volume.restrict (Set.Ioo a b)] g) : Set.EqOn f g (Set.Icc a b)

Continuous real functions agreeing a.e. on an open interval agree on its closure.

theorem BGW.Skorokhod.continuous_eq_iff_rat_toNNReal {f g : NNReal → ℝ} (hf : Continuous f) (hg : Continuous g) : (∀ (t : NNReal), f t = g t) ↔ ∀ (q : ℚ), f (↑q).toNNReal = g (↑q).toNNReal

Equality of two continuous functions is determined by nonnegative rational ages.

theorem BGW.Skorokhod.tendsto_div_zero_of_dyadic {U : ℝ → ℝ} (hU : MonotoneOn U (Set.Ioi 0)) (hU0 : ∀ (ε : ℝ), 0 < ε → 0 ≤ U ε) {b : ℝ} (hb : 0 < b) (hseq : Filter.Tendsto (fun (n : ℕ) => U (b * (1 / 2) ^ n) / (b * (1 / 2) ^ n)) Filter.atTop (nhds 0)) : Filter.Tendsto (fun (ε : ℝ) => U ε / ε) (nhdsWithin 0 (Set.Ioi 0)) (nhds 0)

Vanishing dyadic quotients of a monotone numerator imply full-filter vanishing.