Documentation

Lean 4 Proof

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

Dependency Graph

Location

thesis/CESProofs/Potential/SubstituteRegime.lean:205

Module Section

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

In the same file