Documentation

Lean 4 Proof

theorem correlation_above_floor {r : ℝ} {J : ℕ} (hJ : 2 ≤ J) (hr : 0 ≤ r) :
    -1 / (↑J - 1) < compoundSymmetryCorr r J := by
  have h := correlation_floor_identity hJ hr
  have hJ1 := hJ_sub_one_pos hJ
  have hden := den_pos hJ hr
  have hJp : (0 : ℝ) < ↑J := Nat.cast_pos.mpr (by omega)
  have key : 0 < compoundSymmetryCorr r J + 1 / (↑J - 1) := by
    rw [h]; exact div_pos hJp (mul_pos hJ1 hden)
  have neg_cancel : (-1 : ℝ) / (↑J - 1) + 1 / (↑J - 1) = 0 := by
    rw [← add_div]; simp
  linarith

Dependency Graph

Used by

Location

thesis/CESProofs/Foundations/CorrelationConvergence.lean:131

Module Section

Correlation Convergence at the Regime Boundary

In the same file