Documentation

Lean 4 Proof

private lemma bernoulli_rpow_ge_linear {ρ S : ℝ} (hρ0 : 0 < ρ) (hρ1 : ρ < 1) (hS : 1 ≤ S) :
    S ^ (1 / ρ) ≥ 1 + 1 / ρ * (S - 1) := by
  have hs_ge : -1 ≤ S - 1 := by linarith
  have hp_ge : 1 ≤ 1 / ρ := by rw [le_div_iff₀ hρ0]; linarith
  have := one_add_mul_self_le_rpow_one_add hs_ge hp_ge
  rwa [show 1 + (S - 1) = S from by ring] at this

Dependency Graph

Used by

Location

thesis/CESProofs/CurvatureRoles/Superadditivity.lean:290

Module Section

Superadditivity of CES (Paper 1, Section 6):

In the same file