Modulus of continuity

DefinitionModulus of continuity#✓fully proved

For a function \(f : \mathbb{R} \to \mathbb{R}\), real numbers \(a\) and \(b\), and a scale \(\eta \in \mathbb{R}\), the modulus of continuity of \(f\) on \([a, b]\) at scale \(\eta\) is

\[\omega_f(\eta) = \sup \{|f(x) - f(y)| : x, y \in [a, b],\ |x - y| \le \eta\},\]

where the supremum is taken in \(\mathbb{R}\) with the convention that it is \(0\) when the set is empty or not bounded above.

noncomputable def modulusOfContinuity (f : ℝ → ℝ) (a b η : ℝ) : ℝ :=
  sSup {|f x - f y| | (x ∈ Set.Icc a b) (y ∈ Set.Icc a b) (_ : |x - y| ≤ η)}

Used by 4

Used byThe modulus of continuity bounds increments · Monotonicity of the modulus of continuity · Nonnegativity of the modulus of continuity · Theorem I (Modulus of continuity vanishes)

TheoremThe set defining the modulus of continuity is bounded above#✓fully proved

Let \(f : \mathbb{R} \to \mathbb{R}\) be continuous on \([a, b]\). Then for every \(\eta \in \mathbb{R}\) the set \(\{|f(x) - f(y)| : x, y \in [a, b],\ |x - y| \le \eta\}\) is bounded above.

theorem modulusOfContinuity_bddAbove (f : ℝ → ℝ) (a b η : ℝ)
    (hf : ContinuousOn f (Set.Icc a b)) :
    BddAbove {|f x - f y| | (x ∈ Set.Icc a b) (y ∈ Set.Icc a b) (_ : |x - y| ≤ η)}

Used by 3

Used byThe modulus of continuity bounds increments · Monotonicity of the modulus of continuity · Nonnegativity of the modulus of continuity

TheoremThe modulus of continuity bounds increments#✓fully proved

Let \(f : \mathbb{R} \to \mathbb{R}\) be continuous on \([a, b]\), let \(\eta \in \mathbb{R}\), and let \(\omega_f(\eta)\) be the modulus of continuity of \(f\) on \([a, b]\) at scale \(\eta\). For all \(x, y \in [a, b]\) with \(|x - y| \le \eta\), we have \(|f(x) - f(y)| \le \omega_f(\eta)\).

theorem le_modulusOfContinuity (f : ℝ → ℝ) (a b : ℝ) (η : ℝ)
    (hf : ContinuousOn f (Set.Icc a b))
    {x : ℝ} (hx : x ∈ Set.Icc a b) {y : ℝ} (hy : y ∈ Set.Icc a b) (hxy : |x - y| ≤ η) :
    |f x - f y| ≤ modulusOfContinuity f a b η

Uses 2

Statement usesModulus of continuity

Proof usesThe set defining the modulus of continuity is bounded above

TheoremNonnegativity of the modulus of continuity#✓fully proved

Let \(a \le b\) and let \(f : \mathbb{R} \to \mathbb{R}\) be continuous on \([a, b]\). For every \(\eta \ge 0\), the modulus of continuity \(\omega_f(\eta)\) of \(f\) on \([a, b]\) at scale \(\eta\) satisfies \(0 \le \omega_f(\eta)\).

The defining set contains \(|f(a) - f(a)| = 0\).

theorem modulusOfContinuity_nonneg (f : ℝ → ℝ) (a b : ℝ) (hab : a ≤ b)
    (hf : ContinuousOn f (Set.Icc a b)) {η : ℝ} (hη : 0 ≤ η) :
    0 ≤ modulusOfContinuity f a b η

Uses 2 · Used by 1

Statement usesModulus of continuity

Proof usesThe set defining the modulus of continuity is bounded above

Used byTheorem I (Modulus of continuity vanishes)

TheoremMonotonicity of the modulus of continuity#✓fully proved

Let \(a \le b\), let \(f : \mathbb{R} \to \mathbb{R}\) be continuous on \([a, b]\), and write \(\omega_f(\eta)\) for the modulus of continuity of \(f\) on \([a, b]\) at scale \(\eta\). If \(0 \le \eta_1 \le \eta_2\), then \(\omega_f(\eta_1) \le \omega_f(\eta_2)\).

A smaller scale takes the supremum over a smaller set of pairs.

theorem modulusOfContinuity_mono (f : ℝ → ℝ) (a b : ℝ) (hab : a ≤ b)
    (hf : ContinuousOn f (Set.Icc a b)) {η₁ η₂ : ℝ} (hη₁ : 0 ≤ η₁) (h : η₁ ≤ η₂) :
    modulusOfContinuity f a b η₁ ≤ modulusOfContinuity f a b η₂

Uses 2

Statement usesModulus of continuity

Proof usesThe set defining the modulus of continuity is bounded above

TheoremTheorem I (Modulus of continuity vanishes)#✓fully proved

Let \(a \le b\) and let \(f : \mathbb{R} \to \mathbb{R}\) be continuous on \([a, b]\). Then the modulus of continuity \(\omega_f(\eta)\) of \(f\) on \([a, b]\) tends to \(0\) as \(\eta \to 0^+\).

theorem modulusOfContinuity_tendsto_zero (f : ℝ → ℝ) (a b : ℝ) (hab : a ≤ b)
    (hf : ContinuousOn f (Set.Icc a b)) :
    Filter.Tendsto (modulusOfContinuity f a b) (𝓝[>] 0) (𝓝 0)

Uses 2

Statement usesModulus of continuity

Proof usesNonnegativity of the modulus of continuity

6 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.