Documentation

Lean 4 Proof

theorem fragility_bounds {ρ : ℝ} (hρ : 0 < ρ) (hJ : 0 < J) (hJ2 : 1 < J) :
    0 < fragilityIndex J ρ ∧ fragilityIndex J ρ < 1 := by
  simp only [fragilityIndex]
  have hk := knockout_partial_retained hρ hJ (by omega : 0 < 1) (by omega : 1 < J)
  constructor
  · linarith [hk.2]
  · linarith [hk.1]

Dependency Graph

Location

thesis/CESProofs/Potential/FirmScope.lean:180

Module Section

Propositions 12-17 and Corollary 5:

In the same file