Documentation

Lean 4 Proof

theorem knockout_total_failure {ρ : ℝ} (hρ : ρ ≤ 0) {m : ℕ} (hm : 0 < m) :
    knockoutRetained J ρ m = 0 := by
  simp only [knockoutRetained]
  simp [show ¬(ρ > 0) by linarith, show ¬(m = 0) by omega]

Dependency Graph

Used by

Location

thesis/CESProofs/Foundations/FurtherProperties.lean:84

Module Section

Further properties of CES curvature (Paper 1, Section 9):

In the same file