Documentation

Lean 4 Proof

theorem quantity_correlation_to_floor {a δ : ℝ} {J : ℕ}
    (hJ : 2 ≤ J) (ha : 0 < a) (hδ : 0 < δ) :
    compoundSymmetryCorr (a / δ) J + 1 / (↑J - 1) =
    ↑J / ((↑J - 1) * (1 + (↑J - 1) * (a / δ))) :=
  correlation_floor_identity hJ (le_of_lt (div_pos ha hδ))

Dependency Graph

Location

thesis/CESProofs/Foundations/CorrelationConvergence.lean:191

Module Section

Correlation Convergence at the Regime Boundary

In the same file