Conclusions and the zero-dimensional flag decomposition

This file defines the conclusion of Theorem 4.13 and proves its monotonicity and zero-dimensional case. The asymptotic dependencies are:

• δ and the flag-cardinality bound depend only on d and ε;
• after the growing function g is fixed, the prime threshold and the uniform coordinate bound may also depend on g;
• none of these constants depends on the prime or the input weight.

The zero-dimensional case is proved by the initial one-node decomposition. The positive-dimensional existence proof is assembled in Existence.lean.

def EGZ.HasFlagDecompositionConclusion {p d : ℕ} (hp : Nat.Prime p) (f : FpCoord p d → ℕ) (ε δ : ℝ) (g : ℕ → ℕ) (Bcard BK : ℕ) : Prop

The conclusions supplied by the Flag Decomposition Lemma for one prime and one nonzero input function.

The primality proof installs the NeZero p instance required by finite sums over ZMod p. Keeping that implementation detail inside this predicate makes the public theorem quantify naturally over primes.

Equations

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

theorem EGZ.HasFlagDecompositionConclusion.mono_epsilon {p d : ℕ} {hp : Nat.Prime p} {f : FpCoord p d → ℕ} {ε ε' δ : ℝ} {g : ℕ → ℕ} {Bcard BK : ℕ} (h : HasFlagDecompositionConclusion hp f ε δ g Bcard BK) (hε : ε ≤ ε') : HasFlagDecompositionConclusion hp f ε' δ g Bcard BK

The final conclusion is monotone in the permitted mass loss. This justifies the paper's reduction to ε ≤ 1/2.

theorem EGZ.HasFlagDecompositionConclusion.mono_delta {p d : ℕ} {hp : Nat.Prime p} {f : FpCoord p d → ℕ} {ε δ δ' : ℝ} {g : ℕ → ℕ} {Bcard BK : ℕ} (h : HasFlagDecompositionConclusion hp f ε δ g Bcard BK) (hδ' : 0 ≤ δ') (hδ : δ' ≤ δ) : HasFlagDecompositionConclusion hp f ε δ' g Bcard BK

A smaller positive scale preserves both completeness and the gap estimate. This is the final uniform-scale replacement in the paper.

theorem EGZ.hasFlagDecompositionConclusion_dimZero (p : ℕ) (hp : Nat.Prime p) (f : FpCoord p 0 → ℕ) (hf : f ≠ 0) (ε : ℝ) (hε : 0 ≤ ε) (g : ℕ → ℕ) : HasFlagDecompositionConclusion hp f ε 1 g 1 1

Dimension zero needs no refinement: there are no nonconstant affine functionals, and the unique lifted atom carries the full input mass.

theorem EGZ.flag_decomposition_lemma_dimZero (ε : ℝ) (hε : 0 < ε) : ∃ (δ : ℝ) (Bcard : ℕ), 0 < δ ∧ ∀ (g : ℕ → ℕ), IsGrowing g → ∃ (p₀ : ℕ) (BK : ℕ), 2 ≤ p₀ ∧ 1 ≤ BK ∧ ∀ (p : ℕ) (hp : Nat.Prime p), p₀ < p → ∀ (f : FpCoord p 0 → ℕ), f ≠ 0 → HasFlagDecompositionConclusion hp f ε δ g Bcard BK