Physical phase volume of retained action domains. Angle cells have side length 2 * pi. This source-volume estimate is separate from volume preservation by transformations.

theorem KamProject.Arnold1963.Iteration.InitialData.limit_physicalCell_volume_gt {n : ℕ} {Ω₀ : Set (ComplexSpace n)} {δ₁ θ₀ Θ₀ ρ₀ : NNReal} {κ D : ℝ} (b : InitialParameters n δ₁ θ₀ Θ₀ ρ₀ κ D) (h : InitialData n Ω₀ δ₁ θ₀ Θ₀ ρ₀ D) : ENNReal.ofReal (1 - κ) * (realPhaseLebesgue n) (realSlice h.domain ×ˢ realAngleCell n (2 * Real.pi)) < (realPhaseLebesgue n) (realSlice (limitDomain b h) ×ˢ realAngleCell n (2 * Real.pi))