Documentation

LeanPool.ErdosGinzburgZiv.EGZ.Decomposition.CenteredLift

Centered coordinate lifts #

For odd moduli, reduction identifies the centered integer box with the whole finite coordinate space. The finite boxes also supply explicit support sets for the lifted weights used in flag decompositions.

source
@[simp]
theorem EGZ.latticeSupNorm_le_iff {n K : ℕ} {z : IntCoord n} :
latticeSupNorm z ≤ K ↔ ∀ (i : Fin n), (z i).natAbs ≤ K
source
@[simp]
theorem EGZ.isCenteredLift_iff {p n : ℕ} {z : IntCoord n} :
IsCenteredLift p z ↔ ∀ (i : Fin n), (z i).natAbs ≤ (p - 1) / 2
source
noncomputable def EGZ.latticeBox (n K : ℕ) :
Finset (IntCoord n)

Integer coordinate vectors in the closed box of radius K.

Equations
Instances For
    source
    @[simp]
    theorem EGZ.mem_latticeBox {n K : ℕ} {z : IntCoord n} :
    z ∈ latticeBox n K ↔ latticeSupNorm z ≤ K
    source
    @[simp]
    theorem EGZ.card_latticeBox (n K : ℕ) :
    (latticeBox n K).card = (2 * K + 1) ^ n
    source
    theorem EGZ.card_le_of_latticeSupNorm_le {n K : ℕ} (S : Finset (IntCoord n)) (hS : ∀ z ∈ S, latticeSupNorm z ≤ K) :
    S.card ≤ (2 * K + 1) ^ n
    source
    def EGZ.FpCoord.centeredLift {p n : ℕ} (c : FpCoord p n) :
    IntCoord n

    Coordinatewise integer representatives with least absolute value.

    Equations
    Instances For
      source
      @[simp]
      theorem EGZ.FpCoord.centeredLift_apply {p n : ℕ} (c : FpCoord p n) (i : Fin n) :
      c.centeredLift i = (c i).valMinAbs
      source
      @[simp]
      theorem EGZ.FpCoord.mod_centeredLift {p n : ℕ} (c : FpCoord p n) :
      IntCoord.mod p c.centeredLift = c
      source
      theorem EGZ.FpCoord.isCenteredLift_centeredLift {p n : ℕ} [NeZero p] (hp : Odd p) (c : FpCoord p n) :
      IsCenteredLift p c.centeredLift
      source
      theorem EGZ.FpCoord.centeredLift_mod {p n : ℕ} [NeZero p] {z : IntCoord n} (hz : IsCenteredLift p z) :
      (IntCoord.mod p z).centeredLift = z
      source
      theorem EGZ.IsCenteredLift.eq_of_mod_eq {p n : ℕ} [NeZero p] {z w : IntCoord n} (hz : IsCenteredLift p z) (hw : IsCenteredLift p w) (h : IntCoord.mod p z = IntCoord.mod p w) :
      z = w

      Reduction is injective on the centered box, even for an even modulus.

      source
      theorem EGZ.existsUnique_isCenteredLift {p n : ℕ} [NeZero p] (hp : Odd p) (c : FpCoord p n) :
      ∃! z : IntCoord n, IsCenteredLift p z ∧ IntCoord.mod p z = c

      For odd moduli each finite-field vector has exactly one centered lift.

      source
      theorem EGZ.sum_latticeBox_mod {p n : ℕ} [NeZero p] (hp : Odd p) (g : FpCoord p n → ℕ) :
      ∑ z ∈ latticeBox n ((p - 1) / 2), g (IntCoord.mod p z) = ∑ c : FpCoord p n, g c

      Summing over centered integer coordinates is the same as summing over the finite coordinate space.

      source
      noncomputable def EGZ.FlagDecompositionRaw.hatSupport {p d : ℕ} [NeZero p] {F : ConvexFlag} (R : FpRepresentation p d F) (pieces : F.Node → FpCoord p d → ℕ) (x : F.Node) :
      Finset (IntCoord (F.rank x))

      The support of the cumulative centered lift, constructed from a finite box instead of stored as extra data.

      Equations
      Instances For
        source
        @[simp]
        theorem EGZ.FlagDecompositionRaw.mem_hatSupport {p d : ℕ} [NeZero p] {F : ConvexFlag} (R : FpRepresentation p d F) (pieces : F.Node → FpCoord p d → ℕ) (x : F.Node) (z : IntCoord (F.rank x)) :
        z ∈ hatSupport R pieces x ↔ hat R pieces x z ≠ 0
        source
        theorem EGZ.FlagDecompositionRaw.sum_affineFibreMass {p d : ℕ} [NeZero p] {n : ℕ} (w : FpCoord p d → ℕ) (φ : FpCoord p d → FpCoord p n) :
        ∑ c : FpCoord p n, affineFibreMass w φ c = natMass w
        source
        theorem EGZ.FlagDecompositionRaw.sum_hatSupport {p d : ℕ} [NeZero p] {F : ConvexFlag} (hp : Odd p) (R : FpRepresentation p d F) (pieces : F.Node → FpCoord p d → ℕ) (x : F.Node) :
        ∑ z ∈ hatSupport R pieces x, hat R pieces x z = natMass (cumulativeWeight pieces x)

        Cumulative lifted mass is exactly cumulative finite-field mass.

        source
        theorem EGZ.FlagDecomposition.liftedSupport_eq_hatSupport {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) (x : Φ.flag.Node) :
        Φ.liftedSupport x = FlagDecompositionRaw.hatSupport Φ.representation Φ.localWeight x
        source
        theorem EGZ.FlagDecomposition.sum_liftedSupport {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} (hp : Odd p) (Φ : FlagDecomposition p d f) (x : Φ.flag.Node) :
        ∑ z ∈ Φ.liftedSupport x, Φ.hat x z = natMass (Φ.cumulativeWeight x)

        The stored support does not change the total cumulative mass.

        source
        theorem EGZ.FpRepresentation.rank_le {p d : ℕ} [Fact (Nat.Prime p)] {F : ConvexFlag} (R : FpRepresentation p d F) (x : F.Node) :
        F.rank x ≤ d

        The rank of a represented node cannot exceed the ambient dimension.