Documentation

Lean 4 Proof

theorem concentration_raises_share_variance {H₁ H₂ : ℝ} {J : ℕ}
    (hH : H₁ < H₂) :
    H₁ - 1 / (↑J : ℝ) < H₂ - 1 / (↑J : ℝ) := by
  linarith

Dependency Graph

Location

thesis/CESProofs/Applications/Inequality.lean:338

Module Section

## CES Inequality Measures

In the same file