cascadeIterate_subset

formal source

 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
 185/-- Recovery time after a cascade of depth `k` (in φ-ladder units of
 186the natural recovery scale `τ_0`). -/
 187def recoveryTime (k : ℕ) : ℝ := phi ^ k
 188
 189theorem recoveryTime_pos (k : ℕ) : 0 < recoveryTime k := by
 190  unfold recoveryTime
 191  exact pow_pos phi_pos k
 192
 193theorem recoveryTime_strict_mono (k : ℕ) :
 194    recoveryTime k < recoveryTime (k + 1) := by
 195  unfold recoveryTime