Documentation

Lean 4 Proof

theorem gap_from_one_le {r : ℝ} {J : ℕ} (hJ : 2 ≤ J) (hr : 0 ≤ r) :
    1 - compoundSymmetryCorr r J ≤ ↑J * r := by
  rw [gap_from_one hJ hr]
  have hd : 1 ≤ 1 + (↑J - 1) * r := by nlinarith [hJ_sub_one_pos hJ]
  exact div_le_self (mul_nonneg (Nat.cast_nonneg J) hr) hd

Dependency Graph

Used by

Location

thesis/CESProofs/Foundations/CorrelationConvergence.lean:155

Module Section

Correlation Convergence at the Regime Boundary

In the same file