Finite and countable domain-loss estimates from the individual step budgets.

theorem KamProject.Arnold1963.Iteration.finite_loss_le {n : ℕ} (G : ℕ → Set (ComplexSpace n)) (b : ℕ → ENNReal) (hstep : ∀ (s : ℕ), realVolume (G s \ G (s + 1)) ≤ b s * realVolume (G 0)) (s : ℕ) : realVolume (G 0 \ G s) ≤ (∑ j ∈ Finset.range s, b j) * realVolume (G 0)

theorem KamProject.Arnold1963.Iteration.limit_loss_le {n : ℕ} (G : ℕ → Set (ComplexSpace n)) (b : ℕ → ENNReal) (hstep : ∀ (s : ℕ), realVolume (G s \ G (s + 1)) ≤ b s * realVolume (G 0)) : realVolume (G 0 \ ⋂ (s : ℕ), G s) ≤ (∑' (s : ℕ), b s) * realVolume (G 0)

theorem KamProject.Arnold1963.Iteration.limit_positive_of_budget {n : ℕ} (G : ℕ → Set (ComplexSpace n)) (b : ℕ → ENNReal) {κ : ENNReal} (hstep : ∀ (s : ℕ), realVolume (G s \ G (s + 1)) ≤ b s * realVolume (G 0)) (hsum : ∑' (s : ℕ), b s < κ) (hκ : κ < 1) (hpos : 0 < realVolume (G 0)) (hfinite : realVolume (G 0) ≠ ⊤) : realVolume (G 0 \ ⋂ (s : ℕ), G s) < κ * realVolume (G 0) ∧ 0 < realVolume (⋂ (s : ℕ), G s) ∧ (realSlice (⋂ (s : ℕ), G s)).Nonempty