Documentation

Lean 4 Proof

theorem irs_amplifies_diversity_window
    (Tstar_base γ : ℝ) (hTs : 0 < Tstar_base) (hγ : 1 < γ) :
    Tstar_base < irsCriticalFrictionPerp Tstar_base γ := by
  unfold irsCriticalFrictionPerp
  calc Tstar_base = Tstar_base * 1 := by ring
    _ < Tstar_base * γ := by exact mul_lt_mul_of_pos_left hγ hTs

Dependency Graph

Location

thesis/CESProofs/Potential/FirmScope.lean:227

Module Section

## IRS and Firm Scope

In the same file