Documentation

Lean 4 Proof

theorem transaction_cost_reduces_coupling {baseCoupling c₁ c₂ c₀ : ℝ}
    (hb : 0 < baseCoupling) (hc₀ : 0 < c₀) (hlt : c₁ < c₂) :
    crossBlockCoupling baseCoupling c₂ c₀ <
      crossBlockCoupling baseCoupling c₁ c₀ := by
  unfold crossBlockCoupling
  apply mul_lt_mul_of_pos_left _ hb
  apply Real.exp_lt_exp.mpr
  -- Goal: -c₂/c₀ < -c₁/c₀
  apply div_lt_div_of_pos_right _ hc₀
  linarith

Dependency Graph

Used by

Location

thesis/CESProofs/Hierarchy/SpectralHierarchy.lean:241

Module Section

Endogenous Hierarchy: Why N Levels?

In the same file