Documentation

Lean 4 Proof

theorem complementarity_no_tradeoff {ρ₁ ρ₂ r : ℝ} (J : ℕ) (hJ : 2 ≤ J)
    (_hρ₁ : ρ₁ < 1) (_hρ₂ : ρ₂ < 1) (h12 : ρ₁ < ρ₂)
    (_hρ₂_pos : 0 < ρ₂) (hr : 1 < r) :
    -- (a) Lower ρ → higher K
    (1 - ρ₂) * ((J - 1 : ℝ) / J) < (1 - ρ₁) * ((J - 1 : ℝ) / J)
    -- (b) Lower ρ → more compressed income (r^ρ₁ < r^ρ₂ when 0 < ρ₁ < ρ₂ < 1)
    ∧ r ^ ρ₁ < r ^ ρ₂ := by
  constructor
  · apply mul_lt_mul_of_pos_right (by linarith)
    apply div_pos
    · have : (2 : ℝ) ≤ (J : ℝ) := by exact_mod_cast hJ
      linarith
    · exact_mod_cast Nat.pos_of_ne_zero (by omega)
  · exact rpow_lt_rpow_of_exponent_lt (by linarith) h12

Dependency Graph

Location

thesis/CESProofs/Applications/Inequality.lean:128

Module Section

CES Inequality Decomposition

In the same file