Documentation

Lean 4 Proof

theorem knockout_from_paper1 {ρ : ℝ} (hρ : 0 < ρ) {m : ℕ}
    (hJ : 0 < J) (hm_pos : 0 < m) (hm_lt : m < J) :
    0 < knockoutRetained J ρ m ∧ knockoutRetained J ρ m < 1 :=
  knockout_partial_retained hρ hJ hm_pos hm_lt

Dependency Graph

Location

thesis/CESProofs/Potential/FirmScope.lean:201

Module Section

Propositions 12-17 and Corollary 5:

In the same file