Documentation

Lean 4 Proof

theorem escort_amplifies_leader {x₁ x₂ : ℝ} (_hx₁ : 0 < x₁) (hx₂ : 0 < x₂)
    (hgt : x₂ < x₁) {ρ : ℝ} (hρ : 1 < ρ) :
    (x₁ / x₂) ^ (1 : ℝ) < (x₁ / x₂) ^ ρ := by
  have hratio : (1 : ℝ) < x₁ / x₂ := by rwa [one_lt_div hx₂]
  exact rpow_lt_rpow_of_exponent_lt hratio hρ

Dependency Graph

Location

thesis/CESProofs/Potential/SubstituteRegime.lean:281

Module Section

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

In the same file