Source indexedtheorem · leanprover/lean4:v4.32.0

log_ge'

PrimeNumberTheoremAnd.IEANTN.SecondaryDefinitions · PrimeNumberTheoremAnd/IEANTN/SecondaryDefinitions.lean:71 to 90

Mathematical statement

Exact Lean statement

@[blueprint
  "log_lower_2"
  (title := "Second log lower bound")
  (statement := /--
    For $0 \leq t \leq t_0 < 1$, one has
    $\frac{t}{t_0} \log (1-t_0) \leq \log(1-t)$. -/)
  (proof := /-- Use concavity of log. -/)
  (latexEnv := "sublemma")
  (discussion := 766)]
theorem log_ge' {t t₀ : ℝ} (ht : 0 ≤ t) (ht0 : t ≤ t₀) (ht0' : t₀ < 1) :
    (t / t₀) * log (1 - t₀) ≤ log (1 - t)

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

@[blueprint  "log_lower_2"  (title := "Second log lower bound")  (statement := /--    For $0 \leq t \leq t_0 < 1$, one has    $\frac{t}{t_0} \log (1-t_0) \leq \log(1-t)$. -/)  (proof := /-- Use concavity of log. -/)  (latexEnv := "sublemma")  (discussion := 766)]theorem log_ge' {t t₀ : ℝ} (ht : 0 ≤ t) (ht0 : t ≤ t₀) (ht0' : t₀ < 1) :    (t / t₀) * log (1 - t₀) ≤ log (1 - t) := by  rcases ht.eq_or_lt with rfl | ht  · simp  rcases ht0.eq_or_lt with rfl | ht0  · field_simp [ht.ne]    rfl  have := strictConcaveOn_log_Ioi.2 (y := 1) (x := 1 - t₀) (by grind) (by grind) (by linarith)  simp only [smul_eq_mul, log_one, mul_zero, add_zero, mul_one] at this  convert! this (a := t / t₀) (b := 1 - t / t₀) (by bound) (by bound) (by ring) |>.le using 2  field [show t₀ ≠ 0 by linarith]