Two-layer refinements of a finite node poset

Every old node has an upper copy, while nodes below an anchor also have a lower copy. The product order preserves joins. A global selector moves the selected atoms below the anchor to the lower layer; this preserves all total mass and every upper cumulative weight.

@[reducible, inline]

abbrev EGZ.TwoLayer.Node {α : Type u_1} [SemilatticeSup α] (anchor : α) : Type u_1

Upper copies of every node and lower copies below the chosen anchor.

Equations

• EGZ.TwoLayer.Node anchor = { a : α × Fin 2 // a.2 = 0 → a.1 ≤ anchor }

@[instance_reducible]

noncomputable instance EGZ.TwoLayer.instFintypeNode {α : Type u_1} [SemilatticeSup α] (anchor : α) [Fintype α] : Fintype (Node anchor)

Equations

• EGZ.TwoLayer.instFintypeNode anchor = Subtype.fintype fun (a : α × Fin 2) => a.2 = 0 → a.1 ≤ anchor

@[instance_reducible]

instance EGZ.TwoLayer.instSemilatticeSupNode {α : Type u_1} [SemilatticeSup α] (anchor : α) : SemilatticeSup (Node anchor)

Equations

• EGZ.TwoLayer.instSemilatticeSupNode anchor = Subtype.semilatticeSup ⋯

@[instance_reducible]

instance EGZ.TwoLayer.instOrderTopNode {α : Type u_1} [SemilatticeSup α] (anchor : α) [OrderTop α] : OrderTop (Node anchor)

Equations

• EGZ.TwoLayer.instOrderTopNode anchor = { top := ⟨(⊤, 1), ⋯⟩, le_top := ⋯ }

def EGZ.TwoLayer.projection {α : Type u_1} [SemilatticeSup α] (anchor : α) : SupHom (Node anchor) α

Forget the layer; this preserves joins.

Equations

• EGZ.TwoLayer.projection anchor = { toFun := fun (a : EGZ.TwoLayer.Node anchor) => (↑a).1, map_sup' := ⋯ }

def EGZ.TwoLayer.upper {α : Type u_1} [SemilatticeSup α] (anchor a : α) : Node anchor

The upper copy of an old node.

Equations

• EGZ.TwoLayer.upper anchor a = ⟨(a, 1), ⋯⟩

def EGZ.TwoLayer.lower {α : Type u_1} [SemilatticeSup α] (anchor a : α) (ha : a ≤ anchor) : Node anchor

The lower copy of a node below the anchor.

Equations

• EGZ.TwoLayer.lower anchor a ha = ⟨(a, 0), ⋯⟩

@[simp]

theorem EGZ.TwoLayer.projection_upper {α : Type u_1} [SemilatticeSup α] (anchor a : α) : (projection anchor) (upper anchor a) = a

@[simp]

theorem EGZ.TwoLayer.projection_lower {α : Type u_1} [SemilatticeSup α] (anchor a : α) (ha : a ≤ anchor) : (projection anchor) (lower anchor a ha) = a

@[simp]

theorem EGZ.TwoLayer.upper_le_upper {α : Type u_1} [SemilatticeSup α] (anchor a b : α) : upper anchor a ≤ upper anchor b ↔ a ≤ b

@[simp]

theorem EGZ.TwoLayer.lower_le_lower {α : Type u_1} [SemilatticeSup α] (anchor a b : α) (ha : a ≤ anchor) (hb : b ≤ anchor) : lower anchor a ha ≤ lower anchor b hb ↔ a ≤ b

@[simp]

theorem EGZ.TwoLayer.lower_le_upper {α : Type u_1} [SemilatticeSup α] (anchor a b : α) (ha : a ≤ anchor) : lower anchor a ha ≤ upper anchor b ↔ a ≤ b

@[simp]

theorem EGZ.TwoLayer.not_upper_le_lower {α : Type u_1} [SemilatticeSup α] (anchor a b : α) (hb : b ≤ anchor) : ¬upper anchor a ≤ lower anchor b hb

def EGZ.TwoLayer.upperEmbedding {α : Type u_1} [SemilatticeSup α] (anchor : α) : α ↪o Node anchor

The order embedding of the original poset into the upper layer.

Equations

• EGZ.TwoLayer.upperEmbedding anchor = { toFun := EGZ.TwoLayer.upper anchor, inj' := ⋯, map_rel_iff' := ⋯ }

def EGZ.TwoLayer.lowerEmbedding {α : Type u_1} [SemilatticeSup α] (anchor : α) : { a : α // a ≤ anchor } ↪o Node anchor

The order embedding of the principal lower set of the anchor into the lower layer.

Equations

• EGZ.TwoLayer.lowerEmbedding anchor = { toFun := fun (a : { a : α // a ≤ anchor }) => EGZ.TwoLayer.lower anchor ↑a ⋯, inj' := ⋯, map_rel_iff' := ⋯ }

noncomputable def EGZ.TwoLayer.layerEquiv {α : Type u_1} [SemilatticeSup α] (anchor : α) : α ⊕ { a : α // a ≤ anchor } ≃ Node anchor

Every layered node is uniquely either an upper copy or a lower copy.

Equations

• One or more equations did not get rendered due to their size.

theorem EGZ.TwoLayer.card_nodes {α : Type u_1} [SemilatticeSup α] [Fintype α] (anchor : α) : Fintype.card (Node anchor) = Fintype.card α + Fintype.card { a : α // a ≤ anchor }

theorem EGZ.TwoLayer.card_nodes_le {α : Type u_1} [SemilatticeSup α] [Fintype α] (anchor : α) : Fintype.card (Node anchor) ≤ 2 * Fintype.card α

theorem EGZ.TwoLayer.sum_nodes {α : Type u_1} [SemilatticeSup α] [Fintype α] {M : Type u_2} [AddCommMonoid M] (anchor : α) (g : Node anchor → M) : ∑ a : Node anchor, g a = ∑ a : α, g (upper anchor a) + ∑ a : { a : α // a ≤ anchor }, g (lower anchor ↑a ⋯)

Split a sum over layered nodes into upper and lower contributions.

theorem EGZ.TwoLayer.sum_below_eq {α : Type u_1} [SemilatticeSup α] [Fintype α] {M : Type u_2} [AddCommMonoid M] (anchor : α) (g : α → M) : ∑ a : { a : α // a ≤ anchor }, g ↑a = ∑ a : α, if a ≤ anchor then g a else 0

noncomputable def EGZ.TwoLayer.splitWeight {α : Type u_1} [SemilatticeSup α] {β : Type u_2} (anchor : α) (w : α → β → ℕ) (S : β → Prop) (a : Node anchor) (v : β) : ℕ

Move selected atoms below the anchor into the lower layer.

Equations

• EGZ.TwoLayer.splitWeight anchor w S a v = if (↑a).2 = 0 then if S v then w (↑a).1 v else 0 else if (↑a).1 ≤ anchor ∧ S v then 0 else w (↑a).1 v

@[simp]

theorem EGZ.TwoLayer.splitWeight_upper {α : Type u_1} [SemilatticeSup α] {β : Type u_2} (anchor : α) (w : α → β → ℕ) (S : β → Prop) (a : α) (v : β) : splitWeight anchor w S (upper anchor a) v = if a ≤ anchor ∧ S v then 0 else w a v

@[simp]

theorem EGZ.TwoLayer.splitWeight_lower {α : Type u_1} [SemilatticeSup α] {β : Type u_2} (anchor : α) (w : α → β → ℕ) (S : β → Prop) (a : α) (ha : a ≤ anchor) (v : β) : splitWeight anchor w S (lower anchor a ha) v = if S v then w a v else 0

theorem EGZ.TwoLayer.splitWeight_le {α : Type u_1} [SemilatticeSup α] {β : Type u_2} (anchor : α) (w : α → β → ℕ) (S : β → Prop) (a : Node anchor) (v : β) : splitWeight anchor w S a v ≤ w ((projection anchor) a) v

theorem EGZ.TwoLayer.exists_splitWeight_eq {α : Type u_1} [SemilatticeSup α] {β : Type u_2} (anchor : α) (w : α → β → ℕ) (S : β → Prop) (a : α) (v : β) : ∃ (b : Node anchor), (projection anchor) b = a ∧ splitWeight anchor w S b v = w a v

Every old atom retains its full weight at one of the two copies.

theorem EGZ.TwoLayer.sum_splitWeight {α : Type u_1} [SemilatticeSup α] {β : Type u_2} [Fintype α] (anchor : α) (w : α → β → ℕ) (S : β → Prop) (v : β) : ∑ a : Node anchor, splitWeight anchor w S a v = ∑ a : α, w a v

Splitting atoms between the two layers preserves every retained weight.

noncomputable def EGZ.TwoLayer.cumulativeWeight {α : Type u_1} [SemilatticeSup α] {β : Type u_2} [Fintype α] (w : α → β → ℕ) (a : α) (v : β) : ℕ

Cumulative weight in an arbitrary finite node order.

Equations

• EGZ.TwoLayer.cumulativeWeight w a v = ∑ b : α, if b ≤ a then w b v else 0

theorem EGZ.TwoLayer.cumulativeWeight_upper {α : Type u_1} [SemilatticeSup α] {β : Type u_2} [Fintype α] (anchor : α) (w : α → β → ℕ) (S : β → Prop) (a : α) (v : β) : cumulativeWeight (splitWeight anchor w S) (upper anchor a) v = cumulativeWeight w a v

Every upper node retains its entire old cumulative weight.

theorem EGZ.TwoLayer.cumulativeWeight_lower {α : Type u_1} [SemilatticeSup α] {β : Type u_2} [Fintype α] (anchor : α) (w : α → β → ℕ) (S : β → Prop) (a : α) (ha : a ≤ anchor) (v : β) : cumulativeWeight (splitWeight anchor w S) (lower anchor a ha) v = if S v then cumulativeWeight w a v else 0

A lower node has precisely the selected part of its old cumulative weight.

theorem EGZ.TwoLayer.cumulativeWeight_projection_le {α : Type u_1} [SemilatticeSup α] {β : Type u_2} [Fintype α] (anchor : α) (w : α → β → ℕ) (S : β → Prop) (a : Node anchor) (v : β) : cumulativeWeight (splitWeight anchor w S) a v ≤ cumulativeWeight w ((projection anchor) a) v

Every layered cumulative weight is bounded by its old projected weight.