Sections / Section 11: Dynamics and Business Cycles / compoundSymmetryMatrix

Compound Symmetry Covariance

defprovedDynamics & Crises

Documentation

Lean 4 Proof

def compoundSymmetryMatrix (J : ℕ) (s_sq g : ℝ) (i j : Fin J) : ℝ :=
  if i = j then s_sq else g

Dependency Graph

Used by

compound_symmetry_cov compound_symmetry_decomp compound_symmetry_cov_perp

Location

thesis/CESProofs/Dynamics/ConservationLaws.lean:89

Module Section

Results 36-46: Conservation Laws and Symmetry Identities

In the same file

euler_equilibrium_identity T_cross_sectional compound_symmetry_decomp compound_symmetry_cov compound_symmetry_cov_perp compoundSymmEigMarket compoundSymmEigIdio compound_symmetry_market_eigenvalue compound_symmetry_idio_eigenvalue compound_symmetry_trace covEigenvaluePerp eigenvalue_T_Keff_pos portfolio_diversification crooks_reversibility quantified_irreversibility deadweight_from_variance crisis_count_invariant antisym_total_sum_zero antisym_preserves_sum