logIntervalMono_contains_log

formal source

  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