Documentation

Lean 4 Proof

theorem diversification_dominates {J : ℕ} (hJ : 2 ≤ J) {ρ : ℝ}
    (hρ₀ : 0 < ρ) (hρ₁ : ρ < 1) :
    specializationRatio J ρ < 1 := by
  unfold specializationRatio
  have hJgt : (1 : ℝ) < ↑J := by exact_mod_cast (show 1 < J by omega)
  have hexp : (ρ - 1) / ρ < 0 := div_neg_of_neg_of_pos (by linarith) hρ₀
  calc (↑J : ℝ) ^ ((ρ - 1) / ρ) < (↑J : ℝ) ^ (0 : ℝ) :=
        rpow_lt_rpow_of_exponent_lt hJgt hexp
    _ = 1 := rpow_zero _

Dependency Graph

Location

thesis/CESProofs/Potential/SubstituteRegime.lean:218

Module Section

Substitute Regime: The ρ > 1 Theory (Anti-Complementarity)

In the same file