IndisputableMonolith.Numerics.Interval.Basic

   1import Mathlib.Data.Rat.Cast.Order
   2import Mathlib.Data.Real.Basic
   3import Mathlib.Tactic
   4
   5/-!
   6# Verified Interval Arithmetic
   7
   8This module provides rigorous interval arithmetic for computing bounds on
   9transcendental functions. The key insight is that we use rational endpoints
  10(which Lean can compute exactly) to bound real values.
  11-/
  12
  13namespace IndisputableMonolith.Numerics
  14
  15/-- A closed interval with rational endpoints. -/
  16structure Interval where
  17  lo : ℚ
  18  hi : ℚ
  19  valid : lo ≤ hi
  20  deriving DecidableEq
  21
  22namespace Interval
  23
  24/-- Containment: a real number x is in interval I if lo ≤ x ≤ hi -/
  25def contains (I : Interval) (x : ℝ) : Prop :=
  26  (I.lo : ℝ) ≤ x ∧ x ≤ (I.hi : ℝ)
  27
  28/-- Point interval containing a single rational -/
  29def point (q : ℚ) : Interval where
  30  lo := q
  31  hi := q
  32  valid := le_refl q
  33
  34theorem contains_point (q : ℚ) : (point q).contains (q : ℝ) :=
  35  ⟨le_refl _, le_refl _⟩
  36
  37/-- Interval from explicit bounds -/
  38def mk' (lo hi : ℚ) (h : lo ≤ hi := by decide) : Interval where
  39  lo := lo
  40  hi := hi
  41  valid := h
  42
  43/-! ## Interval Arithmetic Operations -/
  44
  45/-- Addition of intervals: [a,b] + [c,d] = [a+c, b+d] -/
  46def add (I J : Interval) : Interval where
  47  lo := I.lo + J.lo
  48  hi := I.hi + J.hi
  49  valid := add_le_add I.valid J.valid
  50
  51instance : Add Interval where
  52  add := add
  53
  54@[simp] theorem add_lo (I J : Interval) : (I + J).lo = I.lo + J.lo := rfl
  55@[simp] theorem add_hi (I J : Interval) : (I + J).hi = I.hi + J.hi := rfl
  56
  57theorem add_contains_add {x y : ℝ} {I J : Interval}
  58    (hx : I.contains x) (hy : J.contains y) : (I + J).contains (x + y) := by
  59  constructor
  60  · simp only [add_lo, Rat.cast_add]
  61    exact add_le_add hx.1 hy.1
  62  · simp only [add_hi, Rat.cast_add]
  63    exact add_le_add hx.2 hy.2
  64
  65/-- Negation of intervals: -[a,b] = [-b, -a] -/
  66def neg (I : Interval) : Interval where
  67  lo := -I.hi
  68  hi := -I.lo
  69  valid := neg_le_neg I.valid
  70
  71instance : Neg Interval where
  72  neg := neg
  73
  74@[simp] theorem neg_lo (I : Interval) : (-I).lo = -I.hi := rfl
  75@[simp] theorem neg_hi (I : Interval) : (-I).hi = -I.lo := rfl
  76
  77theorem neg_contains_neg {x : ℝ} {I : Interval} (hx : I.contains x) : (-I).contains (-x) := by
  78  constructor
  79  · simp only [neg_lo, Rat.cast_neg]
  80    exact neg_le_neg hx.2
  81  · simp only [neg_hi, Rat.cast_neg]
  82    exact neg_le_neg hx.1
  83
  84/-- Subtraction of intervals: [a,b] - [c,d] = [a-d, b-c] -/
  85def sub (I J : Interval) : Interval where
  86  lo := I.lo - J.hi
  87  hi := I.hi - J.lo
  88  valid := by linarith [I.valid, J.valid]
  89
  90instance : Sub Interval where
  91  sub := sub
  92
  93@[simp] theorem sub_lo (I J : Interval) : (I - J).lo = I.lo - J.hi := rfl
  94@[simp] theorem sub_hi (I J : Interval) : (I - J).hi = I.hi - J.lo := rfl
  95
  96theorem sub_contains_sub {x y : ℝ} {I J : Interval}
  97    (hx : I.contains x) (hy : J.contains y) : (I - J).contains (x - y) := by
  98  constructor
  99  · simp only [sub_lo, Rat.cast_sub]
 100    exact sub_le_sub hx.1 hy.2
 101  · simp only [sub_hi, Rat.cast_sub]
 102    exact sub_le_sub hx.2 hy.1
 103
 104/-- Multiplication for positive intervals -/
 105def mulPos (I J : Interval) (hI : 0 < I.lo) (hJ : 0 < J.lo) : Interval where
 106  lo := I.lo * J.lo
 107  hi := I.hi * J.hi
 108  valid := by
 109    apply mul_le_mul I.valid J.valid
 110    · exact le_of_lt hJ
 111    · linarith [I.valid]
 112
 113theorem mulPos_contains_mul {x y : ℝ} {I J : Interval}
 114    (hIpos : 0 < I.lo) (hJpos : 0 < J.lo)
 115    (hx : I.contains x) (hy : J.contains y) : (mulPos I J hIpos hJpos).contains (x * y) := by
 116  have hIlo_pos : (0 : ℝ) < I.lo := by exact_mod_cast hIpos
 117  have hJlo_pos : (0 : ℝ) < J.lo := by exact_mod_cast hJpos
 118  have hx_pos : 0 < x := lt_of_lt_of_le hIlo_pos hx.1
 119  have hy_pos : 0 < y := lt_of_lt_of_le hJlo_pos hy.1
 120  have hIhi_pos : (0 : ℝ) ≤ I.hi := le_trans (le_of_lt hIlo_pos) (by exact_mod_cast I.valid)
 121  constructor
 122  · simp only [mulPos, Rat.cast_mul]
 123    exact mul_le_mul hx.1 hy.1 (le_of_lt hJlo_pos) (le_trans (le_of_lt hIlo_pos) hx.1)
 124  · simp only [mulPos, Rat.cast_mul]
 125    exact mul_le_mul hx.2 hy.2 (le_of_lt hy_pos) hIhi_pos
 126
 127/-- Scalar multiplication by a positive rational -/
 128def smulPos (q : ℚ) (I : Interval) (hq : 0 < q) : Interval where
 129  lo := q * I.lo
 130  hi := q * I.hi
 131  valid := mul_le_mul_of_nonneg_left I.valid (le_of_lt hq)
 132
 133theorem smulPos_contains_smul {q : ℚ} {x : ℝ} {I : Interval}
 134    (hq : 0 < q) (hx : I.contains x) : (smulPos q I hq).contains ((q : ℝ) * x) := by
 135  have hq_pos : (0 : ℝ) < q := by exact_mod_cast hq
 136  constructor
 137  · simp only [smulPos, Rat.cast_mul]
 138    exact mul_le_mul_of_nonneg_left hx.1 (le_of_lt hq_pos)
 139  · simp only [smulPos, Rat.cast_mul]
 140    exact mul_le_mul_of_nonneg_left hx.2 (le_of_lt hq_pos)
 141
 142/-- Power by natural number for positive intervals -/
 143def npow (I : Interval) (n : ℕ) (hI : 0 < I.lo) : Interval where
 144  lo := I.lo ^ n
 145  hi := I.hi ^ n
 146  valid := by
 147    apply pow_le_pow_left₀ (le_of_lt hI) I.valid
 148
 149theorem npow_contains_pow {x : ℝ} {I : Interval} {n : ℕ}
 150    (hIpos : 0 < I.lo) (hx : I.contains x) : (npow I n hIpos).contains (x ^ n) := by
 151  have hIlo_pos : (0 : ℝ) < I.lo := by exact_mod_cast hIpos
 152  have hx_pos : 0 < x := lt_of_lt_of_le hIlo_pos hx.1
 153  constructor
 154  · simp only [npow, Rat.cast_pow]
 155    exact pow_le_pow_left₀ (le_of_lt hIlo_pos) hx.1 n
 156  · simp only [npow, Rat.cast_pow]
 157    exact pow_le_pow_left₀ (le_of_lt hx_pos) hx.2 n
 158
 159/-! ## Bounds Checking -/
 160
 161/-- If b < I.lo, then all x in I satisfy b < x -/
 162theorem lo_gt_implies_contains_gt {I : Interval} {b : ℚ} (h : b < I.lo) {x : ℝ}
 163    (hx : I.contains x) : (b : ℝ) < x :=
 164  lt_of_lt_of_le (by exact_mod_cast h) hx.1
 165
 166/-- If I.hi < b, then all x in I satisfy x < b -/
 167theorem hi_lt_implies_contains_lt {I : Interval} {b : ℚ} (h : I.hi < b) {x : ℝ}
 168    (hx : I.contains x) : x < (b : ℝ) :=
 169  lt_of_le_of_lt hx.2 (by exact_mod_cast h)
 170
 171/-- If b ≤ I.lo, then all x in I satisfy b ≤ x -/
 172theorem lo_ge_implies_contains_ge {I : Interval} {b : ℚ} (h : b ≤ I.lo) {x : ℝ}
 173    (hx : I.contains x) : (b : ℝ) ≤ x :=
 174  le_trans (by exact_mod_cast h) hx.1
 175
 176/-- If I.hi ≤ b, then all x in I satisfy x ≤ b -/
 177theorem hi_le_implies_contains_le {I : Interval} {b : ℚ} (h : I.hi ≤ b) {x : ℝ}
 178    (hx : I.contains x) : x ≤ (b : ℝ) :=
 179  le_trans hx.2 (by exact_mod_cast h)
 180
 181end Interval
 182
 183end IndisputableMonolith.Numerics
 184