Documentation

Lean 4 Proof

theorem correlation_le_one {r : ℝ} {J : ℕ} (hJ : 2 ≤ J) (hr : 0 ≤ r) :
    compoundSymmetryCorr r J ≤ 1 := by
  have h := gap_from_one hJ hr
  have hJ_pos : (0 : ℝ) < ↑J := by linarith [hJ_sub_one_pos hJ]
  have hden := den_pos hJ hr
  linarith [div_nonneg (mul_nonneg (le_of_lt hJ_pos) hr) (le_of_lt hden)]

Dependency Graph

Location

thesis/CESProofs/Foundations/CorrelationConvergence.lean:144

Module Section

Correlation Convergence at the Regime Boundary

In the same file