Documentation

Lean 4 Proof

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

Dependency Graph

Location

thesis/CESProofs/Foundations/CorrelationConvergence.lean:162

Module Section

Correlation Convergence at the Regime Boundary

In the same file