def
definition
phi_pow_16_interval
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.Numerics.Interval.Pow on GitHub at line 180.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
177 _ = ((111 / 10 : ℚ) : ℝ) := by norm_num
178
179/-- φ^16 interval ≈ 2207 - PROVEN -/
180def phi_pow_16_interval : Interval where
181 lo := 22069 / 10
182 hi := 22075 / 10
183 valid := by norm_num
184
185theorem phi_pow_16_in_interval : phi_pow_16_interval.contains (((1 + Real.sqrt 5) / 2) ^ (16 : ℝ)) := by
186 simp only [Interval.contains, phi_pow_16_interval]
187 rw [← phi_eq_formula]
188 have h : goldenRatio ^ (16 : ℝ) = goldenRatio ^ 16 := by
189 have : (16 : ℝ) = (16 : ℕ) := by norm_num
190 rw [this, Real.rpow_natCast]
191 rw [h]
192 constructor
193 · have h1 := phi_pow16_gt
194 calc ((22069 / 10 : ℚ) : ℝ) = (2206.9 : ℝ) := by norm_num
195 _ ≤ goldenRatio ^ 16 := le_of_lt h1
196 · have h1 := phi_pow16_lt
197 calc goldenRatio ^ 16 ≤ (2207.5 : ℝ) := le_of_lt h1
198 _ = ((22075 / 10 : ℚ) : ℝ) := by norm_num
199
200/-- 2^(-22) = 1/4194304 ≈ 2.384e-7 -/
201def two_pow_neg22_interval : Interval where
202 lo := 238 / 1000000000 -- 2.38e-7
203 hi := 239 / 1000000000 -- 2.39e-7
204 valid := by norm_num
205
206/-- 2^(-22) is in the interval - PROVEN -/
207theorem two_pow_neg22_in_interval : two_pow_neg22_interval.contains ((2 : ℝ) ^ (-22 : ℤ)) := by
208 simp only [Interval.contains, two_pow_neg22_interval]
209 -- 2^(-22) = 1/2^22 = 1/4194304
210 have h : (2 : ℝ) ^ (-22 : ℤ) = 1 / 4194304 := by