  29
  30/-- Simple power interval using explicit bounds.
  31    Given bounds on the final result, just package them. -/
  32def rpowIntervalSimple
  33    (result_lo result_hi : ℚ)
  34    (h_valid : result_lo ≤ result_hi) : Interval where
  35  lo := result_lo
  36  hi := result_hi
  37  valid := h_valid
  38
  39/-- The simple power interval contains x^y if the bounds are correct -/
  40theorem rpowIntervalSimple_contains_rpow
  41    {result_lo result_hi : ℚ}
  42    (h_valid : result_lo ≤ result_hi)
  43    {x y : ℝ}
  44    (h_lo : (result_lo : ℝ) ≤ x.rpow y)
  45    (h_hi : x.rpow y ≤ (result_hi : ℝ)) :
  46    (rpowIntervalSimple result_lo result_hi h_valid).contains (x.rpow y) :=
  47  ⟨h_lo, h_hi⟩
  48
  49/-- Interval containing φ = (1 + √5)/2 ≈ 1.618 -/
  50def phiInterval : Interval where
  51  lo := 1618 / 1000
  52  hi := 1619 / 1000
  53  valid := by norm_num
  54
  55/-- φ is in phiInterval - PROVEN using sqrt bounds -/
  56theorem phi_in_phiInterval : phiInterval.contains ((1 + Real.sqrt 5) / 2) := by
  57  simp only [Interval.contains, phiInterval]
  58  constructor
  59  · have h := phi_gt_1618
  60    have h1 : ((1618 / 1000 : ℚ) : ℝ) < (1 + Real.sqrt 5) / 2 := by
  61      calc ((1618 / 1000 : ℚ) : ℝ) = (1.618 : ℝ) := by norm_num
  62        _ < (1 + Real.sqrt 5) / 2 := h

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.