Documentation

Lean 4 Proof

theorem correlation_floor_identity {r : ℝ} {J : ℕ} (hJ : 2 ≤ J) (hr : 0 ≤ r) :
    compoundSymmetryCorr r J + 1 / (↑J - 1) =
    ↑J / ((↑J - 1) * (1 + (↑J - 1) * r)) := by
  unfold compoundSymmetryCorr
  have hJ1 := hJ_sub_one_pos hJ
  have hden : (1 + (↑J - 1) * r) ≠ 0 := ne_of_gt (den_pos hJ hr)
  have hJ1ne : (↑J - 1 : ℝ) ≠ 0 := ne_of_gt hJ1
  field_simp
  ring

Dependency Graph

Used by

Location

thesis/CESProofs/Foundations/CorrelationConvergence.lean:116

Module Section

Correlation Convergence at the Regime Boundary

In the same file