Realizing a face by splitting local weights #

The positive generators of a proper point over an exposed face also lie over that face. This allows a refinement that moves the selected local atoms to a lower layer to realize the face while retaining the old upper fibres.

source

theorem EGZ.ConvexFlag.ConvexCombination.mem_face_of_pos {F : ConvexFlag} {I : Type u_1} [Fintype I] {points : I → F.Point} {weight : I → ℝ} {result : F.Point} (c : ConvexCombination points weight result) {x : F.Node} (hx : result.base ≤ x) (Γ : (F.polytope x).Face) (hΓ : result.coord hx ∈ Γ.carrier) {i : I} (hi : 0 < weight i) :

(points i).coord ⋯ ∈ Γ.carrier

Every positively weighted generator of a flag combination lies on any upper face containing the combination.

source

theorem EGZ.FlagDecomposition.faceIndex_le_of_local_bases {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) (x : Φ.flag.Node) (Γ : (Φ.flag.polytope x).Face) (b : Φ.flag.Node) (hlocal : ∀ q ∈ Φ.omegaZero, ∀ (h : q.base ≤ x), q.coord h ∈ Γ.carrier → q.base ≤ b) :

Φ.faceIndex x Γ ≤ b

Bounding the bases of the local generators over a face bounds its face index. The same bound passes to every proper convex combination.

source

theorem EGZ.FlagDecomposition.isRealizedFace_of_local_bases {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) (x : Φ.flag.Node) (Γ : (Φ.flag.polytope x).Face) (b : Φ.flag.Node) (hb : b ≤ x) (hlocal : ∀ q ∈ Φ.omegaZero, ∀ (h : q.base ≤ x), q.coord h ∈ Γ.carrier → q.base ≤ b) (hpoly : ∀ q ∈ (Φ.flag.polytope b).carrier, (Φ.flag.transition hb).real q ∈ Γ.carrier) :

Φ.IsRealizedFace x Γ

A node containing every local-generator base over a face realizes the face as soon as its whole polytope maps into that face.

source

def EGZ.FlagDecomposition.FaceRefinement.projection {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) (anchor : Φ.flag.Node) :

TwoLayer.Node anchor →o Φ.flag.Node

The layer-forgetting order map.

Equations

EGZ.FlagDecomposition.FaceRefinement.projection Φ anchor = { toFun := ⇑(EGZ.TwoLayer.projection anchor), monotone' := ⋯ }

Instances For

source

@[reducible, inline]

noncomputable abbrev EGZ.FlagDecomposition.FaceRefinement.splitWeights {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) (anchor : Φ.flag.Node) (selected : FpCoord p d → Prop) :

Φ.SplitWeights (projection Φ anchor)

Split the local atoms selected below the anchor into lower copies.

Equations

EGZ.FlagDecomposition.FaceRefinement.splitWeights Φ anchor selected = { weight := EGZ.TwoLayer.splitWeight anchor Φ.localWeight selected, weight_le := ⋯, nonzero := ⋯, retained_le := ⋯ }

Instances For

source

@[simp]

theorem EGZ.FlagDecomposition.FaceRefinement.cumulative_upper {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) (anchor : Φ.flag.Node) (selected : FpCoord p d → Prop) (x : Φ.flag.Node) (v : FpCoord p d) :

(splitWeights Φ anchor selected).cumulative (TwoLayer.upper anchor x) v = Φ.cumulativeWeight x v

source

@[simp]

theorem EGZ.FlagDecomposition.FaceRefinement.cumulative_lower {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) (anchor : Φ.flag.Node) (selected : FpCoord p d → Prop) (x : Φ.flag.Node) (hx : x ≤ anchor) (v : FpCoord p d) :

(splitWeights Φ anchor selected).cumulative (TwoLayer.lower anchor x hx) v = if selected v then Φ.cumulativeWeight x v else 0

source

@[simp]

theorem EGZ.FlagDecomposition.FaceRefinement.hat_upper {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) (anchor : Φ.flag.Node) (selected : FpCoord p d → Prop) (x : Φ.flag.Node) (q : IntCoord (Φ.flag.rank x)) :

(splitWeights Φ anchor selected).hat (TwoLayer.upper anchor x) q = Φ.hat x q

source

@[reducible, inline]

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

FlagDecomposition p d f

Rebuild the selected split on its active nodes.

Equations

EGZ.FlagDecomposition.FaceRefinement.decomposition Φ anchor selected hp = (EGZ.FlagDecomposition.FaceRefinement.splitWeights Φ anchor selected).decomposition hp

Instances For

source

theorem EGZ.FlagDecomposition.FaceRefinement.active_upper {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) (anchor : Φ.flag.Node) (selected : FpCoord p d → Prop) (hp : Odd p) (x : Φ.flag.Node) :

⋯.Active (TwoLayer.upper anchor x)

Every old node survives in the upper layer.

source

theorem EGZ.FlagDecomposition.FaceRefinement.active_lower {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) (anchor : Φ.flag.Node) (selected : FpCoord p d → Prop) (hp : Odd p) (x : Φ.flag.Node) (hx : x ≤ anchor) (v : FpCoord p d) (hv : Φ.cumulativeWeight x v ≠ 0) (hselected : selected v) :

⋯.Active (TwoLayer.lower anchor x hx)

A lower node is active whenever its old cumulative mass contains a selected atom.

source

noncomputable def EGZ.FlagDecomposition.FaceRefinement.upper {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) (anchor : Φ.flag.Node) (selected : FpCoord p d → Prop) (hp : Odd p) (x : Φ.flag.Node) :

(decomposition Φ anchor selected hp).flag.Node

The active upper copy of an old node.

Equations

EGZ.FlagDecomposition.FaceRefinement.upper Φ anchor selected hp x = ⟨EGZ.TwoLayer.upper anchor x, ⋯⟩

Instances For

source

noncomputable def EGZ.FlagDecomposition.FaceRefinement.upperOrderEmbedding {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) (anchor : Φ.flag.Node) (selected : FpCoord p d → Prop) (hp : Odd p) :

Φ.flag.Node ↪o (decomposition Φ anchor selected hp).flag.Node

The original node order embeds into the active upper layer.

Equations

EGZ.FlagDecomposition.FaceRefinement.upperOrderEmbedding Φ anchor selected hp = { toFun := EGZ.FlagDecomposition.FaceRefinement.upper Φ anchor selected hp, inj' := ⋯, map_rel_iff' := ⋯ }

Instances For

source

theorem EGZ.FlagDecomposition.FaceRefinement.upper_cumulativeWeight {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) (anchor : Φ.flag.Node) (selected : FpCoord p d → Prop) (hp : Odd p) (x : Φ.flag.Node) :

(decomposition Φ anchor selected hp).cumulativeWeight (upper Φ anchor selected hp x) = Φ.cumulativeWeight x

source

@[simp]

theorem EGZ.FlagDecomposition.FaceRefinement.upper_hat {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) (anchor : Φ.flag.Node) (selected : FpCoord p d → Prop) (hp : Odd p) (x : Φ.flag.Node) (q : IntCoord (Φ.flag.rank x)) :

(decomposition Φ anchor selected hp).hat (upper Φ anchor selected hp x) q = Φ.hat x q

source

@[simp]

theorem EGZ.FlagDecomposition.FaceRefinement.upper_space {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) (anchor : Φ.flag.Node) (selected : FpCoord p d → Prop) (hp : Odd p) (x : Φ.flag.Node) :

(decomposition Φ anchor selected hp).representation.space (upper Φ anchor selected hp x) = Φ.representation.space x

source

@[simp]

theorem EGZ.FlagDecomposition.FaceRefinement.upper_map {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) (anchor : Φ.flag.Node) (selected : FpCoord p d → Prop) (hp : Odd p) (x : Φ.flag.Node) :

(decomposition Φ anchor selected hp).representation.map (upper Φ anchor selected hp x) = Φ.representation.map x

source

@[simp]

theorem EGZ.FlagDecomposition.FaceRefinement.upper_liftedSupport {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) (anchor : Φ.flag.Node) (selected : FpCoord p d → Prop) (hp : Odd p) (x : Φ.flag.Node) :

(decomposition Φ anchor selected hp).liftedSupport (upper Φ anchor selected hp x) = Φ.liftedSupport x

source

@[simp]

theorem EGZ.FlagDecomposition.FaceRefinement.upper_gap {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) (anchor : Φ.flag.Node) (selected : FpCoord p d → Prop) (hp : Odd p) (x : Φ.flag.Node) :

(decomposition Φ anchor selected hp).gap (upper Φ anchor selected hp x) = Φ.gap x

source

theorem EGZ.FlagDecomposition.FaceRefinement.upper_polytope {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) (anchor : Φ.flag.Node) (selected : FpCoord p d → Prop) (hp : Odd p) (x : Φ.flag.Node) :

((decomposition Φ anchor selected hp).flag.polytope (upper Φ anchor selected hp x)).carrier = (Φ.flag.polytope x).carrier

The upper copy retains its original polytope.

source

noncomputable def EGZ.FlagDecomposition.FaceRefinement.upperFace {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) (anchor : Φ.flag.Node) (selected : FpCoord p d → Prop) (hp : Odd p) (x : Φ.flag.Node) (Γ : (Φ.flag.polytope x).Face) :

((decomposition Φ anchor selected hp).flag.polytope (upper Φ anchor selected hp x)).Face

An original face, viewed in its unchanged upper polytope.

Equations

EGZ.FlagDecomposition.FaceRefinement.upperFace Φ anchor selected hp x Γ = { carrier := Γ.carrier, is_exposed := ⋯, nonempty := ⋯ }

Instances For

source

@[simp]

theorem EGZ.FlagDecomposition.FaceRefinement.upperFace_carrier {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) (anchor : Φ.flag.Node) (selected : FpCoord p d → Prop) (hp : Odd p) (x : Φ.flag.Node) (Γ : (Φ.flag.polytope x).Face) :

(upperFace Φ anchor selected hp x Γ).carrier = Γ.carrier

source

theorem EGZ.FlagDecomposition.FaceRefinement.retainedWeight {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) (anchor : Φ.flag.Node) (selected : FpCoord p d → Prop) (hp : Odd p) :

(decomposition Φ anchor selected hp).retainedWeight = Φ.retainedWeight

source

@[simp]

theorem EGZ.FlagDecomposition.FaceRefinement.retainedMass {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) (anchor : Φ.flag.Node) (selected : FpCoord p d → Prop) (hp : Odd p) :

(decomposition Φ anchor selected hp).retainedMass = Φ.retainedMass

source

theorem EGZ.FlagDecomposition.FaceRefinement.card_le {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) (anchor : Φ.flag.Node) (selected : FpCoord p d → Prop) (hp : Odd p) :

Fintype.card (decomposition Φ anchor selected hp).flag.Node ≤ 2 * Fintype.card Φ.flag.Node

At most two copies of each old node survive.

source

theorem EGZ.FlagDecomposition.FaceRefinement.isKBounded {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) (anchor : Φ.flag.Node) (selected : FpCoord p d → Prop) (hp : Odd p) {K : Φ.flag.Node → ℕ} (hK : Φ.IsKBounded K) :

(decomposition Φ anchor selected hp).IsKBounded fun (x : (decomposition Φ anchor selected hp).flag.Node) => K ((projection Φ anchor) ↑x)

Both layers retain the old nodewise coordinate bounds.

source

noncomputable def EGZ.FlagDecomposition.FaceRefinement.subdivisionMap {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) (anchor : Φ.flag.Node) (selected : FpCoord p d → Prop) (hp : Odd p) :

Φ.SubdivisionMap (decomposition Φ anchor selected hp)

Forgetting layers maps the split decomposition into the old one.

Equations

EGZ.FlagDecomposition.FaceRefinement.subdivisionMap Φ anchor selected hp = (EGZ.FlagDecomposition.FaceRefinement.splitWeights Φ anchor selected).subdivisionMap hp ⋯

Instances For

source

theorem EGZ.FlagDecomposition.FaceRefinement.upper_isCompleteElement {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) (anchor : Φ.flag.Node) (selected : FpCoord p d → Prop) (hp : Odd p) (x : Φ.flag.Node) (t : ℕ) (δ : ℝ) (hc : Φ.IsCompleteElement x t δ) :

(decomposition Φ anchor selected hp).IsCompleteElement (upper Φ anchor selected hp x) t δ

Complete upper elements retain the same cumulative weight and representation fibres.

source

theorem EGZ.FlagDecomposition.FaceRefinement.upper_isRealizedFace {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) (anchor : Φ.flag.Node) (selected : FpCoord p d → Prop) (hp : Odd p) (x : Φ.flag.Node) (Γ : (Φ.flag.polytope x).Face) (hΓ : Φ.IsRealizedFace x Γ) :

(decomposition Φ anchor selected hp).IsRealizedFace (upper Φ anchor selected hp x) (upperFace Φ anchor selected hp x Γ)

Realized old faces remain realized at the unchanged upper nodes.

source

theorem EGZ.FlagDecomposition.FaceRefinement.face_hat_lower {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) (anchor : Φ.flag.Node) (hp : Odd p) (Γ : (Φ.flag.polytope anchor).Face) (x : Φ.flag.Node) (hx : x ≤ anchor) (q : IntCoord (Φ.flag.rank x)) :

(splitWeights Φ anchor (Φ.faceSelector anchor Γ)).hat (TwoLayer.lower anchor x hx) q = if (Φ.flag.transition hx).real q.real ∈ Γ.carrier then Φ.hat x q else 0

On the face-selected lower layer, a cumulative lifted fibre is either retained in full or deleted according to its upper transition coordinate.

source

theorem EGZ.FlagDecomposition.FaceRefinement.face_hat_lower_anchor {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) (anchor : Φ.flag.Node) (hp : Odd p) (Γ : (Φ.flag.polytope anchor).Face) (q : IntCoord (Φ.flag.rank anchor)) :

(splitWeights Φ anchor (Φ.faceSelector anchor Γ)).hat (TwoLayer.lower anchor anchor ⋯) q = if q.real ∈ Γ.carrier then Φ.hat anchor q else 0

The lower anchor keeps precisely the lifted support points on its face.

source

theorem EGZ.FlagDecomposition.FaceRefinement.face_local_layer_zero {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) (anchor : Φ.flag.Node) (hp : Odd p) (Γ : (Φ.flag.polytope anchor).Face) (q : (decomposition Φ anchor (Φ.faceSelector anchor Γ) hp).flag.Point) (hq : q ∈ (decomposition Φ anchor (Φ.faceSelector anchor Γ) hp).omegaZero) (h : q.base ≤ upper Φ anchor (Φ.faceSelector anchor Γ) hp anchor) (hface : q.coord h ∈ Γ.carrier) :

(↑↑q.base).2 = 0

A surviving local generator projecting onto the selected face lies in the lower layer: its selected ambient atoms were removed from the upper copy of its base.

source

theorem EGZ.FlagDecomposition.FaceRefinement.face_active_lower_anchor {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) (anchor : Φ.flag.Node) (hp : Odd p) (Γ : (Φ.flag.polytope anchor).Face) :

⋯.Active (TwoLayer.lower anchor anchor ⋯)

Every nonempty face supplies a selected cumulative atom at the lower anchor, so that anchor survives the rebuilding.

source

noncomputable def EGZ.FlagDecomposition.FaceRefinement.lowerAnchor {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) (anchor : Φ.flag.Node) (hp : Odd p) (Γ : (Φ.flag.polytope anchor).Face) :

(decomposition Φ anchor (Φ.faceSelector anchor Γ) hp).flag.Node

The active lower copy of the selected anchor.

Equations

EGZ.FlagDecomposition.FaceRefinement.lowerAnchor Φ anchor hp Γ = ⟨EGZ.TwoLayer.lower anchor anchor ⋯, ⋯⟩

Instances For

source

theorem EGZ.FlagDecomposition.FaceRefinement.lowerAnchor_le_upper {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) (anchor : Φ.flag.Node) (hp : Odd p) (Γ : (Φ.flag.polytope anchor).Face) :

lowerAnchor Φ anchor hp Γ ≤ upper Φ anchor (Φ.faceSelector anchor Γ) hp anchor

source

@[simp]

theorem EGZ.FlagDecomposition.FaceRefinement.lowerAnchor_liftedSupport {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) (anchor : Φ.flag.Node) (hp : Odd p) (Γ : (Φ.flag.polytope anchor).Face) :

(decomposition Φ anchor (Φ.faceSelector anchor Γ) hp).liftedSupport (lowerAnchor Φ anchor hp Γ) = {q ∈ Φ.liftedSupport anchor | q.real ∈ Γ.carrier}

source

theorem EGZ.FlagDecomposition.FaceRefinement.lowerAnchor_polytope {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) (anchor : Φ.flag.Node) (hp : Odd p) (Γ : (Φ.flag.polytope anchor).Face) :

((decomposition Φ anchor (Φ.faceSelector anchor Γ) hp).flag.polytope (lowerAnchor Φ anchor hp Γ)).carrier = Γ.carrier

The new lower anchor polytope is exactly the selected old face.

source

theorem EGZ.FlagDecomposition.FaceRefinement.face_isRealized {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) (anchor : Φ.flag.Node) (hp : Odd p) (Γ : (Φ.flag.polytope anchor).Face) :

(decomposition Φ anchor (Φ.faceSelector anchor Γ) hp).IsRealizedFace (upper Φ anchor (Φ.faceSelector anchor Γ) hp anchor) (upperFace Φ anchor (Φ.faceSelector anchor Γ) hp anchor Γ)

Splitting all atoms over the face into the lower layer realizes that face at the unchanged upper anchor.

source

theorem EGZ.FlagDecomposition.face_refinement_lemma {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) (hp : Odd p) (anchor : Φ.flag.Node) (Γ : (Φ.flag.polytope anchor).Face) {K : Φ.flag.Node → ℕ} (hK : Φ.IsKBounded K) :

let selected := Φ.faceSelector anchor Γ; let Ψ := FaceRefinement.decomposition Φ anchor selected hp; Ψ.retainedWeight = Φ.retainedWeight ∧ Ψ.retainedMass = Φ.retainedMass ∧ Fintype.card Ψ.flag.Node ≤ 2 * Fintype.card Φ.flag.Node ∧ (Ψ.IsKBounded fun (x : Ψ.flag.Node) => K ((FaceRefinement.projection Φ anchor) ↑x)) ∧ (∀ (x : Φ.flag.Node), Ψ.cumulativeWeight (FaceRefinement.upper Φ anchor selected hp x) = Φ.cumulativeWeight x) ∧ (∀ (x : Φ.flag.Node), (Ψ.flag.polytope (FaceRefinement.upper Φ anchor selected hp x)).carrier = (Φ.flag.polytope x).carrier) ∧ (Ψ.flag.polytope (FaceRefinement.lowerAnchor Φ anchor hp Γ)).carrier = Γ.carrier ∧ Ψ.IsRealizedFace (FaceRefinement.upper Φ anchor selected hp anchor) (FaceRefinement.upperFace Φ anchor selected hp anchor Γ) ∧ (∀ (x : Φ.flag.Node) (t : ℕ) (δ : ℝ), Φ.IsCompleteElement x t δ → Ψ.IsCompleteElement (FaceRefinement.upper Φ anchor selected hp x) t δ) ∧ ∀ (x : Φ.flag.Node) (Δ : (Φ.flag.polytope x).Face), Φ.IsRealizedFace x Δ → Ψ.IsRealizedFace (FaceRefinement.upper Φ anchor selected hp x) (FaceRefinement.upperFace Φ anchor selected hp x Δ)

Splitting the atoms over a chosen face realizes it at an upper copy of the anchor. This operation retains every old upper fibre and all mass, uses at most twice as many nodes, and preserves the old coordinate bounds.

Documentation

LeanPool.ErdosGinzburgZiv.EGZ.Decomposition.FaceRefinement

Realizing a face by splitting local weights #