IndisputableMonolith.Numerics.Interval.Tactic

   1import IndisputableMonolith.Numerics.Interval.Basic
   2import IndisputableMonolith.Numerics.Interval.Exp
   3import IndisputableMonolith.Numerics.Interval.Log
   4import IndisputableMonolith.Numerics.Interval.Pow
   5import Mathlib.Tactic
   6
   7/-!
   8# Interval Bound Tactics
   9
  10This module provides tactics for proving bounds on transcendental expressions
  11using interval arithmetic.
  12
  13## Main Tactics
  14
  15* `interval_bound` - Proves bounds like `a < f(x)` or `f(x) < b` using intervals
  16
  17## Usage
  18
  19```lean
  20example : (0.481 : ℝ) < Real.log 1.618 := by
  21  interval_bound  -- Uses interval arithmetic to verify
  22```
  23-/
  24
  25namespace IndisputableMonolith.Numerics.Interval
  26
  27open Lean Elab Tactic Meta
  28
  29/-- Helper to prove a bound using interval containment -/
  30theorem prove_lower_bound {I : Interval} {x : ℝ} {b : ℚ}
  31    (h_contains : I.contains x) (h_lo : b < I.lo) : (b : ℝ) < x :=
  32  I.lo_gt_implies_contains_gt h_lo h_contains
  33
  34theorem prove_upper_bound {I : Interval} {x : ℝ} {b : ℚ}
  35    (h_contains : I.contains x) (h_hi : I.hi < b) : x < (b : ℝ) :=
  36  I.hi_lt_implies_contains_lt h_hi h_contains
  37
  38theorem prove_lower_bound_le {I : Interval} {x : ℝ} {b : ℚ}
  39    (h_contains : I.contains x) (h_lo : b ≤ I.lo) : (b : ℝ) ≤ x :=
  40  I.lo_ge_implies_contains_ge h_lo h_contains
  41
  42theorem prove_upper_bound_le {I : Interval} {x : ℝ} {b : ℚ}
  43    (h_contains : I.contains x) (h_hi : I.hi ≤ b) : x ≤ (b : ℝ) :=
  44  I.hi_le_implies_contains_le h_hi h_contains
  45
  46/-- Prove that φ is in its interval -/
  47theorem phi_interval_contains :
  48    phiInterval.contains ((1 + Real.sqrt 5) / 2) := phi_in_phiInterval
  49
  50/-- Prove that log(φ) is in its interval -/
  51theorem log_phi_interval_contains :
  52    logPhiInterval.contains (Real.log ((1 + Real.sqrt 5) / 2)) := log_phi_in_interval
  53
  54/-- Example: Prove log(φ) > 0.48 (using interval lo = 481/1000 = 0.481) -/
  55theorem log_phi_gt_048 : (0.48 : ℝ) < Real.log ((1 + Real.sqrt 5) / 2) := by
  56  have h := log_phi_in_interval
  57  -- logPhiInterval.lo = 481/1000 > 0.48
  58  have h1 : (0.48 : ℝ) < (481 / 1000 : ℚ) := by norm_num
  59  exact lt_of_lt_of_le h1 h.1
  60
  61/-- Example: Prove log(φ) < 0.49 (using interval hi = 482/1000 = 0.482) -/
  62theorem log_phi_lt_049 : Real.log ((1 + Real.sqrt 5) / 2) < (0.49 : ℝ) := by
  63  have h := log_phi_in_interval
  64  -- logPhiInterval.hi = 482/1000 < 0.49
  65  have h1 : ((482 / 1000 : ℚ) : ℝ) < (0.49 : ℝ) := by norm_num
  66  exact lt_of_le_of_lt h.2 h1
  67
  68/-- Example: Prove φ > 1.61 (using interval lo = 1618/1000) -/
  69theorem phi_gt_161 : (1.61 : ℝ) < (1 + Real.sqrt 5) / 2 := by
  70  have h := phi_in_phiInterval
  71  -- phiInterval.lo = 1618/1000 > 1.61
  72  have h1 : (1.61 : ℝ) < (1618 / 1000 : ℚ) := by norm_num
  73  exact lt_of_lt_of_le h1 h.1
  74
  75/-- Example: Prove φ < 1.62 (using interval hi = 1619/1000) -/
  76theorem phi_lt_162 : (1 + Real.sqrt 5) / 2 < (1.62 : ℝ) := by
  77  have h := phi_in_phiInterval
  78  -- phiInterval.hi = 1619/1000 < 1.62
  79  have h1 : ((1619 / 1000 : ℚ) : ℝ) < (1.62 : ℝ) := by norm_num
  80  exact lt_of_le_of_lt h.2 h1
  81
  82end IndisputableMonolith.Numerics.Interval
  83