Documentation

Lean 4 Proof

theorem equal_weight_entry_improves_K {J : ℕ} (hJ : 1 ≤ J) {ρ : ℝ} (hρ : ρ < 1) :
    curvatureK J ρ < curvatureK (J + 1) ρ := by
  simp only [curvatureK]
  have hJpos : (0:ℝ) < ↑J := by exact_mod_cast (show 0 < J by omega)
  rw [div_lt_div_iff₀ hJpos (by push_cast; linarith)]
  push_cast; nlinarith

Dependency Graph

Location

thesis/CESProofs/EntryExit/CurvatureInJ.lean:166

Module Section

## Entry with General Weights

In the same file