theorem
proved
tactic proof
logIntervalMono_contains_log
show as:
view Lean formalization →
formal statement (Lean)
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
proof body
Tactic-mode proof.
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 -/