logIntervalMono

formal source

  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