IndisputableMonolith.Numerics.Interval.Log
IndisputableMonolith/Numerics/Interval/Log.lean · 430 lines · 27 declarations
show as:
view math explainer →
1import IndisputableMonolith.Numerics.Interval.Basic
2import IndisputableMonolith.Numerics.Interval.PhiBounds
3import Mathlib.Analysis.SpecialFunctions.Log.Basic
4import Mathlib.Analysis.Complex.ExponentialBounds
5import Mathlib.Analysis.SpecificLimits.Normed
6import Mathlib.Analysis.SpecialFunctions.Complex.LogBounds
7
8/-!
9# Interval Arithmetic for Logarithm Function
10
11This module provides rigorous interval bounds for the natural logarithm
12using Mathlib's bounds and Taylor series error estimates.
13
14## Strategy
15
16For x in [lo, hi] ⊆ (0, ∞):
171. log is monotonically increasing on (0, ∞), so log([lo, hi]) ⊆ [log(lo), log(hi)]
182. For log(1+x) with |x| < 1, we use the Taylor series:
19 log(1+x) = x - x²/2 + x³/3 - x⁴/4 + ...
203. The error after n terms is bounded by |x|^(n+1) / ((n+1)(1-|x|))
21
22For log(φ), we use x = φ - 1 ≈ 0.618 which satisfies 0 < x < 1.
23-/
24
25namespace IndisputableMonolith.Numerics
26
27open Interval
28open Real (log)
29
30/-- Simple lower bound: log(x) ≥ 1 - 1/x for x > 0 -/
31def logLowerSimple (x : ℚ) : ℚ := 1 - 1/x
32
33/-- Simple upper bound: log(x) ≤ x - 1 for x > 0 -/
34def logUpperSimple (x : ℚ) : ℚ := x - 1
35
36/-- For positive intervals, compute log interval using monotonicity of log -/
37def logIntervalMono (I : Interval) (_hI_pos : 0 < I.lo)
38 (lo_bound hi_bound : ℚ)
39 (_h_lo : (lo_bound : ℝ) ≤ log I.lo)
40 (_h_hi : log I.hi ≤ (hi_bound : ℝ))
41 (h_valid : lo_bound ≤ hi_bound) : Interval where
42 lo := lo_bound
43 hi := hi_bound
44 valid := h_valid
45
46theorem logIntervalMono_contains_log {I : Interval} (hI_pos : 0 < I.lo)
47 {lo_bound hi_bound : ℚ}
48 (h_lo : (lo_bound : ℝ) ≤ log I.lo)
49 (h_hi : log I.hi ≤ (hi_bound : ℝ))
50 (h_valid : lo_bound ≤ hi_bound)
51 {x : ℝ} (hx : I.contains x) :
52 (logIntervalMono I hI_pos lo_bound hi_bound h_lo h_hi h_valid).contains (log x) := by
53 simp only [contains, logIntervalMono]
54 have hx_lo : (I.lo : ℝ) ≤ x := hx.1
55 have hx_hi : x ≤ (I.hi : ℝ) := hx.2
56 have hIlo_pos : (0 : ℝ) < I.lo := by exact_mod_cast hI_pos
57 have hx_pos : 0 < x := lt_of_lt_of_le hIlo_pos hx_lo
58 constructor
59 · -- log x ≥ lo_bound
60 have h1 : log (I.lo : ℝ) ≤ log x := Real.log_le_log hIlo_pos hx_lo
61 linarith
62 · -- log x ≤ hi_bound
63 have h1 : log x ≤ log (I.hi : ℝ) := Real.log_le_log hx_pos hx_hi
64 linarith
65
66/-- Interval containing log(φ) where φ = (1 + √5)/2 ≈ 1.618
67 We know log(φ) ≈ 0.4812
68 Using [0.48, 0.483] to enable proof with 15 Taylor terms -/
69def logPhiInterval : Interval where
70 lo := 48 / 100
71 hi := 483 / 1000
72 valid := by norm_num
73
74/-!
75## Proving log(φ) bounds using Taylor series
76
77We use the identity log(φ) = log(1 + (φ - 1)) and the Taylor series error bound.
78
79The Taylor polynomial for log(1+x) up to degree n is:
80 T_n(x) = x - x²/2 + x³/3 - ... + (-1)^(n+1) * x^n / n
81
82The error |log(1+x) - T_n(x)| ≤ |x|^(n+1) / ((n+1)(1-|x|)) for |x| < 1.
83
84For x = φ - 1 ≈ 0.618:
85- We compute T_8(x) using rational bounds
86- The error is bounded by (0.619)^9 / (9 * (1 - 0.619)) ≈ 0.0025
87
88Strategy: Use Complex.norm_log_sub_logTaylor_le from Mathlib, specialized to real numbers.
89-/
90
91/-- For x = φ - 1, we have 0 < x < 1, so |x| = x -/
92lemma phi_minus_one_abs : |Real.goldenRatio - 1| = Real.goldenRatio - 1 := by
93 rw [abs_of_pos phi_sub_one_pos]
94
95/-- x = φ - 1 satisfies |x| < 1 -/
96lemma phi_minus_one_abs_lt_one : |Real.goldenRatio - 1| < 1 := by
97 rw [phi_minus_one_abs]
98 exact phi_sub_one_lt_one
99
100/-- Helper: ‖(x : ℂ)‖ = |x| for real x -/
101lemma complex_norm_ofReal (x : ℝ) : ‖(x : ℂ)‖ = |x| := by
102 have : (x : ℂ) = (RCLike.ofReal x : ℂ) := rfl
103 rw [this, RCLike.norm_ofReal]
104
105/-- Error bound for log Taylor polynomial on reals, using Complex.norm_log_sub_logTaylor_le -/
106lemma log_taylor_error_bound {x : ℝ} (hx : |x| < 1) (n : ℕ) :
107 |log (1 + x) - (Complex.logTaylor (n + 1) x).re| ≤ |x| ^ (n + 1) * (1 - |x|)⁻¹ / (n + 1) := by
108 -- Use the complex version and specialize to reals
109 have hx_complex : ‖(x : ℂ)‖ < 1 := by rw [complex_norm_ofReal]; exact hx
110 have h := Complex.norm_log_sub_logTaylor_le n hx_complex
111 -- log(1 + x) for real x equals Re(log(1 + x)) when 1 + x > 0
112 have h1x_pos : (0 : ℝ) < 1 + x := by
113 have : -1 < x := by
114 have := abs_lt.mp hx
115 linarith
116 linarith
117 have hlog_real : log (1 + x) = (Complex.log (1 + x)).re := by
118 have h1 : (1 : ℂ) + (x : ℂ) = ((1 + x : ℝ) : ℂ) := by push_cast; ring
119 rw [h1, Complex.log_ofReal_re]
120 rw [hlog_real]
121 have hsub_re : (Complex.log (1 + ↑x) - Complex.logTaylor (n + 1) ↑x).re =
122 (Complex.log (1 + ↑x)).re - (Complex.logTaylor (n + 1) ↑x).re := by
123 simp only [Complex.sub_re]
124 rw [← hsub_re]
125 calc |((Complex.log (1 + ↑x) - Complex.logTaylor (n + 1) ↑x).re : ℝ)|
126 ≤ ‖Complex.log (1 + ↑x) - Complex.logTaylor (n + 1) ↑x‖ := Complex.abs_re_le_norm _
127 _ ≤ ‖(x : ℂ)‖ ^ (n + 1) * (1 - ‖(x : ℂ)‖)⁻¹ / (n + 1) := h
128 _ = |x| ^ (n + 1) * (1 - |x|)⁻¹ / (n + 1) := by simp only [complex_norm_ofReal]
129
130/-- Key lemma: bound on log(1+y) using Mathlib's abs_log_sub_add_sum_range_le.
131 For y > 0, log(1+y) = -log(1-(-y)), and the series is:
132 log(1+y) = y - y²/2 + y³/3 - y⁴/4 + ...
133 The partial sum S_n = Σ_{i=0}^{n-1} (-1)^i * y^(i+1) / (i+1)
134 Error bound: |log(1+y) - S_n| ≤ y^(n+1) / (1-y) for 0 < y < 1
135-/
136lemma log_one_add_bounds {y : ℝ} (hy_pos : 0 < y) (hy_lt : y < 1) (n : ℕ) :
137 let S := ∑ i ∈ Finset.range n, (-1 : ℝ) ^ i * y ^ (i + 1) / (i + 1)
138 let err := y ^ (n + 1) / (1 - y)
139 S - err ≤ log (1 + y) ∧ log (1 + y) ≤ S + err := by
140 intro S err
141 -- Use abs_log_sub_add_sum_range_le with x = -y
142 have hy_abs : |(-y)| < 1 := by simp [abs_of_neg (neg_neg_of_pos hy_pos)]; exact hy_lt
143 have h := Real.abs_log_sub_add_sum_range_le hy_abs n
144 -- The sum in Mathlib is Σ x^(i+1)/(i+1) = Σ (-y)^(i+1)/(i+1)
145 -- = Σ (-1)^(i+1) * y^(i+1) / (i+1) = -S (since (-1)^(i+1) = -(-1)^i)
146 have hsum_eq : (∑ i ∈ Finset.range n, (-y) ^ (i + 1) / (i + 1)) = -S := by
147 simp only [S]
148 rw [← Finset.sum_neg_distrib]
149 congr 1
150 ext i
151 have : (-y) ^ (i + 1) = (-1) ^ (i + 1) * y ^ (i + 1) := by
152 rw [neg_eq_neg_one_mul, mul_pow]
153 rw [this]
154 have h2 : (-1 : ℝ) ^ (i + 1) = -(-1 : ℝ) ^ i := by
155 rw [pow_succ]
156 ring
157 rw [h2]
158 ring
159 -- log(1 - (-y)) = log(1 + y)
160 have hlog_eq : log (1 - (-y)) = log (1 + y) := by ring_nf
161 -- |(-y)| = y since y > 0
162 have habs_neg_y : |(-y)| = y := by rw [abs_neg, abs_of_pos hy_pos]
163 rw [hsum_eq, hlog_eq, habs_neg_y] at h
164 -- h : |-S + log(1+y)| ≤ y^(n+1) / (1-y)
165 -- i.e., |log(1+y) - S| ≤ err
166 have h' : |log (1 + y) - S| ≤ err := by
167 have heq : -S + log (1 + y) = log (1 + y) - S := by ring
168 rw [heq] at h
169 exact h
170 constructor
171 · -- S - err ≤ log(1+y)
172 have := neg_abs_le (log (1 + y) - S)
173 linarith [h']
174 · -- log(1+y) ≤ S + err
175 have := le_abs_self (log (1 + y) - S)
176 linarith [h']
177
178/-- Taylor sum for exp at x = 48/100 (rational) -/
179private def exp_taylor_10_at_048 : ℚ :=
180 let x : ℚ := 48 / 100
181 1 + x + x^2/2 + x^3/6 + x^4/24 + x^5/120 + x^6/720 + x^7/5040 + x^8/40320 + x^9/362880
182
183/-- Error bound for Taylor at x = 48/100 -/
184private def exp_error_10_at_048 : ℚ :=
185 let x : ℚ := 48 / 100
186 x^10 * 11 / (Nat.factorial 10 * 10)
187
188/-- exp(0.48) < φ (via Taylor bound + φ lower bound) -/
189private lemma exp_048_lt_phi : exp_taylor_10_at_048 + exp_error_10_at_048 < 161803395 / 100000000 := by
190 native_decide
191
192/-- Rigorous lower bound: log(φ) > 0.48
193
194 Proof using exp monotonicity: log(φ) > 0.48 ↔ φ > exp(0.48).
195 We have φ > 1.61803395 and exp(0.48) ≈ 1.6160... < 1.61803395. -/
196theorem log_phi_gt_048 : (0.48 : ℝ) < log Real.goldenRatio := by
197 -- Equivalent to: exp(0.48) < φ
198 rw [Real.lt_log_iff_exp_lt Real.goldenRatio_pos]
199 -- Use Taylor bound for exp(0.48)
200 have hx_pos : (0 : ℝ) ≤ (0.48 : ℝ) := by norm_num
201 have hx_le1 : (0.48 : ℝ) ≤ 1 := by norm_num
202 have h_bound := Real.exp_bound' hx_pos hx_le1 (n := 10) (by norm_num : 0 < 10)
203 -- exp(0.48) ≤ S_10 + error
204 have h_taylor_eq : (∑ m ∈ Finset.range 10, (0.48 : ℝ)^m / m.factorial) =
205 (exp_taylor_10_at_048 : ℝ) := by
206 simp only [exp_taylor_10_at_048, Finset.sum_range_succ, Finset.sum_range_zero, Nat.factorial]
207 norm_num
208 have h_err_eq : (0.48 : ℝ)^10 * (10 + 1) / (Nat.factorial 10 * 10) =
209 (exp_error_10_at_048 : ℝ) := by
210 simp only [exp_error_10_at_048, Nat.factorial]
211 norm_num
212 have h_lt := exp_048_lt_phi
213 calc Real.exp (0.48 : ℝ)
214 ≤ (∑ m ∈ Finset.range 10, (0.48 : ℝ)^m / m.factorial) +
215 (0.48 : ℝ)^10 * (10 + 1) / (Nat.factorial 10 * 10) := h_bound
216 _ = (exp_taylor_10_at_048 : ℝ) + (exp_error_10_at_048 : ℝ) := by rw [h_taylor_eq, h_err_eq]
217 _ < ((161803395 / 100000000 : ℚ) : ℝ) := by exact_mod_cast h_lt
218 _ = (1.61803395 : ℝ) := by norm_num
219 _ < Real.goldenRatio := phi_gt_161803395
220
221/-- Taylor sum for exp at x = 481/1000 (rational). -/
222private def exp_taylor_10_at_0481 : ℚ :=
223 let x : ℚ := 481 / 1000
224 1 + x + x^2/2 + x^3/6 + x^4/24 + x^5/120 + x^6/720 + x^7/5040 + x^8/40320 + x^9/362880
225
226/-- Error bound for Taylor at x = 481/1000. -/
227private def exp_error_10_at_0481 : ℚ :=
228 let x : ℚ := 481 / 1000
229 x^10 * 11 / (Nat.factorial 10 * 10)
230
231/-- exp(0.481) < φ (via Taylor bound + φ lower bound). -/
232private lemma exp_0481_lt_phi : exp_taylor_10_at_0481 + exp_error_10_at_0481 < 161803395 / 100000000 := by
233 native_decide
234
235/-- Rigorous lower bound: log(φ) > 0.481.
236
237 Proof using exp monotonicity: log(φ) > 0.481 ↔ φ > exp(0.481).
238 We have φ > 1.61803395 and exp(0.481) ≈ 1.617691... < 1.61803395. -/
239theorem log_phi_gt_0481 : (0.481 : ℝ) < log Real.goldenRatio := by
240 rw [Real.lt_log_iff_exp_lt Real.goldenRatio_pos]
241 have hx_pos : (0 : ℝ) ≤ (0.481 : ℝ) := by norm_num
242 have hx_le1 : (0.481 : ℝ) ≤ 1 := by norm_num
243 have h_bound := Real.exp_bound' hx_pos hx_le1 (n := 10) (by norm_num : 0 < 10)
244 have h_taylor_eq : (∑ m ∈ Finset.range 10, (0.481 : ℝ)^m / m.factorial) =
245 (exp_taylor_10_at_0481 : ℝ) := by
246 simp only [exp_taylor_10_at_0481, Finset.sum_range_succ, Finset.sum_range_zero, Nat.factorial]
247 norm_num
248 have h_err_eq : (0.481 : ℝ)^10 * (10 + 1) / (Nat.factorial 10 * 10) =
249 (exp_error_10_at_0481 : ℝ) := by
250 simp only [exp_error_10_at_0481, Nat.factorial]
251 norm_num
252 have h_lt := exp_0481_lt_phi
253 calc Real.exp (0.481 : ℝ)
254 ≤ (∑ m ∈ Finset.range 10, (0.481 : ℝ)^m / m.factorial) +
255 (0.481 : ℝ)^10 * (10 + 1) / (Nat.factorial 10 * 10) := h_bound
256 _ = (exp_taylor_10_at_0481 : ℝ) + (exp_error_10_at_0481 : ℝ) := by rw [h_taylor_eq, h_err_eq]
257 _ < ((161803395 / 100000000 : ℚ) : ℝ) := by exact_mod_cast h_lt
258 _ = (1.61803395 : ℝ) := by norm_num
259 _ < Real.goldenRatio := phi_gt_161803395
260
261/-- Taylor sum for exp at x = 483/1000 (rational) -/
262private def exp_taylor_10_at_0483 : ℚ :=
263 let x : ℚ := 483 / 1000
264 1 + x + x^2/2 + x^3/6 + x^4/24 + x^5/120 + x^6/720 + x^7/5040 + x^8/40320 + x^9/362880
265
266/-- Error bound for Taylor at x = 483/1000 -/
267private def exp_error_10_at_0483 : ℚ :=
268 let x : ℚ := 483 / 1000
269 x^10 * 11 / (Nat.factorial 10 * 10)
270
271/-- φ < exp(0.483) (via Taylor bound + φ upper bound) -/
272private lemma phi_lt_exp_0483 : 16180340 / 10000000 + exp_error_10_at_0483 < exp_taylor_10_at_0483 := by
273 native_decide
274
275/-- Rigorous upper bound: log(φ) < 0.483
276
277 Proof using exp monotonicity: log(φ) < 0.483 ↔ φ < exp(0.483).
278 We have φ < 1.6180340 and exp(0.483) ≈ 1.6210... > 1.6180340. -/
279theorem log_phi_lt_0483 : log Real.goldenRatio < (0.483 : ℝ) := by
280 -- Equivalent to: φ < exp(0.483)
281 rw [Real.log_lt_iff_lt_exp Real.goldenRatio_pos]
282 -- Use Taylor bound for exp(0.483): exp(x) ≥ S_10 - error
283 have hx_abs : |(0.483 : ℝ)| ≤ 1 := by norm_num
284 have h_bound := Real.exp_bound hx_abs (n := 10) (by norm_num : 0 < 10)
285 have h_abs := abs_sub_le_iff.mp h_bound
286 -- h_abs.2: S_10 - exp ≤ error, i.e., S_10 - error ≤ exp
287 have h_taylor_eq : (∑ m ∈ Finset.range 10, (0.483 : ℝ)^m / m.factorial) =
288 (exp_taylor_10_at_0483 : ℝ) := by
289 simp only [exp_taylor_10_at_0483, Finset.sum_range_succ, Finset.sum_range_zero, Nat.factorial]
290 norm_num
291 have h_err_eq : |(0.483 : ℝ)|^10 * ((Nat.succ 10 : ℕ) / ((Nat.factorial 10 : ℕ) * 10)) =
292 (exp_error_10_at_0483 : ℝ) := by
293 simp only [abs_of_nonneg (by norm_num : (0 : ℝ) ≤ 0.483), exp_error_10_at_0483,
294 Nat.factorial, Nat.succ_eq_add_one]
295 norm_num
296 have h_lt := phi_lt_exp_0483
297 have h_lower : (exp_taylor_10_at_0483 : ℝ) - (exp_error_10_at_0483 : ℝ) ≤
298 Real.exp (0.483 : ℝ) := by
299 have h2 := h_abs.2
300 simp only [h_taylor_eq] at h2
301 linarith
302 calc Real.goldenRatio
303 < (1.6180340 : ℝ) := phi_lt_16180340
304 _ = ((16180340 / 10000000 : ℚ) : ℝ) := by norm_num
305 _ < (exp_taylor_10_at_0483 : ℝ) - (exp_error_10_at_0483 : ℝ) := by
306 have h_cast : ((16180340 / 10000000 : ℚ) : ℝ) + (exp_error_10_at_0483 : ℝ) <
307 (exp_taylor_10_at_0483 : ℝ) := by exact_mod_cast h_lt
308 linarith
309 _ ≤ Real.exp (0.483 : ℝ) := h_lower
310
311/-- log(φ) is contained in logPhiInterval - PROVEN using Taylor series bounds -/
312theorem log_phi_in_interval : logPhiInterval.contains (log ((1 + Real.sqrt 5) / 2)) := by
313 simp only [contains, logPhiInterval]
314 have hphi_eq : (1 + Real.sqrt 5) / 2 = Real.goldenRatio := by
315 unfold Real.goldenRatio
316 ring
317 rw [hphi_eq]
318 constructor
319 · -- 0.48 ≤ log φ
320 have h := log_phi_gt_048
321 have h1 : ((48 / 100 : ℚ) : ℝ) < log Real.goldenRatio := by
322 calc ((48 / 100 : ℚ) : ℝ) = (0.48 : ℝ) := by norm_num
323 _ < log Real.goldenRatio := h
324 exact le_of_lt h1
325 · -- log φ ≤ 0.483
326 have h := log_phi_lt_0483
327 have h1 : log Real.goldenRatio < ((483 / 1000 : ℚ) : ℝ) := by
328 calc log Real.goldenRatio < (0.483 : ℝ) := h
329 _ = ((483 / 1000 : ℚ) : ℝ) := by norm_num
330 exact le_of_lt h1
331
332/-- Interval containing log(2) ≈ 0.693 -/
333def log2Interval : Interval where
334 lo := 693 / 1000
335 hi := 694 / 1000
336 valid := by norm_num
337
338/-- log(2) is contained in log2Interval - PROVEN using Mathlib's log_two bounds -/
339theorem log_2_in_interval : log2Interval.contains (log 2) := by
340 simp only [contains, log2Interval]
341 constructor
342 · -- 0.693 ≤ log 2
343 have h := Real.log_two_gt_d9 -- 0.6931471803 < log 2
344 have h1 : ((693 / 1000 : ℚ) : ℝ) < log 2 := by
345 calc ((693 / 1000 : ℚ) : ℝ) = (0.693 : ℝ) := by norm_num
346 _ < (0.6931471803 : ℝ) := by norm_num
347 _ < log 2 := h
348 exact le_of_lt h1
349 · -- log 2 ≤ 0.694
350 have h := Real.log_two_lt_d9 -- log 2 < 0.6931471808
351 have h1 : log 2 < ((694 / 1000 : ℚ) : ℝ) := by
352 calc log 2 < (0.6931471808 : ℝ) := h
353 _ < (0.694 : ℝ) := by norm_num
354 _ = ((694 / 1000 : ℚ) : ℝ) := by norm_num
355 exact le_of_lt h1
356
357/-- Interval containing log(10) ≈ 2.3025 -/
358def log10Interval : Interval where
359 lo := 230 / 100
360 hi := 231 / 100
361 valid := by norm_num
362
363/-- log(10) is contained in log10Interval.
364 Proof using log(10) = log(2) + log(5) and Mathlib bounds.
365 log(2) ≈ 0.693, log(5) = log(10/2) requires log(10).
366 Instead: log(10) = 2*log(√10), but √10 computation is circular.
367 Best approach: log(10) = log(2) + log(5) where log(5) = log(4*5/4) = 2*log(2) + log(1.25)
368 So log(10) = 3*log(2) + log(1.25) -/
369theorem log_10_in_interval : log10Interval.contains (log 10) := by
370 simp only [contains, log10Interval]
371 -- log(10) = log(2 * 5) = log(2) + log(5)
372 -- log(5) = log(4 * 1.25) = log(4) + log(1.25) = 2*log(2) + log(1.25)
373 -- So log(10) = log(2) + 2*log(2) + log(1.25) = 3*log(2) + log(1.25)
374 have h_log10_eq : log 10 = 3 * log 2 + log (5/4) := by
375 have h1 : (10 : ℝ) = 8 * (5/4) := by norm_num
376 have h2 : (8 : ℝ) = 2^(3 : ℕ) := by norm_num
377 calc log 10 = log (8 * (5/4)) := by rw [h1]
378 _ = log 8 + log (5/4) := Real.log_mul (by norm_num) (by norm_num)
379 _ = log (2^(3 : ℕ)) + log (5/4) := by rw [h2]
380 _ = (3 : ℕ) * log 2 + log (5/4) := by rw [Real.log_pow]
381 _ = 3 * log 2 + log (5/4) := by norm_num
382 -- Bounds on log(2) from Mathlib
383 have h_log2_gt : log 2 > 0.6931471803 := Real.log_two_gt_d9
384 have h_log2_lt : log 2 < 0.6931471808 := Real.log_two_lt_d9
385 -- Bounds on log(5/4) = log(1.25) using Taylor series
386 -- log(1 + x) for x = 0.25: 0.25 - 0.25²/2 + 0.25³/3 - ... ≈ 0.2231
387 have h_log125_gt : log (5/4) > 0.223 := by
388 -- log(1.25) > 0.223 ↔ exp(0.223) < 1.25
389 rw [gt_iff_lt, Real.lt_log_iff_exp_lt (by norm_num : (0 : ℝ) < 5/4)]
390 -- exp(0.223) < 1.25
391 have hx_abs : |(0.223 : ℝ)| ≤ 1 := by norm_num
392 have h_bound := Real.exp_bound hx_abs (n := 5) (by norm_num : 0 < 5)
393 have h_upper := (abs_sub_le_iff.mp h_bound).1
394 have h_taylor : (∑ m ∈ Finset.range 5, (0.223 : ℝ)^m / m.factorial) +
395 |(0.223 : ℝ)|^5 * (6 : ℕ) / (Nat.factorial 5 * 5) < 1.25 := by
396 simp only [Finset.sum_range_succ, Finset.sum_range_zero, Nat.factorial,
397 abs_of_nonneg (by norm_num : (0 : ℝ) ≤ 0.223)]
398 norm_num
399 linarith
400 have h_log125_lt : log (5/4) < 0.224 := by
401 -- log(1.25) < 0.224 ↔ 1.25 < exp(0.224)
402 rw [Real.log_lt_iff_lt_exp (by norm_num : (0 : ℝ) < 5/4)]
403 -- exp(0.224) > 1.25
404 have hx_abs : |(0.224 : ℝ)| ≤ 1 := by norm_num
405 have h_bound := Real.exp_bound hx_abs (n := 4) (by norm_num : 0 < 4)
406 have h_lower := (abs_sub_le_iff.mp h_bound).2
407 have h_sum : (∑ m ∈ Finset.range 4, (0.224 : ℝ)^m / m.factorial) -
408 |(0.224 : ℝ)|^4 * (5 : ℕ) / (Nat.factorial 4 * 4) > 1.25 := by
409 simp only [Finset.sum_range_succ, Finset.sum_range_zero, Nat.factorial,
410 abs_of_nonneg (by norm_num : (0 : ℝ) ≤ 0.224)]
411 norm_num
412 calc (5/4 : ℝ) = 1.25 := by norm_num
413 _ < (∑ m ∈ Finset.range 4, (0.224 : ℝ)^m / m.factorial) -
414 |(0.224 : ℝ)|^4 * (5 : ℕ) / (Nat.factorial 4 * 4) := h_sum
415 _ ≤ Real.exp 0.224 := by linarith
416 rw [h_log10_eq]
417 constructor
418 · -- 2.30 ≤ 3*log(2) + log(5/4)
419 -- 3 * 0.6931471803 + 0.223 = 2.3024415409 > 2.30
420 have h1 : (3 : ℝ) * 0.6931471803 + 0.223 > 2.30 := by norm_num
421 have h2 : 3 * log 2 + log (5/4) > 3 * 0.6931471803 + 0.223 := by linarith
422 linarith
423 · -- 3*log(2) + log(5/4) ≤ 2.31
424 -- 3 * 0.6931471808 + 0.224 = 2.3034415424 < 2.31
425 have h1 : (3 : ℝ) * 0.6931471808 + 0.224 < 2.31 := by norm_num
426 have h2 : 3 * log 2 + log (5/4) < 3 * 0.6931471808 + 0.224 := by linarith
427 linarith
428
429end IndisputableMonolith.Numerics
430