Applying relative expansion to affine fibres

The relative expansion statement implies an affine-subspace version with uniform thresholds in the original ambient dimension. Translating the integer centre doubles the box radius and changes the weighted sum to zero.

theorem EGZ.Expansion.AffineModel.apply_relativeExpansion {p d r t K T : ℕ} [NeZero p] [Fact (Nat.Prime p)] {δ : ℝ} {V : AffineSubspace (ZMod p) (FpCoord p d)} {φ : FpCoord p d →ᵃ[ZMod p] FpCoord p r} (S : Finset (IntCoord r)) (c : IntCoord r) (M : AffineModel V φ (IntCoord.mod p c) t) (hexp : RelativeExpansionAt r t (2 * K) δ T p) (w : FpCoord p d → ℕ) (α : ↥S → ℕ) (hbox : ∀ q ∈ S, latticeSupNorm q ≤ K) (hc : latticeSupNorm c ≤ K) (hw : ∀ (v : FpCoord p d), w v ≠ 0 → v ∈ V) (hs : ∀ (v : FpCoord p d), w v ≠ 0 → ∃ q ∈ S, φ v = IntCoord.mod p q) (hz : ∑ q : ↥S, α q • ↑q = p • c) (hm : ∑ q : ↥S, α q = p) (ha : ∀ (q : ↥S), δ * ↑p ≤ ↑(α q) ∧ ↑(α q) ≤ ↑(pushWeight (⇑φ) w (IntCoord.mod p ↑q)) - δ * ↑p) (hthick : IsThickRelativeOn w (↑V) (⇑φ) T δ) : HasZeroSumMultiplicity w

def EGZ.Expansion.AffineExpansionAt (d K : ℕ) (δ : ℝ) (T p : ℕ) [NeZero p] : Prop

The expansion conclusion for an arbitrary affine surjection on the affine subspace carrying a weight. The centre and support share one box.

Equations

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

theorem EGZ.Expansion.RelativeExpansionStatement.affine_thresholds (h : RelativeExpansionStatement) (d K : ℕ) (hK : 1 ≤ K) (δ : ℝ) (hδ : 0 < δ) : ∃ (T₀ : ℕ) (p₀ : ℕ), ∀ (T : ℕ), T₀ ≤ T → ∀ (p : ℕ), Fact (Nat.Prime p) → ∀ (x : NeZero p), p₀ ≤ p → AffineExpansionAt d K δ T p

Uniformity over the finitely many possible quotient and kernel dimensions gives thresholds depending only on d, K, and δ.

theorem EGZ.Expansion.AffineExpansionAt.decomposition {p d K T : ℕ} [NeZero p] {δ δ₀ : ℝ} (h : AffineExpansionAt d K δ T p) {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) (hp : Odd p) (x : Φ.flag.Node) (hr : Φ.flag.rank x ≤ d) (hbox : ∀ q ∈ Φ.liftedSupport x, latticeSupNorm q ≤ K) (c : IntCoord (Φ.flag.rank x)) (hc : latticeSupNorm c ≤ K) (α : ↥(Φ.liftedSupport x) → ℕ) (hz : ∑ q : ↥(Φ.liftedSupport x), α q • ↑q = p • c) (hm : ∑ q : ↥(Φ.liftedSupport x), α q = p) (ha : ∀ (q : ↥(Φ.liftedSupport x)), δ * ↑p ≤ ↑(α q) ∧ ↑(α q) ≤ ↑(Φ.hat x ↑q) - δ * ↑p) (ht : Φ.IsCompleteElement x T δ₀) (hδ : δ ≤ δ₀) : HasZeroSumMultiplicity f

The expansion interface applies directly to a complete decomposition node. Its conclusion is a zero sum in the original multiplicity function.