def
definition
cascadeIterate
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Ecology.ExtinctionCascadeFromLedgerBankruptcy on GitHub at line 154.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
151/-! ## §5. Iterated cascade closure -/
152
153/-- Iterate the cascade step `k` times. -/
154def cascadeIterate {n : ℕ} (E : Ecosystem n) (L : Finset (Fin n)) :
155 ℕ → Finset (Fin n)
156 | 0 => L
157 | k + 1 => cascadeStep E (cascadeIterate E L k)
158
159theorem cascadeIterate_zero {n : ℕ} (E : Ecosystem n) (L : Finset (Fin n)) :
160 cascadeIterate E L 0 = L := rfl
161
162theorem cascadeIterate_succ {n : ℕ} (E : Ecosystem n) (L : Finset (Fin n)) (k : ℕ) :
163 cascadeIterate E L (k + 1) = cascadeStep E (cascadeIterate E L k) := rfl
164
165theorem cascadeIterate_subset {n : ℕ} (E : Ecosystem n) (L : Finset (Fin n)) (k : ℕ) :
166 cascadeIterate E L (k + 1) ⊆ cascadeIterate E L k := by
167 rw [cascadeIterate_succ]
168 exact cascadeStep_subset E (cascadeIterate E L k)
169
170theorem cascadeIterate_subset_initial {n : ℕ} (E : Ecosystem n)
171 (L : Finset (Fin n)) (k : ℕ) :
172 cascadeIterate E L k ⊆ L := by
173 induction k with
174 | zero => simp [cascadeIterate]
175 | succ k ih =>
176 apply Finset.Subset.trans (cascadeIterate_subset E L k) ih
177
178theorem cascadeIterate_card_monotone {n : ℕ} (E : Ecosystem n)
179 (L : Finset (Fin n)) (k : ℕ) :
180 (cascadeIterate E L (k + 1)).card ≤ (cascadeIterate E L k).card :=
181 Finset.card_le_card (cascadeIterate_subset E L k)
182
183/-! ## §6. Cascade-recovery time on the φ-ladder -/
184