Minimal and reduced face refinements

Minimalizing the active face split and then restricting to reduced nodes keeps the upper anchor for every proper selected face of a reduced old node. This gives a normalized operation with unchanged mass and uniform bounds.

theorem EGZ.FlagDecomposition.Rechart.decomposition_isReducedElement_iff {p d : ℕ} [NeZero p] [Fact (Nat.Prime p)] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) (C : (x : Φ.flag.Node) → IntegerLatticeChart (Φ.liftedSupport x)) (hp : Odd p) (hmod : ∀ (x : Φ.flag.Node), Function.Injective ⇑((chart Φ C x).modp p)) (hcenter : ∀ (x : Φ.flag.Node), ∀ q ∈ (C x).coordinateSupport, IsCenteredLift p q) (x : Φ.flag.Node) : (decomposition Φ C hp hmod hcenter).IsReducedElement x ↔ Φ.IsReducedElement x

@[reducible, inline]

noncomputable abbrev EGZ.FlagDecomposition.FaceRefinement.minimalized {p d : ℕ} [NeZero p] [Fact (Nat.Prime p)] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) (anchor : Φ.flag.Node) (Γ : (Φ.flag.polytope anchor).Face) (hp : Odd p) (C : (x : (decomposition Φ anchor (Φ.faceSelector anchor Γ) hp).flag.Node) → IntegerLatticeChart ((decomposition Φ anchor (Φ.faceSelector anchor Γ) hp).liftedSupport x)) (hmod : ∀ (x : (decomposition Φ anchor (Φ.faceSelector anchor Γ) hp).flag.Node), Function.Injective ⇑((Rechart.chart (decomposition Φ anchor (Φ.faceSelector anchor Γ) hp) C x).modp p)) (hcenter : ∀ (x : (decomposition Φ anchor (Φ.faceSelector anchor Γ) hp).flag.Node), ∀ q ∈ (C x).coordinateSupport, IsCenteredLift p q) : FlagDecomposition p d f

The face refinement expressed in minimal integer lattice charts.

Equations

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

@[reducible, inline]

noncomputable abbrev EGZ.FlagDecomposition.FaceRefinement.normalized {p d : ℕ} [NeZero p] [Fact (Nat.Prime p)] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) (anchor : Φ.flag.Node) (Γ : (Φ.flag.polytope anchor).Face) (hp : Odd p) (C : (x : (decomposition Φ anchor (Φ.faceSelector anchor Γ) hp).flag.Node) → IntegerLatticeChart ((decomposition Φ anchor (Φ.faceSelector anchor Γ) hp).liftedSupport x)) (hmod : ∀ (x : (decomposition Φ anchor (Φ.faceSelector anchor Γ) hp).flag.Node), Function.Injective ⇑((Rechart.chart (decomposition Φ anchor (Φ.faceSelector anchor Γ) hp) C x).modp p)) (hcenter : ∀ (x : (decomposition Φ anchor (Φ.faceSelector anchor Γ) hp).flag.Node), ∀ q ∈ (C x).coordinateSupport, IsCenteredLift p q) : FlagDecomposition p d f

The minimalized face refinement after reduction.

Equations

• EGZ.FlagDecomposition.FaceRefinement.normalized Φ anchor Γ hp C hmod hcenter = (EGZ.FlagDecomposition.FaceRefinement.minimalized Φ anchor Γ hp C hmod hcenter).reduced hp

theorem EGZ.FlagDecomposition.FaceRefinement.minimalized_upperAnchor_isReduced {p d : ℕ} [NeZero p] [Fact (Nat.Prime p)] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) (anchor : Φ.flag.Node) (Γ : (Φ.flag.polytope anchor).Face) (hp : Odd p) (C : (x : (decomposition Φ anchor (Φ.faceSelector anchor Γ) hp).flag.Node) → IntegerLatticeChart ((decomposition Φ anchor (Φ.faceSelector anchor Γ) hp).liftedSupport x)) (hmod : ∀ (x : (decomposition Φ anchor (Φ.faceSelector anchor Γ) hp).flag.Node), Function.Injective ⇑((Rechart.chart (decomposition Φ anchor (Φ.faceSelector anchor Γ) hp) C x).modp p)) (hcenter : ∀ (x : (decomposition Φ anchor (Φ.faceSelector anchor Γ) hp).flag.Node), ∀ q ∈ (C x).coordinateSupport, IsCenteredLift p q) (hΓ : Γ ≠ ⊤) (hred : Φ.IsReducedElement anchor) : (minimalized Φ anchor Γ hp C hmod hcenter).IsReducedElement (upper Φ anchor (Φ.faceSelector anchor Γ) hp anchor)

@[reducible, inline]

noncomputable abbrev EGZ.FlagDecomposition.FaceRefinement.normalizedTargetNode {p d : ℕ} [NeZero p] [Fact (Nat.Prime p)] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) (anchor : Φ.flag.Node) (Γ : (Φ.flag.polytope anchor).Face) (hp : Odd p) (C : (x : (decomposition Φ anchor (Φ.faceSelector anchor Γ) hp).flag.Node) → IntegerLatticeChart ((decomposition Φ anchor (Φ.faceSelector anchor Γ) hp).liftedSupport x)) (hmod : ∀ (x : (decomposition Φ anchor (Φ.faceSelector anchor Γ) hp).flag.Node), Function.Injective ⇑((Rechart.chart (decomposition Φ anchor (Φ.faceSelector anchor Γ) hp) C x).modp p)) (hcenter : ∀ (x : (decomposition Φ anchor (Φ.faceSelector anchor Γ) hp).flag.Node), ∀ q ∈ (C x).coordinateSupport, IsCenteredLift p q) (hΓ : Γ ≠ ⊤) (hred : Φ.IsReducedElement anchor) : (normalized Φ anchor Γ hp C hmod hcenter).flag.Node

The retained upper copy of the anchor in the normalized face refinement.

Equations

• EGZ.FlagDecomposition.FaceRefinement.normalizedTargetNode Φ anchor Γ hp C hmod hcenter hΓ hred = ⟨EGZ.FlagDecomposition.FaceRefinement.upper Φ anchor (Φ.faceSelector anchor Γ) hp anchor, ⋯⟩

noncomputable def EGZ.FlagDecomposition.FaceRefinement.normalizedTargetFace {p d : ℕ} [NeZero p] [Fact (Nat.Prime p)] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) (anchor : Φ.flag.Node) (Γ : (Φ.flag.polytope anchor).Face) (hp : Odd p) (C : (x : (decomposition Φ anchor (Φ.faceSelector anchor Γ) hp).flag.Node) → IntegerLatticeChart ((decomposition Φ anchor (Φ.faceSelector anchor Γ) hp).liftedSupport x)) (hmod : ∀ (x : (decomposition Φ anchor (Φ.faceSelector anchor Γ) hp).flag.Node), Function.Injective ⇑((Rechart.chart (decomposition Φ anchor (Φ.faceSelector anchor Γ) hp) C x).modp p)) (hcenter : ∀ (x : (decomposition Φ anchor (Φ.faceSelector anchor Γ) hp).flag.Node), ∀ q ∈ (C x).coordinateSupport, IsCenteredLift p q) (hΓ : Γ ≠ ⊤) (hred : Φ.IsReducedElement anchor) : ((normalized Φ anchor Γ hp C hmod hcenter).flag.polytope (normalizedTargetNode Φ anchor Γ hp C hmod hcenter hΓ hred)).Face

The face corresponding to the original target face in normalized coordinates.

Equations

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

theorem EGZ.FlagDecomposition.FaceRefinement.normalizedTargetFace_isRealized {p d : ℕ} [NeZero p] [Fact (Nat.Prime p)] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) (anchor : Φ.flag.Node) (Γ : (Φ.flag.polytope anchor).Face) (hp : Odd p) (C : (x : (decomposition Φ anchor (Φ.faceSelector anchor Γ) hp).flag.Node) → IntegerLatticeChart ((decomposition Φ anchor (Φ.faceSelector anchor Γ) hp).liftedSupport x)) (hmod : ∀ (x : (decomposition Φ anchor (Φ.faceSelector anchor Γ) hp).flag.Node), Function.Injective ⇑((Rechart.chart (decomposition Φ anchor (Φ.faceSelector anchor Γ) hp) C x).modp p)) (hcenter : ∀ (x : (decomposition Φ anchor (Φ.faceSelector anchor Γ) hp).flag.Node), ∀ q ∈ (C x).coordinateSupport, IsCenteredLift p q) (hΓ : Γ ≠ ⊤) (hred : Φ.IsReducedElement anchor) : (normalized Φ anchor Γ hp C hmod hcenter).IsRealizedFace (normalizedTargetNode Φ anchor Γ hp C hmod hcenter hΓ hred) (normalizedTargetFace Φ anchor Γ hp C hmod hcenter hΓ hred)

theorem EGZ.FlagDecomposition.FaceRefinement.normalized_isMinimal {p d : ℕ} [NeZero p] [Fact (Nat.Prime p)] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) (anchor : Φ.flag.Node) (Γ : (Φ.flag.polytope anchor).Face) (hp : Odd p) (C : (x : (decomposition Φ anchor (Φ.faceSelector anchor Γ) hp).flag.Node) → IntegerLatticeChart ((decomposition Φ anchor (Φ.faceSelector anchor Γ) hp).liftedSupport x)) (hmod : ∀ (x : (decomposition Φ anchor (Φ.faceSelector anchor Γ) hp).flag.Node), Function.Injective ⇑((Rechart.chart (decomposition Φ anchor (Φ.faceSelector anchor Γ) hp) C x).modp p)) (hcenter : ∀ (x : (decomposition Φ anchor (Φ.faceSelector anchor Γ) hp).flag.Node), ∀ q ∈ (C x).coordinateSupport, IsCenteredLift p q) : (normalized Φ anchor Γ hp C hmod hcenter).IsMinimal

theorem EGZ.FlagDecomposition.FaceRefinement.normalized_isReduced {p d : ℕ} [NeZero p] [Fact (Nat.Prime p)] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) (anchor : Φ.flag.Node) (Γ : (Φ.flag.polytope anchor).Face) (hp : Odd p) (C : (x : (decomposition Φ anchor (Φ.faceSelector anchor Γ) hp).flag.Node) → IntegerLatticeChart ((decomposition Φ anchor (Φ.faceSelector anchor Γ) hp).liftedSupport x)) (hmod : ∀ (x : (decomposition Φ anchor (Φ.faceSelector anchor Γ) hp).flag.Node), Function.Injective ⇑((Rechart.chart (decomposition Φ anchor (Φ.faceSelector anchor Γ) hp) C x).modp p)) (hcenter : ∀ (x : (decomposition Φ anchor (Φ.faceSelector anchor Γ) hp).flag.Node), ∀ q ∈ (C x).coordinateSupport, IsCenteredLift p q) : (normalized Φ anchor Γ hp C hmod hcenter).IsReduced

theorem EGZ.FlagDecomposition.FaceRefinement.normalized_retainedMass {p d : ℕ} [NeZero p] [Fact (Nat.Prime p)] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) (anchor : Φ.flag.Node) (Γ : (Φ.flag.polytope anchor).Face) (hp : Odd p) (C : (x : (decomposition Φ anchor (Φ.faceSelector anchor Γ) hp).flag.Node) → IntegerLatticeChart ((decomposition Φ anchor (Φ.faceSelector anchor Γ) hp).liftedSupport x)) (hmod : ∀ (x : (decomposition Φ anchor (Φ.faceSelector anchor Γ) hp).flag.Node), Function.Injective ⇑((Rechart.chart (decomposition Φ anchor (Φ.faceSelector anchor Γ) hp) C x).modp p)) (hcenter : ∀ (x : (decomposition Φ anchor (Φ.faceSelector anchor Γ) hp).flag.Node), ∀ q ∈ (C x).coordinateSupport, IsCenteredLift p q) : (normalized Φ anchor Γ hp C hmod hcenter).retainedMass = Φ.retainedMass

theorem EGZ.FlagDecomposition.FaceRefinement.normalized_card_le {p d : ℕ} [NeZero p] [Fact (Nat.Prime p)] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) (anchor : Φ.flag.Node) (Γ : (Φ.flag.polytope anchor).Face) (hp : Odd p) (C : (x : (decomposition Φ anchor (Φ.faceSelector anchor Γ) hp).flag.Node) → IntegerLatticeChart ((decomposition Φ anchor (Φ.faceSelector anchor Γ) hp).liftedSupport x)) (hmod : ∀ (x : (decomposition Φ anchor (Φ.faceSelector anchor Γ) hp).flag.Node), Function.Injective ⇑((Rechart.chart (decomposition Φ anchor (Φ.faceSelector anchor Γ) hp) C x).modp p)) (hcenter : ∀ (x : (decomposition Φ anchor (Φ.faceSelector anchor Γ) hp).flag.Node), ∀ q ∈ (C x).coordinateSupport, IsCenteredLift p q) : Fintype.card (normalized Φ anchor Γ hp C hmod hcenter).flag.Node ≤ 2 * Fintype.card Φ.flag.Node

theorem EGZ.FlagDecomposition.FaceRefinement.normalized_isKBounded {p d : ℕ} [NeZero p] [Fact (Nat.Prime p)] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) (anchor : Φ.flag.Node) (Γ : (Φ.flag.polytope anchor).Face) (hp : Odd p) (C : (x : (decomposition Φ anchor (Φ.faceSelector anchor Γ) hp).flag.Node) → IntegerLatticeChart ((decomposition Φ anchor (Φ.faceSelector anchor Γ) hp).liftedSupport x)) (hmod : ∀ (x : (decomposition Φ anchor (Φ.faceSelector anchor Γ) hp).flag.Node), Function.Injective ⇑((Rechart.chart (decomposition Φ anchor (Φ.faceSelector anchor Γ) hp) C x).modp p)) (hcenter : ∀ (x : (decomposition Φ anchor (Φ.faceSelector anchor Γ) hp).flag.Node), ∀ q ∈ (C x).coordinateSupport, IsCenteredLift p q) {K B : ℕ} (hK : Φ.IsKBounded fun (x : Φ.flag.Node) => K) (hC : ∀ (x : (decomposition Φ anchor (Φ.faceSelector anchor Γ) hp).flag.Node) (q : IntCoord (C x).rank), latticeSupNorm ((C x).map q) ≤ K → latticeSupNorm q ≤ B) : (normalized Φ anchor Γ hp C hmod hcenter).IsKBounded fun (x : (normalized Φ anchor Γ hp C hmod hcenter).flag.Node) => B

noncomputable def EGZ.FlagDecomposition.FaceRefinement.normalizedSubdivisionMap {p d : ℕ} [NeZero p] [Fact (Nat.Prime p)] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) (anchor : Φ.flag.Node) (Γ : (Φ.flag.polytope anchor).Face) (hp : Odd p) (C : (x : (decomposition Φ anchor (Φ.faceSelector anchor Γ) hp).flag.Node) → IntegerLatticeChart ((decomposition Φ anchor (Φ.faceSelector anchor Γ) hp).liftedSupport x)) (hmod : ∀ (x : (decomposition Φ anchor (Φ.faceSelector anchor Γ) hp).flag.Node), Function.Injective ⇑((Rechart.chart (decomposition Φ anchor (Φ.faceSelector anchor Γ) hp) C x).modp p)) (hcenter : ∀ (x : (decomposition Φ anchor (Φ.faceSelector anchor Γ) hp).flag.Node), ∀ q ∈ (C x).coordinateSupport, IsCenteredLift p q) : Φ.SubdivisionMap (normalized Φ anchor Γ hp C hmod hcenter)

The subdivision map from the original decomposition to the normalized face refinement.

Equations

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

@[simp]

theorem EGZ.FlagDecomposition.FaceRefinement.normalizedTargetNode_projection {p d : ℕ} [NeZero p] [Fact (Nat.Prime p)] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) (anchor : Φ.flag.Node) (Γ : (Φ.flag.polytope anchor).Face) (hp : Odd p) (C : (x : (decomposition Φ anchor (Φ.faceSelector anchor Γ) hp).flag.Node) → IntegerLatticeChart ((decomposition Φ anchor (Φ.faceSelector anchor Γ) hp).liftedSupport x)) (hmod : ∀ (x : (decomposition Φ anchor (Φ.faceSelector anchor Γ) hp).flag.Node), Function.Injective ⇑((Rechart.chart (decomposition Φ anchor (Φ.faceSelector anchor Γ) hp) C x).modp p)) (hcenter : ∀ (x : (decomposition Φ anchor (Φ.faceSelector anchor Γ) hp).flag.Node), ∀ q ∈ (C x).coordinateSupport, IsCenteredLift p q) (hΓ : Γ ≠ ⊤) (hred : Φ.IsReducedElement anchor) : (normalizedSubdivisionMap Φ anchor Γ hp C hmod hcenter).node (normalizedTargetNode Φ anchor Γ hp C hmod hcenter hΓ hred) = anchor

theorem EGZ.FlagDecomposition.FaceRefinement.normalizedTargetFace_carrier {p d : ℕ} [NeZero p] [Fact (Nat.Prime p)] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) (anchor : Φ.flag.Node) (Γ : (Φ.flag.polytope anchor).Face) (hp : Odd p) (C : (x : (decomposition Φ anchor (Φ.faceSelector anchor Γ) hp).flag.Node) → IntegerLatticeChart ((decomposition Φ anchor (Φ.faceSelector anchor Γ) hp).liftedSupport x)) (hmod : ∀ (x : (decomposition Φ anchor (Φ.faceSelector anchor Γ) hp).flag.Node), Function.Injective ⇑((Rechart.chart (decomposition Φ anchor (Φ.faceSelector anchor Γ) hp) C x).modp p)) (hcenter : ∀ (x : (decomposition Φ anchor (Φ.faceSelector anchor Γ) hp).flag.Node), ∀ q ∈ (C x).coordinateSupport, IsCenteredLift p q) (hΓ : Γ ≠ ⊤) (hred : Φ.IsReducedElement anchor) : (normalizedTargetFace Φ anchor Γ hp C hmod hcenter hΓ hred).carrier = ((normalized Φ anchor Γ hp C hmod hcenter).flag.polytope (normalizedTargetNode Φ anchor Γ hp C hmod hcenter hΓ hred)).carrier ∩ ⇑((normalizedSubdivisionMap Φ anchor Γ hp C hmod hcenter).fibre (normalizedTargetNode Φ anchor Γ hp C hmod hcenter hΓ hred)) ⁻¹' Γ.carrier

The realized target face is exactly the pullback of the selected old face through the normalized subdivision, including its polytope constraint.

theorem EGZ.FlagDecomposition.FaceRefinement.normalized_isRealizedFace {p d : ℕ} [NeZero p] [Fact (Nat.Prime p)] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) (anchor : Φ.flag.Node) (Γ : (Φ.flag.polytope anchor).Face) (hp : Odd p) (C : (x : (decomposition Φ anchor (Φ.faceSelector anchor Γ) hp).flag.Node) → IntegerLatticeChart ((decomposition Φ anchor (Φ.faceSelector anchor Γ) hp).liftedSupport x)) (hmod : ∀ (x : (decomposition Φ anchor (Φ.faceSelector anchor Γ) hp).flag.Node), Function.Injective ⇑((Rechart.chart (decomposition Φ anchor (Φ.faceSelector anchor Γ) hp) C x).modp p)) (hcenter : ∀ (x : (decomposition Φ anchor (Φ.faceSelector anchor Γ) hp).flag.Node), ∀ q ∈ (C x).coordinateSupport, IsCenteredLift p q) (x : (normalized Φ anchor Γ hp C hmod hcenter).flag.Node) (Δ : (Φ.flag.polytope ((normalizedSubdivisionMap Φ anchor Γ hp C hmod hcenter).node x)).Face) (hne : (((normalized Φ anchor Γ hp C hmod hcenter).flag.polytope x).carrier ∩ ⇑((normalizedSubdivisionMap Φ anchor Γ hp C hmod hcenter).fibre x) ⁻¹' Δ.carrier).Nonempty) (hΔ : Φ.IsRealizedFace ((normalizedSubdivisionMap Φ anchor Γ hp C hmod hcenter).node x) Δ) : (normalized Φ anchor Γ hp C hmod hcenter).IsRealizedFace x ((normalizedSubdivisionMap Φ anchor Γ hp C hmod hcenter).face x Δ hne)

theorem EGZ.normalized_face_refinement_lemma (d : ℕ) : ∃ (A : ℕ → ℕ), Monotone A ∧ (∀ (K : ℕ), K ≤ A K) ∧ ∀ (K : ℕ), ∃ (p₀ : ℕ), 2 ≤ p₀ ∧ ∀ (p : ℕ) [inst : NeZero p] [inst_1 : Fact (Nat.Prime p)], p₀ < p → ∀ (f : FpCoord p d → ℕ) (Φ : FlagDecomposition p d f) (anchor : Φ.flag.Node) (Γ : (Φ.flag.polytope anchor).Face) (hΓ : Γ ≠ ⊤) (hred : Φ.IsReducedElement anchor), (Φ.IsKBounded fun (x : Φ.flag.Node) => K) → ∃ (hp : Odd p) (C : (x : (FlagDecomposition.FaceRefinement.decomposition Φ anchor (Φ.faceSelector anchor Γ) hp).flag.Node) → IntegerLatticeChart ((FlagDecomposition.FaceRefinement.decomposition Φ anchor (Φ.faceSelector anchor Γ) hp).liftedSupport x)) (hmod : ∀ (x : (FlagDecomposition.FaceRefinement.decomposition Φ anchor (Φ.faceSelector anchor Γ) hp).flag.Node), Function.Injective ⇑((FlagDecomposition.Rechart.chart (FlagDecomposition.FaceRefinement.decomposition Φ anchor (Φ.faceSelector anchor Γ) hp) C x).modp p)) (hcenter : ∀ (x : (FlagDecomposition.FaceRefinement.decomposition Φ anchor (Φ.faceSelector anchor Γ) hp).flag.Node), ∀ q ∈ (C x).coordinateSupport, IsCenteredLift p q), let Ψ := FlagDecomposition.FaceRefinement.normalized Φ anchor Γ hp C hmod hcenter; Ψ.IsMinimal ∧ Ψ.IsReduced ∧ (Ψ.IsKBounded fun (x : Ψ.flag.Node) => A K) ∧ Ψ.retainedMass = Φ.retainedMass ∧ Fintype.card Ψ.flag.Node ≤ 2 * Fintype.card Φ.flag.Node ∧ Ψ.IsRealizedFace (FlagDecomposition.FaceRefinement.normalizedTargetNode Φ anchor Γ hp C hmod hcenter hΓ hred) (FlagDecomposition.FaceRefinement.normalizedTargetFace Φ anchor Γ hp C hmod hcenter hΓ hred)

Uniform normalization of a proper-face refinement at a reduced node. The new radius depends only on the original radius and ambient dimension.