Documentation

Lean 4 Proof

theorem knockout_no_failure (ρ : ℝ) (hJ : 0 < J) :
    knockoutRetained J ρ 0 = 1 := by
  simp only [knockoutRetained, Nat.cast_zero, sub_zero]
  split_ifs with h
  · rw [div_self (Nat.cast_ne_zero.mpr (by omega))]
    simp
  · rfl

Dependency Graph

Location

thesis/CESProofs/Foundations/FurtherProperties.lean:90

Module Section

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

In the same file