Pruning only below one node

Restrict the local weights below an anchor to a fixed set of ambient points. The lost total mass is exactly the lost cumulative mass at the anchor. The surviving weights can be rebuilt using the geometric pruning construction.

noncomputable def EGZ.FlagDecomposition.LocalizedPruning.weight {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) (anchor : Φ.flag.Node) (S : Set (FpCoord p d)) (y : Φ.flag.Node) (v : FpCoord p d) : ℕ

Restrict local weights below the anchor to S, retaining all other local weights.

Equations

• EGZ.FlagDecomposition.LocalizedPruning.weight Φ anchor S y v = if y ≤ anchor then EGZ.restrictWeight (Φ.localWeight y) S v else Φ.localWeight y v

theorem EGZ.FlagDecomposition.LocalizedPruning.weight_le {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) (anchor : Φ.flag.Node) (S : Set (FpCoord p d)) (y : Φ.flag.Node) (v : FpCoord p d) : weight Φ anchor S y v ≤ Φ.localWeight y v

theorem EGZ.FlagDecomposition.LocalizedPruning.cumulative_below {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) (anchor : Φ.flag.Node) (S : Set (FpCoord p d)) (y : Φ.flag.Node) (hy : y ≤ anchor) (v : FpCoord p d) : FlagDecompositionRaw.cumulativeWeight (weight Φ anchor S) y v = restrictWeight (Φ.cumulativeWeight y) S v

theorem EGZ.FlagDecomposition.LocalizedPruning.retainedWeight_le {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) (anchor : Φ.flag.Node) (S : Set (FpCoord p d)) (v : FpCoord p d) : FlagDecompositionRaw.retainedWeight (weight Φ anchor S) v ≤ Φ.retainedWeight v

theorem EGZ.FlagDecomposition.LocalizedPruning.retainedWeight_loss {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) (anchor : Φ.flag.Node) (S : Set (FpCoord p d)) (v : FpCoord p d) : Φ.retainedWeight v - FlagDecompositionRaw.retainedWeight (weight Φ anchor S) v = Φ.cumulativeWeight anchor v - restrictWeight (Φ.cumulativeWeight anchor) S v

At every ambient point, all loss occurs in the cumulative summand at the anchor and is exactly its excluded part.

theorem EGZ.FlagDecomposition.LocalizedPruning.retainedMass_loss {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) (anchor : Φ.flag.Node) (S : Set (FpCoord p d)) : Φ.retainedMass - natMass (FlagDecompositionRaw.retainedWeight (weight Φ anchor S)) = natMass (Φ.cumulativeWeight anchor) - natMass (restrictWeight (Φ.cumulativeWeight anchor) S)

theorem EGZ.FlagDecomposition.LocalizedPruning.nonzero {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) (anchor : Φ.flag.Node) (S : Set (FpCoord p d)) (hne : ∃ (v : FpCoord p d), restrictWeight (Φ.cumulativeWeight anchor) S v ≠ 0) : ∃ (y : Φ.flag.Node) (v : FpCoord p d), weight Φ anchor S y v ≠ 0

@[reducible, inline]

noncomputable abbrev EGZ.FlagDecomposition.LocalizedPruning.prunedWeights {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) (anchor : Φ.flag.Node) (S : Set (FpCoord p d)) (hne : ∃ (v : FpCoord p d), restrictWeight (Φ.cumulativeWeight anchor) S v ≠ 0) : Φ.PrunedWeights

The surviving local weights, ready for geometric rebuilding.

Equations

• EGZ.FlagDecomposition.LocalizedPruning.prunedWeights Φ anchor S hne = { weight := EGZ.FlagDecomposition.LocalizedPruning.weight Φ anchor S, weight_le := ⋯, nonzero := ⋯ }

@[reducible, inline]

noncomputable abbrev EGZ.FlagDecomposition.LocalizedPruning.decomposition {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) (anchor : Φ.flag.Node) (S : Set (FpCoord p d)) (hne : ∃ (v : FpCoord p d), restrictWeight (Φ.cumulativeWeight anchor) S v ≠ 0) (hp : Odd p) : FlagDecomposition p d f

The flag decomposition rebuilt from the locally pruned weights.

Equations

• EGZ.FlagDecomposition.LocalizedPruning.decomposition Φ anchor S hne hp = (EGZ.FlagDecomposition.LocalizedPruning.prunedWeights Φ anchor S hne).rebuilt hp

theorem EGZ.FlagDecomposition.LocalizedPruning.active_anchor {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) (anchor : Φ.flag.Node) (S : Set (FpCoord p d)) (hne : ∃ (v : FpCoord p d), restrictWeight (Φ.cumulativeWeight anchor) S v ≠ 0) (hp : Odd p) : ⋯.Active anchor

def EGZ.FlagDecomposition.LocalizedPruning.anchorNode {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) (anchor : Φ.flag.Node) (S : Set (FpCoord p d)) (hne : ∃ (v : FpCoord p d), restrictWeight (Φ.cumulativeWeight anchor) S v ≠ 0) (hp : Odd p) : (decomposition Φ anchor S hne hp).flag.Node

The surviving anchor as a node of the rebuilt decomposition.

Equations

• EGZ.FlagDecomposition.LocalizedPruning.anchorNode Φ anchor S hne hp = ⟨anchor, ⋯⟩

theorem EGZ.FlagDecomposition.LocalizedPruning.cumulativeWeight_anchorNode {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) (anchor : Φ.flag.Node) (S : Set (FpCoord p d)) (hne : ∃ (v : FpCoord p d), restrictWeight (Φ.cumulativeWeight anchor) S v ≠ 0) (hp : Odd p) : (decomposition Φ anchor S hne hp).cumulativeWeight (anchorNode Φ anchor S hne hp) = restrictWeight (Φ.cumulativeWeight anchor) S

theorem EGZ.FlagDecomposition.LocalizedPruning.cumulativeWeight_below {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) (anchor : Φ.flag.Node) (S : Set (FpCoord p d)) (hne : ∃ (v : FpCoord p d), restrictWeight (Φ.cumulativeWeight anchor) S v ≠ 0) (hp : Odd p) (x : (decomposition Φ anchor S hne hp).flag.Node) (hx : x ≤ anchorNode Φ anchor S hne hp) : (decomposition Φ anchor S hne hp).cumulativeWeight x = restrictWeight (Φ.cumulativeWeight ↑x) S

theorem EGZ.FlagDecomposition.LocalizedPruning.decomposition_retainedMass_loss {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) (anchor : Φ.flag.Node) (S : Set (FpCoord p d)) (hne : ∃ (v : FpCoord p d), restrictWeight (Φ.cumulativeWeight anchor) S v ≠ 0) (hp : Odd p) : ↑Φ.retainedMass - ↑(decomposition Φ anchor S hne hp).retainedMass = ↑(natMass (Φ.cumulativeWeight anchor)) - ↑(natMass (restrictWeight (Φ.cumulativeWeight anchor) S))