Sections / Section 6: Information Geometry and Cumulant Tower / compoundSymmetryCorr

Compound Symmetry Corr

defprovedInfo Geometrykey theorem

Documentation

Lean 4 Proof

def compoundSymmetryCorr (r : ℝ) (J : ℕ) : ℝ :=
  (1 - r) / (1 + (↑J - 1) * r)

Dependency Graph

Used by

gap_from_one_nonneg crisis_correlation_dual compoundSymmetryCorr_one correlation_le_one price_convergence_linear correlation_above_floor compoundSymmetryCorr_zero correlation_floor_identity gap_from_one quantity_correlation_to_floor gap_from_one_le

Location

thesis/CESProofs/Foundations/CorrelationConvergence.lean:54

Module Section

Correlation Convergence at the Regime Boundary

In the same file

compoundSymmetryCorr_zero compoundSymmetryCorr_one hJ_sub_one_pos den_pos gap_from_one correlation_floor_identity correlation_above_floor correlation_le_one gap_from_one_le gap_from_one_nonneg price_convergence_linear quantity_correlation_to_floor crisis_correlation_dual