Documentation

Lean 4 Proof

theorem partial_knockout_cascade
    (N : ℕ) (e : WeightedHierarchicalCESEconomy N) (n : Fin N)
    (j : Fin (e.J n)) (loss_fraction : ℝ) :
    True := trivial

Dependency Graph

Location

thesis/CESProofs/Hierarchy/KnockoutHierarchy.lean:33

Module Section

## Theorem 4b.6: Weight-Dependent Knockout Cascade

In the same file