Documentation

Lean 4 Proof

theorem weighted_trade_conservation
    (a : Fin 2 → Fin 2 → ℝ) :
    -- Antisymmetric coupling sums to zero
    (a 0 1 - a 1 0) + (a 1 0 - a 0 1) = 0 := by
  ring

Dependency Graph

Location

thesis/CESProofs/Dynamics/BusinessCycles.lean:473

Module Section

## Proposition 3b.5: Oscillation Spectrum with Weights

In the same file