Mass transport at surviving nodes

An integral coordinate map compatible with the cumulative ambient atoms transports centered lifts exactly. A stable node map additionally bounds the loss at the node by the loss of the entire decomposition. These data compose, so the same estimates apply along a surviving lineage.

structure EGZ.FlagDecomposition.NodeMassMap {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} (Φ Ψ : FlagDecomposition p d f) (x : Φ.flag.Node) (y : Ψ.flag.Node) : Type

A compatible integral affine node map whose cumulative weight does not increase.

• coord : IntegralAffineMap (Ψ.flag.rank y) (Φ.flag.rank x)

  The integral affine map from the new node's coordinates to the original node's coordinates.

• polytope_mem : Set.MapsTo (⇑self.coord.real) (Ψ.flag.polytope y).carrier (Φ.flag.polytope x).carrier
• cumulative_le : Ψ.cumulativeWeight y ≤ Φ.cumulativeWeight x
• map_eq (v : FpCoord p d) : Ψ.cumulativeWeight y v ≠ 0 → (self.coord.modp p) ((Ψ.representation.map y) v) = (Φ.representation.map x) v

def EGZ.FlagDecomposition.NodeMassMap.refl {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) (x : Φ.flag.Node) : Φ.NodeMassMap Φ x x

The identity map on a node and its cumulative weight.

Equations

• EGZ.FlagDecomposition.NodeMassMap.refl Φ x = { coord := EGZ.IntegralAffineMap.id (Φ.flag.rank x), polytope_mem := ⋯, cumulative_le := ⋯, map_eq := ⋯ }

def EGZ.FlagDecomposition.NodeMassMap.comp {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} {Φ Ψ Ω : FlagDecomposition p d f} {x : Φ.flag.Node} {y : Ψ.flag.Node} {z : Ω.flag.Node} (M : Φ.NodeMassMap Ψ x y) (N : Ψ.NodeMassMap Ω y z) : Φ.NodeMassMap Ω x z

Compose compatible coordinate and cumulative-weight maps between three nodes.

Equations

• M.comp N = { coord := M.coord.comp N.coord, polytope_mem := ⋯, cumulative_le := ⋯, map_eq := ⋯ }

theorem EGZ.FlagDecomposition.NodeMassMap.centeredLift_eq {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} {Φ Ψ : FlagDecomposition p d f} {x : Φ.flag.Node} {y : Ψ.flag.Node} (M : Φ.NodeMassMap Ψ x y) (hp : Odd p) (v : FpCoord p d) (hv : Ψ.cumulativeWeight y v ≠ 0) : M.coord.integer ((Ψ.representation.map y) v).centeredLift = ((Φ.representation.map x) v).centeredLift

theorem EGZ.FlagDecomposition.NodeMassMap.real_centeredLift_eq {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} {Φ Ψ : FlagDecomposition p d f} {x : Φ.flag.Node} {y : Ψ.flag.Node} (M : Φ.NodeMassMap Ψ x y) (hp : Odd p) (v : FpCoord p d) (hv : Ψ.cumulativeWeight y v ≠ 0) : M.coord.real ((Ψ.representation.map y) v).centeredLift.real = ((Φ.representation.map x) v).centeredLift.real

theorem EGZ.FlagDecomposition.NodeMassMap.liftedMassOn_preimage {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} {Φ Ψ : FlagDecomposition p d f} {x : Φ.flag.Node} {y : Ψ.flag.Node} (M : Φ.NodeMassMap Ψ x y) (hp : Odd p) (S : Set (RealCoord (Φ.flag.rank x))) : Ψ.liftedMassOn y (⇑M.coord.real ⁻¹' S) = natMassOn (Ψ.cumulativeWeight y) {v : FpCoord p d | ((Φ.representation.map x) v).centeredLift.real ∈ S}

theorem EGZ.FlagDecomposition.NodeMassMap.liftedMassOn_preimage_le {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} {Φ Ψ : FlagDecomposition p d f} {x : Φ.flag.Node} {y : Ψ.flag.Node} (M : Φ.NodeMassMap Ψ x y) (hp : Odd p) (S : Set (RealCoord (Φ.flag.rank x))) : Ψ.liftedMassOn y (⇑M.coord.real ⁻¹' S) ≤ Φ.liftedMassOn x S

theorem EGZ.FlagDecomposition.NodeMassMap.liftedMassOn_loss_le {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} {Φ Ψ : FlagDecomposition p d f} {x : Φ.flag.Node} {y : Ψ.flag.Node} (M : Φ.NodeMassMap Ψ x y) (hp : Odd p) (S : Set (RealCoord (Φ.flag.rank x))) : ↑(Φ.liftedMassOn x S) - ↑(Ψ.liftedMassOn y (⇑M.coord.real ⁻¹' S)) ≤ ↑(natMass (Φ.cumulativeWeight x)) - ↑(natMass (Ψ.cumulativeWeight y))

structure EGZ.FlagDecomposition.StableNodeMap {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} (Φ Ψ : FlagDecomposition p d f) (x : Φ.flag.Node) (y : Ψ.flag.Node) extends Φ.NodeMassMap Ψ x y : Type

A node mass map whose mass loss is bounded by the decomposition's total retained-mass loss.

• coord : IntegralAffineMap (Ψ.flag.rank y) (Φ.flag.rank x)
• polytope_mem : Set.MapsTo (⇑self.coord.real) (Ψ.flag.polytope y).carrier (Φ.flag.polytope x).carrier
• cumulative_le : Ψ.cumulativeWeight y ≤ Φ.cumulativeWeight x
• map_eq (v : FpCoord p d) : Ψ.cumulativeWeight y v ≠ 0 → (self.coord.modp p) ((Ψ.representation.map y) v) = (Φ.representation.map x) v
• mass_loss_le : ↑(natMass (Φ.cumulativeWeight x)) - ↑(natMass (Ψ.cumulativeWeight y)) ≤ ↑Φ.retainedMass - ↑Ψ.retainedMass

def EGZ.FlagDecomposition.StableNodeMap.refl {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) (x : Φ.flag.Node) : Φ.StableNodeMap Φ x x

The identity stable node map, with zero mass loss.

Equations

• EGZ.FlagDecomposition.StableNodeMap.refl Φ x = { toNodeMassMap := EGZ.FlagDecomposition.NodeMassMap.refl Φ x, mass_loss_le := ⋯ }

def EGZ.FlagDecomposition.StableNodeMap.comp {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} {Φ Ψ Ω : FlagDecomposition p d f} {x : Φ.flag.Node} {y : Ψ.flag.Node} {z : Ω.flag.Node} (M : Φ.StableNodeMap Ψ x y) (N : Ψ.StableNodeMap Ω y z) : Φ.StableNodeMap Ω x z

Compose stable node maps, adding their bounds on mass loss.

Equations

• M.comp N = { toNodeMassMap := M.comp N.toNodeMassMap, mass_loss_le := ⋯ }

theorem EGZ.FlagDecomposition.StableNodeMap.liftedMassOn_loss_le {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} {Φ Ψ : FlagDecomposition p d f} {x : Φ.flag.Node} {y : Ψ.flag.Node} (M : Φ.StableNodeMap Ψ x y) (hp : Odd p) (S : Set (RealCoord (Φ.flag.rank x))) : ↑(Φ.liftedMassOn x S) - ↑(Ψ.liftedMassOn y (⇑M.coord.real ⁻¹' S)) ≤ ↑Φ.retainedMass - ↑Ψ.retainedMass