Stable mass maps for normalized refinement steps

noncomputable def EGZ.FlagDecomposition.PrunedWeights.normalizedStableNodeMap {p d : ℕ} [NeZero p] [Fact (Nat.Prime p)] {f : FpCoord p d → ℕ} {Φ : FlagDecomposition p d f} (D : Φ.PrunedWeights) (hp : Odd p) (C : (x : (D.cleaned hp).flag.Node) → IntegerLatticeChart ((D.cleaned hp).liftedSupport x)) (hmod : ∀ (x : (D.cleaned hp).flag.Node), Function.Injective ⇑((Rechart.chart (D.cleaned hp) C x).modp p)) (hcenter : ∀ (x : (D.cleaned hp).flag.Node), ∀ q ∈ (C x).coordinateSupport, IsCenteredLift p q) (x : (D.normalized hp C hmod hcenter).flag.Node) : Φ.StableNodeMap (D.normalized hp C hmod hcenter) ((D.normalizedSubdivisionMap hp C hmod hcenter).node x) x

The stable map from a normalized pruned node to its original ancestor.

Equations

• D.normalizedStableNodeMap hp C hmod hcenter x = (D.cleanedStableNodeMap hp x).comp (EGZ.FlagDecomposition.Rechart.stableNodeMap (D.cleaned hp) C hp hmod hcenter x)

@[simp]

theorem EGZ.FlagDecomposition.PrunedWeights.normalizedStableNodeMap_real {p d : ℕ} [NeZero p] [Fact (Nat.Prime p)] {f : FpCoord p d → ℕ} {Φ : FlagDecomposition p d f} (D : Φ.PrunedWeights) (hp : Odd p) (C : (x : (D.cleaned hp).flag.Node) → IntegerLatticeChart ((D.cleaned hp).liftedSupport x)) (hmod : ∀ (x : (D.cleaned hp).flag.Node), Function.Injective ⇑((Rechart.chart (D.cleaned hp) C x).modp p)) (hcenter : ∀ (x : (D.cleaned hp).flag.Node), ∀ q ∈ (C x).coordinateSupport, IsCenteredLift p q) (x : (D.normalized hp C hmod hcenter).flag.Node) : (D.normalizedStableNodeMap hp C hmod hcenter x).coord.real = (D.normalizedSubdivisionMap hp C hmod hcenter).fibre x

noncomputable def EGZ.FlagDecomposition.CompletePreparation.splitStableNodeMap {p d : ℕ} [NeZero p] [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) (x : (D.split hp hδ hsmall).flag.Node) : Φ.StableNodeMap (D.split hp hδ hsmall) ((D.subdivisionMap hp hδ hsmall).node x) x

The stable node map induced by the splitting stage of complete preparation.

Equations

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

noncomputable def EGZ.FlagDecomposition.CompletePreparation.refinedStableNodeMap {p d : ℕ} [NeZero p] [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.refined hp hδ hsmall C hmod hcenter).flag.Node) : Φ.StableNodeMap (D.refined hp hδ hsmall C hmod hcenter) ((D.refinedSubdivisionMap hp hδ hsmall C hmod hcenter).node x) x

The stable node map after splitting and recharting the completion refinement.

Equations

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

noncomputable def EGZ.FlagDecomposition.CompletePreparation.normalizedStableNodeMap {p d : ℕ} [NeZero p] [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) : Φ.StableNodeMap (D.normalized hp hδ hsmall C hmod hcenter) ((D.normalizedSubdivisionMap hp hδ hsmall C hmod hcenter).node x) x

The stable node map from a normalized complete refinement to the original decomposition.

Equations

• D.normalizedStableNodeMap hp hδ hsmall C hmod hcenter x = (D.refinedStableNodeMap hp hδ hsmall C hmod hcenter ↑x).comp ((D.refined hp hδ hsmall C hmod hcenter).reducedStableNodeMap hp x)

@[simp]

theorem EGZ.FlagDecomposition.CompletePreparation.normalizedStableNodeMap_real {p d : ℕ} [NeZero p] [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) : (D.normalizedStableNodeMap hp hδ hsmall C hmod hcenter x).coord.real = (D.normalizedSubdivisionMap hp hδ hsmall C hmod hcenter).fibre x

noncomputable def EGZ.FlagDecomposition.FaceRefinement.normalizedUpperStableNodeMap {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) (hx : (↑↑↑x).2 = 1) : Φ.StableNodeMap (normalized Φ anchor Γ hp C hmod hcenter) ((normalizedSubdivisionMap Φ anchor Γ hp C hmod hcenter).node x) x

The stable node map for an upper-layer node of the normalized face refinement.

Equations

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

@[simp]

theorem EGZ.FlagDecomposition.FaceRefinement.normalizedUpperStableNodeMap_real {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) (hx : (↑↑↑x).2 = 1) : (normalizedUpperStableNodeMap Φ anchor Γ hp C hmod hcenter x hx).coord.real = (normalizedSubdivisionMap Φ anchor Γ hp C hmod hcenter).fibre x