Reduced complete-element refinements #
Restricting the constructed complete-element refinement to its reduced nodes retains the explicit complete representative and removes the old upper anchor. Minimality, all mass bounds, and the subdivision map survive.
@[reducible, inline]
noncomputable abbrev
EGZ.FlagDecomposition.CompletePreparation.normalized
{p d : ℕ}
[Fact (Nat.Prime p)]
{f : FpCoord p d → ℕ}
{Φ : FlagDecomposition p d f}
{anchor : Φ.flag.Node}
{t : ℕ → ℕ}
{δ : ℝ}
(D : Φ.CompletePreparation anchor t δ)
(hp : Odd p)
(hδ : 0 ≤ δ)
(hsmall : 3 ^ (d + 1) * δ < 1)
(C : (x : (D.diagram hp hδ hsmall).Node) → IntegerLatticeChart ((D.diagram hp hδ hsmall).support x))
(hmod :
∀ (x : (D.diagram hp hδ hsmall).Node), Function.Injective ⇑((IntegralAffineMap.ofIntAffineMap (C x).map).modp p))
(hcenter : ∀ (x : (D.diagram hp hδ hsmall).Node), ∀ q ∈ (C x).coordinateSupport, IsCenteredLift p q)
:
FlagDecomposition p d f
The completed refinement after recharting and reduction.
Equations
- D.normalized hp hδ hsmall C hmod hcenter = (D.refined hp hδ hsmall C hmod hcenter).reduced hp
Instances For
@[reducible, inline]
noncomputable abbrev
EGZ.FlagDecomposition.CompletePreparation.normalizedCompleteNode
{p d : ℕ}
[Fact (Nat.Prime p)]
{f : FpCoord p d → ℕ}
{Φ : FlagDecomposition p d f}
{anchor : Φ.flag.Node}
{t : ℕ → ℕ}
{δ : ℝ}
(D : Φ.CompletePreparation anchor t δ)
(hp : Odd p)
(hδ : 0 ≤ δ)
(hsmall : 3 ^ (d + 1) * δ < 1)
(C : (x : (D.diagram hp hδ hsmall).Node) → IntegerLatticeChart ((D.diagram hp hδ hsmall).support x))
(hmod :
∀ (x : (D.diagram hp hδ hsmall).Node), Function.Injective ⇑((IntegralAffineMap.ofIntAffineMap (C x).map).modp p))
(hcenter : ∀ (x : (D.diagram hp hδ hsmall).Node), ∀ q ∈ (C x).coordinateSupport, IsCenteredLift p q)
:
(D.normalized hp hδ hsmall C hmod hcenter).flag.Node
The distinguished complete node retained in the normalized decomposition.
Equations
- D.normalizedCompleteNode hp hδ hsmall C hmod hcenter = ⟨D.completeNode hp hδ hsmall C hmod hcenter, ⋯⟩
Instances For
theorem
EGZ.FlagDecomposition.CompletePreparation.normalized_isMinimal
{p d : ℕ}
[Fact (Nat.Prime p)]
{f : FpCoord p d → ℕ}
{Φ : FlagDecomposition p d f}
{anchor : Φ.flag.Node}
{t : ℕ → ℕ}
{δ : ℝ}
(D : Φ.CompletePreparation anchor t δ)
(hp : Odd p)
(hδ : 0 ≤ δ)
(hsmall : 3 ^ (d + 1) * δ < 1)
(C : (x : (D.diagram hp hδ hsmall).Node) → IntegerLatticeChart ((D.diagram hp hδ hsmall).support x))
(hmod :
∀ (x : (D.diagram hp hδ hsmall).Node), Function.Injective ⇑((IntegralAffineMap.ofIntAffineMap (C x).map).modp p))
(hcenter : ∀ (x : (D.diagram hp hδ hsmall).Node), ∀ q ∈ (C x).coordinateSupport, IsCenteredLift p q)
:
(D.normalized hp hδ hsmall C hmod hcenter).IsMinimal
theorem
EGZ.FlagDecomposition.CompletePreparation.normalized_isReduced
{p d : ℕ}
[Fact (Nat.Prime p)]
{f : FpCoord p d → ℕ}
{Φ : FlagDecomposition p d f}
{anchor : Φ.flag.Node}
{t : ℕ → ℕ}
{δ : ℝ}
(D : Φ.CompletePreparation anchor t δ)
(hp : Odd p)
(hδ : 0 ≤ δ)
(hsmall : 3 ^ (d + 1) * δ < 1)
(C : (x : (D.diagram hp hδ hsmall).Node) → IntegerLatticeChart ((D.diagram hp hδ hsmall).support x))
(hmod :
∀ (x : (D.diagram hp hδ hsmall).Node), Function.Injective ⇑((IntegralAffineMap.ofIntAffineMap (C x).map).modp p))
(hcenter : ∀ (x : (D.diagram hp hδ hsmall).Node), ∀ q ∈ (C x).coordinateSupport, IsCenteredLift p q)
:
(D.normalized hp hδ hsmall C hmod hcenter).IsReduced
theorem
EGZ.FlagDecomposition.CompletePreparation.normalized_retainedMass
{p d : ℕ}
[Fact (Nat.Prime p)]
{f : FpCoord p d → ℕ}
{Φ : FlagDecomposition p d f}
{anchor : Φ.flag.Node}
{t : ℕ → ℕ}
{δ : ℝ}
(D : Φ.CompletePreparation anchor t δ)
(hp : Odd p)
(hδ : 0 ≤ δ)
(hsmall : 3 ^ (d + 1) * δ < 1)
(C : (x : (D.diagram hp hδ hsmall).Node) → IntegerLatticeChart ((D.diagram hp hδ hsmall).support x))
(hmod :
∀ (x : (D.diagram hp hδ hsmall).Node), Function.Injective ⇑((IntegralAffineMap.ofIntAffineMap (C x).map).modp p))
(hcenter : ∀ (x : (D.diagram hp hδ hsmall).Node), ∀ q ∈ (C x).coordinateSupport, IsCenteredLift p q)
:
(D.normalized hp hδ hsmall C hmod hcenter).retainedMass = (D.refined hp hδ hsmall C hmod hcenter).retainedMass
theorem
EGZ.FlagDecomposition.CompletePreparation.normalized_retainedMass_loss_le
{p d : ℕ}
[Fact (Nat.Prime p)]
{f : FpCoord p d → ℕ}
{Φ : FlagDecomposition p d f}
{anchor : Φ.flag.Node}
{t : ℕ → ℕ}
{δ : ℝ}
(D : Φ.CompletePreparation anchor t δ)
(hp : Odd p)
(hδ : 0 ≤ δ)
(hsmall : 3 ^ (d + 1) * δ < 1)
(C : (x : (D.diagram hp hδ hsmall).Node) → IntegerLatticeChart ((D.diagram hp hδ hsmall).support x))
(hmod :
∀ (x : (D.diagram hp hδ hsmall).Node), Function.Injective ⇑((IntegralAffineMap.ofIntAffineMap (C x).map).modp p))
(hcenter : ∀ (x : (D.diagram hp hδ hsmall).Node), ∀ q ∈ (C x).coordinateSupport, IsCenteredLift p q)
:
↑Φ.retainedMass - ↑(D.normalized hp hδ hsmall C hmod hcenter).retainedMass ≤ 3 ^ (d + 1) * δ * ↑(natMass (Φ.cumulativeWeight anchor))
theorem
EGZ.FlagDecomposition.CompletePreparation.normalized_card_le
{p d : ℕ}
[Fact (Nat.Prime p)]
{f : FpCoord p d → ℕ}
{Φ : FlagDecomposition p d f}
{anchor : Φ.flag.Node}
{t : ℕ → ℕ}
{δ : ℝ}
(D : Φ.CompletePreparation anchor t δ)
(hp : Odd p)
(hδ : 0 ≤ δ)
(hsmall : 3 ^ (d + 1) * δ < 1)
(C : (x : (D.diagram hp hδ hsmall).Node) → IntegerLatticeChart ((D.diagram hp hδ hsmall).support x))
(hmod :
∀ (x : (D.diagram hp hδ hsmall).Node), Function.Injective ⇑((IntegralAffineMap.ofIntAffineMap (C x).map).modp p))
(hcenter : ∀ (x : (D.diagram hp hδ hsmall).Node), ∀ q ∈ (C x).coordinateSupport, IsCenteredLift p q)
:
theorem
EGZ.FlagDecomposition.CompletePreparation.normalized_isKBounded
{p d : ℕ}
[Fact (Nat.Prime p)]
{f : FpCoord p d → ℕ}
{Φ : FlagDecomposition p d f}
{anchor : Φ.flag.Node}
{t : ℕ → ℕ}
{δ : ℝ}
(D : Φ.CompletePreparation anchor t δ)
(hp : Odd p)
(hδ : 0 ≤ δ)
(hsmall : 3 ^ (d + 1) * δ < 1)
(C : (x : (D.diagram hp hδ hsmall).Node) → IntegerLatticeChart ((D.diagram hp hδ hsmall).support x))
(hmod :
∀ (x : (D.diagram hp hδ hsmall).Node), Function.Injective ⇑((IntegralAffineMap.ofIntAffineMap (C x).map).modp p))
(hcenter : ∀ (x : (D.diagram hp hδ hsmall).Node), ∀ q ∈ (C x).coordinateSupport, IsCenteredLift p q)
{B : ℕ}
(hB :
(D.refined hp hδ hsmall C hmod hcenter).IsKBounded fun (x : (D.refined hp hδ hsmall C hmod hcenter).flag.Node) => B)
:
(D.normalized hp hδ hsmall C hmod hcenter).IsKBounded fun (x : (D.normalized hp hδ hsmall C hmod hcenter).flag.Node) =>
B
theorem
EGZ.FlagDecomposition.CompletePreparation.normalizedCompleteNode_isCompleteElement
{p d : ℕ}
[Fact (Nat.Prime p)]
{f : FpCoord p d → ℕ}
{Φ : FlagDecomposition p d f}
{anchor : Φ.flag.Node}
{t : ℕ → ℕ}
{δ : ℝ}
(D : Φ.CompletePreparation anchor t δ)
(hp : Odd p)
(hδ : 0 ≤ δ)
(hsmall : 3 ^ (d + 1) * δ < 1)
(C : (x : (D.diagram hp hδ hsmall).Node) → IntegerLatticeChart ((D.diagram hp hδ hsmall).support x))
(hmod :
∀ (x : (D.diagram hp hδ hsmall).Node), Function.Injective ⇑((IntegralAffineMap.ofIntAffineMap (C x).map).modp p))
(hcenter : ∀ (x : (D.diagram hp hδ hsmall).Node), ∀ q ∈ (C x).coordinateSupport, IsCenteredLift p q)
:
(D.normalized hp hδ hsmall C hmod hcenter).IsCompleteElement (D.normalizedCompleteNode hp hδ hsmall C hmod hcenter)
(t (D.count + 1)) δ
theorem
EGZ.FlagDecomposition.CompletePreparation.normalizedCompleteNode_cumulativeWeight
{p d : ℕ}
[Fact (Nat.Prime p)]
{f : FpCoord p d → ℕ}
{Φ : FlagDecomposition p d f}
{anchor : Φ.flag.Node}
{t : ℕ → ℕ}
{δ : ℝ}
(D : Φ.CompletePreparation anchor t δ)
(hp : Odd p)
(hδ : 0 ≤ δ)
(hsmall : 3 ^ (d + 1) * δ < 1)
(C : (x : (D.diagram hp hδ hsmall).Node) → IntegerLatticeChart ((D.diagram hp hδ hsmall).support x))
(hmod :
∀ (x : (D.diagram hp hδ hsmall).Node), Function.Injective ⇑((IntegralAffineMap.ofIntAffineMap (C x).map).modp p))
(hcenter : ∀ (x : (D.diagram hp hδ hsmall).Node), ∀ q ∈ (C x).coordinateSupport, IsCenteredLift p q)
:
(D.normalized hp hδ hsmall C hmod hcenter).cumulativeWeight (D.normalizedCompleteNode hp hδ hsmall C hmod hcenter) = restrictWeight (Φ.cumulativeWeight anchor) D.selectedSet
theorem
EGZ.FlagDecomposition.CompletePreparation.normalized_node_ne_upperAnchor
{p d : ℕ}
[Fact (Nat.Prime p)]
{f : FpCoord p d → ℕ}
{Φ : FlagDecomposition p d f}
{anchor : Φ.flag.Node}
{t : ℕ → ℕ}
{δ : ℝ}
(D : Φ.CompletePreparation anchor t δ)
(hp : Odd p)
(hδ : 0 ≤ δ)
(hsmall : 3 ^ (d + 1) * δ < 1)
(C : (x : (D.diagram hp hδ hsmall).Node) → IntegerLatticeChart ((D.diagram hp hδ hsmall).support x))
(hmod :
∀ (x : (D.diagram hp hδ hsmall).Node), Function.Injective ⇑((IntegralAffineMap.ofIntAffineMap (C x).map).modp p))
(hcenter : ∀ (x : (D.diagram hp hδ hsmall).Node), ∀ q ∈ (C x).coordinateSupport, IsCenteredLift p q)
(x : (D.normalized hp hδ hsmall C hmod hcenter).flag.Node)
:
The old upper anchor is absent from the normalized node subtype.
noncomputable def
EGZ.FlagDecomposition.CompletePreparation.normalizedSubdivisionMap
{p d : ℕ}
[Fact (Nat.Prime p)]
{f : FpCoord p d → ℕ}
{Φ : FlagDecomposition p d f}
{anchor : Φ.flag.Node}
{t : ℕ → ℕ}
{δ : ℝ}
(D : Φ.CompletePreparation anchor t δ)
(hp : Odd p)
(hδ : 0 ≤ δ)
(hsmall : 3 ^ (d + 1) * δ < 1)
(C : (x : (D.diagram hp hδ hsmall).Node) → IntegerLatticeChart ((D.diagram hp hδ hsmall).support x))
(hmod :
∀ (x : (D.diagram hp hδ hsmall).Node), Function.Injective ⇑((IntegralAffineMap.ofIntAffineMap (C x).map).modp p))
(hcenter : ∀ (x : (D.diagram hp hδ hsmall).Node), ∀ q ∈ (C x).coordinateSupport, IsCenteredLift p q)
:
Φ.SubdivisionMap (D.normalized hp hδ hsmall C hmod hcenter)
The subdivision map from the original decomposition to its normalized completion.
Equations
- D.normalizedSubdivisionMap hp hδ hsmall C hmod hcenter = (D.refinedSubdivisionMap hp hδ hsmall C hmod hcenter).comp ((D.refined hp hδ hsmall C hmod hcenter).reducedSubdivisionMap hp)
Instances For
theorem
EGZ.FlagDecomposition.CompletePreparation.normalized_isRealizedFace
{p d : ℕ}
[Fact (Nat.Prime p)]
{f : FpCoord p d → ℕ}
{Φ : FlagDecomposition p d f}
{anchor : Φ.flag.Node}
{t : ℕ → ℕ}
{δ : ℝ}
(D : Φ.CompletePreparation anchor t δ)
(hp : Odd p)
(hδ : 0 ≤ δ)
(hsmall : 3 ^ (d + 1) * δ < 1)
(C : (x : (D.diagram hp hδ hsmall).Node) → IntegerLatticeChart ((D.diagram hp hδ hsmall).support x))
(hmod :
∀ (x : (D.diagram hp hδ hsmall).Node), Function.Injective ⇑((IntegralAffineMap.ofIntAffineMap (C x).map).modp p))
(hcenter : ∀ (x : (D.diagram hp hδ hsmall).Node), ∀ q ∈ (C x).coordinateSupport, IsCenteredLift p q)
(x : (D.normalized hp hδ hsmall C hmod hcenter).flag.Node)
(Γ : (Φ.flag.polytope ((D.normalizedSubdivisionMap hp hδ hsmall C hmod hcenter).node x)).Face)
(hne :
(((D.normalized hp hδ hsmall C hmod hcenter).flag.polytope x).carrier ∩ ⇑((D.normalizedSubdivisionMap hp hδ hsmall C hmod hcenter).fibre x) ⁻¹' Γ.carrier).Nonempty)
(hΓ : Φ.IsRealizedFace ((D.normalizedSubdivisionMap hp hδ hsmall C hmod hcenter).node x) Γ)
:
(D.normalized hp hδ hsmall C hmod hcenter).IsRealizedFace x
((D.normalizedSubdivisionMap hp hδ hsmall C hmod hcenter).face x Γ hne)
theorem
EGZ.normalized_complete_refinement_lemma
(d : ℕ)
(g : ℕ → ℕ)
(hg : Monotone g)
:
∃ (B : ℕ → ℕ),
Monotone B ∧ (∀ (K : ℕ), K ≤ B 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) (δ : ℝ) (hδ : 0 ≤ δ)
(hsmall : 3 ^ (d + 1) * δ < 1),
(Φ.IsKBounded fun (x : Φ.flag.Node) => K) →
∃ (hp : Odd p) (t : ℕ → ℕ) (D : Φ.CompletePreparation anchor t δ) (C :
(x : (D.diagram hp hδ hsmall).Node) → IntegerLatticeChart ((D.diagram hp hδ hsmall).support x))
(hmod :
∀ (x : (D.diagram hp hδ hsmall).Node),
Function.Injective ⇑((IntegralAffineMap.ofIntAffineMap (C x).map).modp p))
(hcenter :
∀ (x : (D.diagram hp hδ hsmall).Node), ∀ q ∈ (C x).coordinateSupport, IsCenteredLift p q) (b : ℕ),
let Ψ := D.normalized hp hδ hsmall C hmod hcenter;
have S := D.normalizedSubdivisionMap hp hδ hsmall C hmod hcenter;
K ≤ b ∧ b ≤ B K ∧ Monotone t ∧ t 0 = K ∧ g b ≤ t (D.count + 1) ∧ Ψ.IsMinimal ∧ Ψ.IsReduced ∧ (Ψ.IsKBounded fun (x : Ψ.flag.Node) => b) ∧ ↑Φ.retainedMass - ↑Ψ.retainedMass ≤ 3 ^ (d + 1) * δ * ↑(natMass (Φ.cumulativeWeight anchor)) ∧ Fintype.card Ψ.flag.Node ≤ 2 * Fintype.card Φ.flag.Node ∧ Ψ.IsCompleteElement (D.normalizedCompleteNode hp hδ hsmall C hmod hcenter)
(g b) δ ∧ Ψ.cumulativeWeight (D.normalizedCompleteNode hp hδ hsmall C hmod hcenter) = restrictWeight (Φ.cumulativeWeight anchor) D.selectedSet ∧ (∀ (x : Ψ.flag.Node), ↑x ≠ D.upperAnchor hp hδ hsmall) ∧ ∀ (x : Ψ.flag.Node) (Γ : (Φ.flag.polytope (S.node x)).Face)
(hne :
((Ψ.flag.polytope x).carrier ∩ ⇑(S.fibre x) ⁻¹' Γ.carrier).Nonempty),
Φ.IsRealizedFace (S.node x) Γ → Ψ.IsRealizedFace x (S.face x Γ hne)
The uniform complete-element operation with its output already restricted to reduced nodes. The old upper anchor has no surviving copy.