Documentation

Lean 4 Proof

theorem more_sectors_more_information {J₁ J₂ : ℕ}
    (hJ₁ : 2 ≤ J₁) (hJ₂ : J₁ ≤ J₂)
    {ρ : ℝ} (hρ : ρ < 1) :
    curvatureK J₁ ρ ≤ curvatureK J₂ ρ := by
  simp only [curvatureK]
  have hJ₁pos : (↑J₁ : ℝ) ≠ 0 := by exact_mod_cast (show J₁ ≠ 0 by omega)
  have hJ₂pos : (↑J₂ : ℝ) ≠ 0 := by exact_mod_cast (show J₂ ≠ 0 by omega)
  have hJ₁₂ : (↑J₁ : ℝ) ≤ ↑J₂ := by exact_mod_cast hJ₂
  have h1ρ : (0 : ℝ) ≤ 1 - ρ := by linarith
  rw [div_le_div_iff₀ (by positivity) (by positivity)]
  nlinarith [mul_nonneg h1ρ (sub_nonneg.mpr hJ₁₂)]

Dependency Graph

Location

thesis/CESProofs/Foundations/CESEstimation.lean:332

Module Section

CES Estimation Theory: Connecting Theory to Data

In the same file