Documentation

Lean 4 Proof

theorem williamson_hierarchy_creation {baseCoupling c₁ c₂ c₀ withinBlock : ℝ}
    (hb : 0 < baseCoupling) (hc₀ : 0 < c₀) (_hw : 0 < withinBlock)
    (hlt : c₁ < c₂)
    (_hcross₁ : 0 < crossBlockCoupling baseCoupling c₁ c₀)
    (_hcross₂ : 0 < crossBlockCoupling baseCoupling c₂ c₀) :
    nearDecomposabilityParam (crossBlockCoupling baseCoupling c₂ c₀) withinBlock <
      nearDecomposabilityParam (crossBlockCoupling baseCoupling c₁ c₀) withinBlock := by
  unfold nearDecomposabilityParam
  exact div_lt_div_of_pos_right
    (transaction_cost_reduces_coupling hb hc₀ hlt) _hw

Dependency Graph

Location

thesis/CESProofs/Hierarchy/SpectralHierarchy.lean:257

Module Section

Endogenous Hierarchy: Why N Levels?

In the same file