phi_inv2_lt

formal source

 411  have hpos : 0 < goldenRatio⁻¹ := inv_pos.mpr goldenRatio_pos
 412  nlinarith [sq_nonneg goldenRatio⁻¹]
 413
 414theorem phi_inv2_lt : goldenRatio⁻¹ ^ 2 < (0.383 : ℝ) := by
 415  have h := phi_inv_lt
 416  have hpos : 0 < goldenRatio⁻¹ := inv_pos.mpr goldenRatio_pos
 417  nlinarith [sq_nonneg goldenRatio⁻¹]
 418
 419/-- (φ⁻¹)³ bounds -/
 420theorem phi_inv3_gt : (0.2359 : ℝ) < goldenRatio⁻¹ ^ 3 := by
 421  have h1 := phi_inv_gt
 422  have h2 := phi_inv2_gt
 423  have hpos : 0 < goldenRatio⁻¹ := inv_pos.mpr goldenRatio_pos
 424  have hpos2 : 0 < goldenRatio⁻¹ ^ 2 := sq_pos_of_pos hpos
 425  nlinarith [sq_nonneg goldenRatio⁻¹]
 426
 427theorem phi_inv3_lt : goldenRatio⁻¹ ^ 3 < (0.237 : ℝ) := by
 428  have h1 := phi_inv_lt
 429  have h2 := phi_inv2_lt
 430  have hpos : 0 < goldenRatio⁻¹ := inv_pos.mpr goldenRatio_pos
 431  nlinarith [sq_nonneg goldenRatio⁻¹]
 432
 433/-- Interval containing (φ⁻¹)³ - PROVEN -/
 434def phi_inv3_interval_proven : Interval where
 435  lo := 2359 / 10000
 436  hi := 237 / 1000
 437  valid := by norm_num
 438
 439theorem phi_inv3_in_interval_proven : phi_inv3_interval_proven.contains (goldenRatio⁻¹ ^ 3) := by
 440  simp only [Interval.contains, phi_inv3_interval_proven]
 441  constructor
 442  · have h := phi_inv3_gt
 443    exact le_of_lt (by calc ((2359 / 10000 : ℚ) : ℝ) = (0.2359 : ℝ) := by norm_num
 444      _ < goldenRatio⁻¹ ^ 3 := h)