Documentation

Lean 4 Proof

theorem gap_from_one {r : ℝ} {J : ℕ} (hJ : 2 ≤ J) (hr : 0 ≤ r) :
    1 - compoundSymmetryCorr r J =
    ↑J * r / (1 + (↑J - 1) * r) := by
  unfold compoundSymmetryCorr
  have hne : (1 + (↑J - 1) * r) ≠ 0 := ne_of_gt (den_pos hJ hr)
  rw [eq_div_iff hne, sub_mul, div_mul_cancel₀ _ hne]
  ring

Dependency Graph

Used by

Location

thesis/CESProofs/Foundations/CorrelationConvergence.lean:96

Module Section

Correlation Convergence at the Regime Boundary

In the same file