Documentation

Lean 4 Proof

theorem lower_rho_raises_K (J : ℕ) (hJ : 2 ≤ J) {ρ₁ ρ₂ : ℝ}
    (hρ₁ : ρ₁ < 1) (hρ₂ : ρ₂ < 1) (h12 : ρ₁ < ρ₂) :
    -- K(J, ρ₂) < K(J, ρ₁): lower ρ → higher K
    (1 - ρ₂) * ((J - 1 : ℝ) / J) < (1 - ρ₁) * ((J - 1 : ℝ) / J) := by
  apply mul_lt_mul_of_pos_right _ _
  · linarith
  · apply div_pos
    · have : (1 : ℝ) ≤ (J : ℝ) - 1 := by
        have : (2 : ℝ) ≤ (J : ℝ) := by exact_mod_cast hJ
        linarith
      linarith
    · have : (0 : ℝ) < (J : ℝ) := by exact_mod_cast Nat.pos_of_ne_zero (by omega)
      exact this

Dependency Graph

Location

thesis/CESProofs/Dynamics/EndogenousRho.lean:352

Module Section

Results 70-79: Endogenous Complementarity Evolution

In the same file