The complete-element refinement #
The prepared lower layer acquires the chosen slab coordinates and is put in minimal lattice coordinates. Its anchor is complete by maximality of the thin directions. Passing to the face index of its whole polytope supplies a reduced complete representative with exactly the same cumulative function.
@[reducible, inline]
noncomputable abbrev
EGZ.FlagDecomposition.CompletePreparation.refined
{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
Augmented refinement in the chosen integral charts.
Equations
Instances For
theorem
EGZ.FlagDecomposition.CompletePreparation.refined_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)
:
theorem
EGZ.FlagDecomposition.CompletePreparation.refined_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)
(x : (D.split hp hδ hsmall).flag.Node)
:
(D.refined hp hδ hsmall C hmod hcenter).cumulativeWeight x = (D.split hp hδ hsmall).cumulativeWeight x
theorem
EGZ.FlagDecomposition.CompletePreparation.refined_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)
:
theorem
EGZ.FlagDecomposition.CompletePreparation.refined_lowerAnchor_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.refined hp hδ hsmall C hmod hcenter).IsCompleteElement (D.lowerAnchor hp hδ hsmall) (t (D.count + 1)) δ
The lower anchor is complete after adjoining all chosen directions.
noncomputable def
EGZ.FlagDecomposition.CompletePreparation.completeNode
{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)
:
A reduced node below the lower anchor with the same cumulative weight.
Equations
- D.completeNode hp hδ hsmall C hmod hcenter = (D.refined hp hδ hsmall C hmod hcenter).faceIndex (D.lowerAnchor hp hδ hsmall) ⊤
Instances For
theorem
EGZ.FlagDecomposition.CompletePreparation.completeNode_le_lowerAnchor
{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.completeNode_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.refined hp hδ hsmall C hmod hcenter).IsReducedElement (D.completeNode hp hδ hsmall C hmod hcenter)
theorem
EGZ.FlagDecomposition.CompletePreparation.completeNode_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.refined hp hδ hsmall C hmod hcenter).cumulativeWeight (D.completeNode hp hδ hsmall C hmod hcenter) = restrictWeight (Φ.cumulativeWeight anchor) D.selectedSet
theorem
EGZ.FlagDecomposition.CompletePreparation.completeNode_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.refined hp hδ hsmall C hmod hcenter).IsCompleteElement (D.completeNode hp hδ hsmall C hmod hcenter) (t (D.count + 1))
δ
theorem
EGZ.FlagDecomposition.CompletePreparation.refined_upperAnchor_not_isReducedElement
{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.refined hp hδ hsmall C hmod hcenter).IsReducedElement (D.upperAnchor hp hδ hsmall)
theorem
EGZ.FlagDecomposition.CompletePreparation.refined_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.refined hp hδ hsmall C hmod hcenter).retainedMass ≤ 3 ^ (d + 1) * δ * ↑(natMass (Φ.cumulativeWeight anchor))
theorem
EGZ.FlagDecomposition.CompletePreparation.refined_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.refined_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 :
∀ (x : (D.diagram hp hδ hsmall).Node) (q : IntCoord (C x).rank),
q.real ∈ (((D.diagram hp hδ hsmall).chartedFlag C).polytope x).carrier → latticeSupNorm q ≤ B)
:
(D.refined hp hδ hsmall C hmod hcenter).IsKBounded fun (x : (D.refined hp hδ hsmall C hmod hcenter).flag.Node) => B
noncomputable def
EGZ.FlagDecomposition.CompletePreparation.refinedSubdivisionMap
{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.refined hp hδ hsmall C hmod hcenter)
Subdivision map from the augmented refinement back to the original decomposition.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
EGZ.FlagDecomposition.CompletePreparation.count_pos_of_not_complete
{p d : ℕ}
[Fact (Nat.Prime p)]
{f : FpCoord p d → ℕ}
{Φ : FlagDecomposition p d f}
{anchor : Φ.flag.Node}
{t : ℕ → ℕ}
{δ : ℝ}
(D : Φ.CompletePreparation anchor t δ)
(hδ : 0 ≤ δ)
(T : ℕ)
(hwidth : T ≤ t 1)
(hnot : ¬Φ.IsCompleteElement anchor T δ)
:
An incomplete anchor forces the construction to add at least one new direction whenever the first chosen width dominates its requested width.