A constructive proof of Simpson’s Rule

by THIERRY COQUAND BAS SPITTERS

In the paper, uniform continuity is discussed.

We define it in a concrete setting here, and prove formally that:

• y = 2x is uniformly continuous on ℝ.
• y = x² is not uniformly continuous on ℝ.
• z = y² - x² is not uniformly continuous on ℝ².
• y = x² is uniformly continuous on [0,1].

def is_limit (a : ℝ) (L : ℝ) (f : ℝ → ℝ) : Prop

Equations

• is_limit a L f = ∀ ε > 0, ∃ δ > 0, ∀ (x : ℝ), 0 < |x - a| ∧ |x - a| < δ → |f x - L| < ε

noncomputable def is_limit_bool (a : ℝ) (f : ℝ → ℝ) (L : ℝ) : Bool

Equations

• is_limit_bool a f L = if is_limit a L f then true else false

def is_uniformly_continuous (f : ℝ → ℝ) : Prop

Equations

• is_uniformly_continuous f = ∀ ε > 0, ∃ δ > 0, ∀ (x y : ℝ), |x - y| < δ → |f x - f y| < ε

def is_uniformly_continuous₂ (f : ℝ × ℝ → ℝ) : Prop

Equations

• is_uniformly_continuous₂ f = ∀ ε > 0, ∃ δ > 0, ∀ (p q : ℝ × ℝ), (p.1 - q.1) ^ 2 + (p.2 - q.2) ^ 2 < δ ^ 2 → |f p - f q| < ε

theorem extraabs (a : ℝ) (h : 0 < a) : 1 ≤ |1 + a|

theorem mul2UniformlyCont : is_uniformly_continuous fun (x : ℝ) => 2 * x

theorem Hδ (δ : ℝ) (hδ : 0 < δ) : 1 ≤ |δ * δ⁻¹ + δ ^ 2 * (1 / 4)|

theorem transition (x : ℝ) (y : ℝ) (ha : 0 ≤ x) (hb : 0 < y) : x < y ↔ x ^ 2 < y ^ 2

theorem SqNotUniformlyCont : ¬is_uniformly_continuous fun (x : ℝ) => x ^ 2

theorem SaddleNotUniformlyCont : ¬is_uniformly_continuous₂ fun (x : ℝ × ℝ) => x.2 ^ 2 - x.1 ^ 2

def is_uniformly_continuous_on (S : Set ℝ) (f : ↑S → ℝ) : Prop

Equations

• is_uniformly_continuous_on S f = ∀ ε > 0, ∃ δ > 0, ∀ (x y : ↑S), |↑x - ↑y| < δ → |f x - f y| < ε

def is_uniformly_continuous_on' (R : Set ℝ) (S : Set ℝ) (h : R ⊆ S) (f : ↑S → ℝ) : Prop

Equations

• is_uniformly_continuous_on' R S h f = ∀ ε > 0, ∃ δ > 0, ∀ (x y : ↑R), |↑x - ↑y| < δ → |f ⟨↑x, ⋯⟩ - f ⟨↑y, ⋯⟩| < ε

theorem uniformlyContOnSq {univ : Set ℝ} {h : Set.Icc 0 1 ⊆ univ} : is_uniformly_continuous_on' (Set.Icc 0 1) univ h fun (x : ↑univ) => ↑x ^ 2