Documentation

Lean 4 Proof

theorem detection_achievable (hJ : 2 ≤ J) :
    ∀ ρ : ℝ, ρ < -(1 / (↑J - 1 : ℝ)) → curvatureK J ρ > 1 := by
  intro ρ hρ
  simp only [curvatureK]
  have hJ1 : (1 : ℝ) < ↑J := by exact_mod_cast (by omega : 1 < J)
  have hJm1_pos : (0 : ℝ) < ↑J - 1 := by linarith
  rw [gt_iff_lt, ← sub_pos]
  have : (1 - ρ) * (↑J - 1) / ↑J - 1 = ((1 - ρ) * (↑J - 1) - ↑J) / ↑J := by
    field_simp
  rw [this]
  apply div_pos _ (by linarith)
  -- Need: (1-ρ)(J-1) > J.
  -- From ρ < -1/(J-1): 1-ρ > 1 + 1/(J-1).
  -- So (1-ρ)(J-1) > (1 + 1/(J-1))(J-1) = J-1 + 1 = J.
  have h1 : 1 - ρ > 1 + 1 / (↑J - 1) := by linarith
  -- (1-ρ)(J-1) > (1 + 1/(J-1))(J-1) = J-1 + 1 = J
  have h2 : (1 - ρ) * (↑J - 1) > ↑J := by
    calc (1 - ρ) * (↑J - 1) > (1 + 1 / (↑J - 1)) * (↑J - 1) := by
              nlinarith
      _ = (↑J - 1) + 1 := by field_simp
      _ = ↑J := by ring
  linarith

Dependency Graph

Location

thesis/CESProofs/CurvatureRoles/CorrelationRobust.lean:125

Module Section

Correlation robustness of CES (Paper 1, Section 7):

In the same file