phi_quarter_lt

formal source

 154  simpa using hlt
 155
 156/-- Upper bound: `φ^(1/4) < phi_quarter_hi` (proved via monotonicity of `x ↦ x^4`). -/
 157theorem phi_quarter_lt : goldenRatio ^ (1/4 : ℝ) < phi_quarter_hi := by
 158  -- Work in the simp-normal form `4⁻¹` (Lean normalizes `1/4` to `4⁻¹`).
 159  have hx : (0 : ℝ) ≤ goldenRatio ^ (4⁻¹ : ℝ) := by
 160    exact Real.rpow_nonneg (le_of_lt (by simpa using Real.goldenRatio_pos)) _
 161  have hy : (0 : ℝ) ≤ phi_quarter_hi := by simp [phi_quarter_hi]; norm_num
 162  have hz : (0 : ℝ) < (4 : ℝ) := by norm_num
 163  have hright : (goldenRatio ^ (4⁻¹ : ℝ)) ^ (4 : ℝ) = goldenRatio := by
 164    have hg0 : (0 : ℝ) ≤ goldenRatio := le_of_lt (by simpa using Real.goldenRatio_pos)
 165    calc (goldenRatio ^ (4⁻¹ : ℝ)) ^ (4 : ℝ)
 166        = goldenRatio ^ ((4⁻¹ : ℝ) * (4 : ℝ)) := by
 167            simpa using (Real.rpow_mul hg0 (4⁻¹ : ℝ) (4 : ℝ)).symm
 168      _ = goldenRatio ^ (1 : ℝ) := by norm_num
 169      _ = goldenRatio := by simp
 170  have hleft : phi_quarter_hi ^ (4 : ℝ) = phi_quarter_hi ^ (4 : ℕ) := by
 171    simpa using (Real.rpow_natCast phi_quarter_hi 4)
 172  have hq : goldenRatio < phi_quarter_hi ^ (4 : ℝ) := by
 173    have h1 : goldenRatio < (1.6180340 : ℝ) := phi_lt_16180340
 174    have h2 : (1.6180340 : ℝ) < phi_quarter_hi ^ (4 : ℕ) := phi_hi_lt_phi_quarter_hi_pow4
 175    have h2' : (1.6180340 : ℝ) < phi_quarter_hi ^ (4 : ℝ) := by simpa [hleft] using h2
 176    exact lt_trans h1 h2'
 177  have hpow : (goldenRatio ^ (4⁻¹ : ℝ)) ^ (4 : ℝ) < phi_quarter_hi ^ (4 : ℝ) := by
 178    simpa [hright] using hq
 179  have hlt : goldenRatio ^ (4⁻¹ : ℝ) < phi_quarter_hi :=
 180    (Real.rpow_lt_rpow_iff hx hy hz).1 hpow
 181  -- convert back to the displayed exponent `1/4`
 182  simpa using hlt
 183
 184/-- Consolidated quarter-root bounds. -/
 185theorem phi_quarter_bounds : phi_quarter_lo < goldenRatio ^ (1/4 : ℝ) ∧ goldenRatio ^ (1/4 : ℝ) < phi_quarter_hi :=
 186  ⟨phi_quarter_gt, phi_quarter_lt⟩
 187