Mass estimates for decomposition cleanup

The cleanup operations delete local atoms. These finite-sum estimates keep track of the lost mass and of the resulting deterioration of thickness.

theorem EGZ.natMass_mono {α : Type u_1} [Fintype α] {w w' : α → ℕ} (h : w' ≤ w) : natMass w' ≤ natMass w

theorem EGZ.natMassOn_mono_weight {α : Type u_1} [Fintype α] {w w' : α → ℕ} (h : w' ≤ w) (S : Set α) : natMassOn w' S ≤ natMassOn w S

theorem EGZ.natMassOn_le {α : Type u_1} [Fintype α] (w : α → ℕ) (S : Set α) : natMassOn w S ≤ natMass w

theorem EGZ.natMassOn_add_compl {α : Type u_1} [Fintype α] (w : α → ℕ) (S : Set α) : natMassOn w S + natMassOn w Sᶜ = natMass w

theorem EGZ.natMass_sub {α : Type u_1} [Fintype α] {w w' : α → ℕ} (h : w' ≤ w) : (natMass fun (a : α) => w a - w' a) = natMass w - natMass w'

theorem EGZ.natMassOn_sub {α : Type u_1} [Fintype α] {w w' : α → ℕ} (h : w' ≤ w) (S : Set α) : natMassOn (fun (a : α) => w a - w' a) S = natMassOn w S - natMassOn w' S

theorem EGZ.natMassOn_loss_le {α : Type u_1} [Fintype α] {w w' : α → ℕ} (h : w' ≤ w) (S : Set α) : natMassOn w S - natMassOn w' S ≤ natMass w - natMass w'

theorem EGZ.natMassOn_loss_le_real {α : Type u_1} [Fintype α] {w w' : α → ℕ} (h : w' ≤ w) (S : Set α) : ↑(natMassOn w S) - ↑(natMassOn w' S) ≤ ↑(natMass w) - ↑(natMass w')

theorem EGZ.nnrealMass_natCast {α : Type u_1} [Fintype α] (w : α → ℕ) : (nnrealMass fun (a : α) => ↑(w a)) = ↑(natMass w)

theorem EGZ.nnrealMassOn_natCast {α : Type u_1} [Fintype α] (w : α → ℕ) (S : Set α) : nnrealMassOn (fun (a : α) => ↑(w a)) S = ↑(natMassOn w S)

theorem EGZ.isThinAlong_iff_natMass {p d : ℕ} [NeZero p] (w : FpCoord p d → ℕ) (ξ : FpCoord p d →ᵃ[ZMod p] ZMod p) (K : ℕ) (ε : ℝ) : IsThinAlong w ξ K ε ↔ (1 - ε) * ↑(natMass w) ≤ ↑(natMassOn w (slab ξ K))

theorem EGZ.isThickAlong_iff_compl {p d : ℕ} [NeZero p] (w : FpCoord p d → ℕ) (ξ : FpCoord p d →ᵃ[ZMod p] ZMod p) (K : ℕ) (δ : ℝ) : IsThickAlong w ξ K δ ↔ δ * ↑(natMass w) < ↑(natMassOn w (slab ξ K)ᶜ)

theorem EGZ.IsThickAlong.of_pruning {p d : ℕ} [NeZero p] {w w' : FpCoord p d → ℕ} {ξ : FpCoord p d →ᵃ[ZMod p] ZMod p} {K : ℕ} {δ α ε M : ℝ} (hthick : IsThickAlong w ξ K δ) (hle : w' ≤ w) (hε : 0 < ε) (hα : 0 ≤ α) (hlarge : ε * M ≤ ↑(natMass w)) (hloss : ↑(natMass w) - ↑(natMass w') ≤ α * M) (hδ : 0 ≤ δ - α / ε) : IsThickAlong w' ξ K (δ - α / ε)

Deleting at most α M mass from a weight of mass at least ε M degrades thickness by at most α / ε. The strict inequality agrees with the definition of thickness as the negation of thinness.