Documentation

Lean 4 Proof

theorem escort_compresses_leader {x₁ x₂ : ℝ} (_hx₁ : 0 < x₁) (hx₂ : 0 < x₂)
    (hgt : x₂ < x₁) {ρ : ℝ} (_hρ₀ : 0 < ρ) (hρ₁ : ρ < 1) :
    (x₁ / x₂) ^ ρ < (x₁ / x₂) ^ (1 : ℝ) := 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:291

Module Section

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

In the same file