Documentation

Lean 4 Proof

theorem concentration_erodes_complementarity {ρ H : ℝ} {J : ℕ}
    (hρ : ρ < 1) (hJ : (0 : ℝ) < J) (hH : 1 / (J : ℝ) < H) :
    (1 - ρ) * (1 - H) < (1 - ρ) * ((J - 1 : ℝ) / J) := by
  apply mul_lt_mul_of_pos_left _ (by linarith : (0 : ℝ) < 1 - ρ)
  have : (J - 1 : ℝ) / J = 1 - 1 / J := by field_simp
  linarith

Dependency Graph

Location

thesis/CESProofs/Applications/Inequality.lean:191

Module Section

CES Inequality Decomposition

In the same file