Moving all local mass below an anchor to a lower layer

After slab pruning, the completeness refinement transfers every surviving local summand below the anchor to the lower layer. The lower anchor keeps the same cumulative function, while its upper copy ceases to be reduced.

@[reducible, inline]

noncomputable abbrev EGZ.FlagDecomposition.LowerTransfer.decomposition {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) (anchor : Φ.flag.Node) (hp : Odd p) : FlagDecomposition p d f

The decomposition obtained by applying the full lower-transfer refinement at the anchor.

Equations

• EGZ.FlagDecomposition.LowerTransfer.decomposition Φ anchor hp = EGZ.FlagDecomposition.FaceRefinement.decomposition Φ anchor (fun (x : EGZ.FpCoord p d) => True) hp

@[reducible, inline]

noncomputable abbrev EGZ.FlagDecomposition.LowerTransfer.upper {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) (anchor : Φ.flag.Node) (hp : Odd p) (x : Φ.flag.Node) : (FaceRefinement.decomposition Φ anchor (fun (x : FpCoord p d) => True) hp).flag.Node

The upper-layer copy of a node in the lower-transfer decomposition.

Equations

• EGZ.FlagDecomposition.LowerTransfer.upper Φ anchor hp x = EGZ.FlagDecomposition.FaceRefinement.upper Φ anchor (fun (x : EGZ.FpCoord p d) => True) hp x

theorem EGZ.FlagDecomposition.LowerTransfer.active_lowerAnchor {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) (anchor : Φ.flag.Node) (hp : Odd p) : ⋯.Active (TwoLayer.lower anchor anchor ⋯)

def EGZ.FlagDecomposition.LowerTransfer.lowerAnchor {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) (anchor : Φ.flag.Node) (hp : Odd p) : (decomposition Φ anchor hp).flag.Node

The active lower-layer copy of the anchor after lower transfer.

Equations

• EGZ.FlagDecomposition.LowerTransfer.lowerAnchor Φ anchor hp = ⟨EGZ.TwoLayer.lower anchor anchor ⋯, ⋯⟩

theorem EGZ.FlagDecomposition.LowerTransfer.lowerAnchor_le_upper {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) (anchor : Φ.flag.Node) (hp : Odd p) : lowerAnchor Φ anchor hp ≤ upper Φ anchor hp anchor

theorem EGZ.FlagDecomposition.LowerTransfer.lowerAnchor_cumulativeWeight {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) (anchor : Φ.flag.Node) (hp : Odd p) : (decomposition Φ anchor hp).cumulativeWeight (lowerAnchor Φ anchor hp) = Φ.cumulativeWeight anchor

theorem EGZ.FlagDecomposition.LowerTransfer.cumulativeWeight_projection {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) (anchor : Φ.flag.Node) (hp : Odd p) (x : (decomposition Φ anchor hp).flag.Node) : (decomposition Φ anchor hp).cumulativeWeight x = Φ.cumulativeWeight (↑↑x).1

Moving all atoms down preserves the old cumulative function at both copies of every surviving node.

theorem EGZ.FlagDecomposition.LowerTransfer.local_layer_zero {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) (anchor : Φ.flag.Node) (hp : Odd p) (q : (decomposition Φ anchor hp).flag.Point) (hq : q ∈ (decomposition Φ anchor hp).omegaZero) (hbelow : q.base ≤ upper Φ anchor hp anchor) : (↑↑q.base).2 = 0

Every local generator below the upper anchor has lower-layer base.

theorem EGZ.FlagDecomposition.LowerTransfer.upperAnchor_not_isReducedElement {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) (anchor : Φ.flag.Node) (hp : Odd p) : ¬(decomposition Φ anchor hp).IsReducedElement (upper Φ anchor hp anchor)

The old upper anchor has no proper point based there after all its local generators have moved down to the lower layer.

noncomputable def EGZ.FlagDecomposition.LowerTransfer.extra {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) (anchor : Φ.flag.Node) (hp : Odd p) (k : ℕ) (x : (decomposition Φ anchor hp).flag.Node) : ℕ

Additional slab coordinates are carried only by lower nodes.

Equations

• EGZ.FlagDecomposition.LowerTransfer.extra Φ anchor hp k x = if (↑↑x).2 = 0 then k else 0

theorem EGZ.FlagDecomposition.LowerTransfer.extra_antitone {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) (anchor : Φ.flag.Node) (hp : Odd p) (k : ℕ) : Antitone (extra Φ anchor hp k)

@[simp]

theorem EGZ.FlagDecomposition.LowerTransfer.extra_upper {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) (anchor : Φ.flag.Node) (hp : Odd p) (k : ℕ) (x : Φ.flag.Node) : extra Φ anchor hp k (upper Φ anchor hp x) = 0

@[simp]

theorem EGZ.FlagDecomposition.LowerTransfer.extra_lowerAnchor {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) (anchor : Φ.flag.Node) (hp : Odd p) (k : ℕ) : extra Φ anchor hp k (lowerAnchor Φ anchor hp) = k