prove_lower_bound

formal source

  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