Balanced integer convex combinations

This file states the balanced-combination lemma (lm2) as an explicit proposition. Its proof is balanced_combination_lemma in EGZ.Balanced.Existence. The support is written in integer affine-lattice coordinates, so the generated affine lattice and the rationality used in the paper have an unambiguous meaning. Relative interior includes lower-dimensional supports and the singleton case. The constants are chosen before the centrality parameter, as required by the paper's uniformity in the main proof.

def EGZ.BalancedCombination.IsCentral {d : ℕ} (S : Finset (IntCoord d)) (w : ↥S → ℝ) (θ : ℝ) (c : RealCoord d) : Prop

Centrality for a finite weight on integer coordinate points. Testing closed halfspaces through the center suffices for all containing halfspaces.

Equations

• EGZ.BalancedCombination.IsCentral S w θ c = ∀ (ξ : EGZ.RealCoord d →ᵃ[ℝ] ℝ), θ * ∑ q : ↥S, w q ≤ ∑ q : ↥S, if ξ c ≤ ξ (↑q).real then w q else 0

structure EGZ.BalancedCombination.Data (d : ℕ) : Type

A finite positive weight and an interior point of its generated affine integer lattice. All coordinates are taken in a chosen ambient lattice.

• support : Finset (IntCoord d)

  Finite set of lattice points to be combined.

• support_nonempty : self.support.Nonempty
• weight : ↥self.support → ℝ

  Positive real weight assigned to each support point.

• weight_pos (q : ↥self.support) : 0 < self.weight q
• center : IntCoord d

  Integral center of the balanced combination.

• center_mem_span : self.center ∈ affineSpan ℤ ↑self.support
• center_mem_interior : self.center.real ∈ intrinsicInterior ℝ ((convexHull ℝ) (IntCoord.real '' ↑self.support))

structure EGZ.BalancedCombination.Coefficients {d : ℕ} (D : Data d) (ε θ μ : ℝ) (n : ℕ) : Type

The integer coefficients and all bounds supplied by the lemma.

• coeff : ↥D.support → ℕ

  Multiplicity of each support point in the integer combination.

• sum_eq : ∑ q : ↥D.support, self.coeff q = n
• weighted_sum_eq : ∑ q : ↥D.support, self.coeff q • ↑q = n • D.center
• lower (q : ↥D.support) : μ * ↑n ≤ ↑(self.coeff q)
• upper (q : ↥D.support) : ↑(self.coeff q) ≤ (1 + ε) * ↑n * D.weight q / (θ * ∑ r : ↥D.support, D.weight r)

theorem EGZ.BalancedCombination.Data.totalWeight_pos {d : ℕ} (D : Data d) : 0 < ∑ q : ↥D.support, D.weight q

theorem EGZ.BalancedCombination.Data.centrality_le_one {d : ℕ} (D : Data d) {θ : ℝ} (h : IsCentral D.support D.weight θ D.center.real) : θ ≤ 1

def EGZ.BalancedCombination.Coefficients.monoLower {d : ℕ} {D : Data d} {ε θ μ μ' : ℝ} {n : ℕ} (A : Coefficients D ε θ μ n) (hμ : μ' ≤ μ) : Coefficients D ε θ μ' n

The lower fraction can be decreased without changing any coefficient.

Equations

• A.monoLower hμ = { coeff := A.coeff, sum_eq := ⋯, weighted_sum_eq := ⋯, lower := ⋯, upper := ⋯ }

theorem EGZ.BalancedCombination.Coefficients.mod_sum_eq_zero {d p : ℕ} {D : Data d} {ε θ μ : ℝ} (A : Coefficients D ε θ μ p) : ∑ q : ↥D.support, ↑(A.coeff q) • IntCoord.mod p ↑q = 0

Balance at length p becomes zero sum after reducing lattice coordinates modulo p. The center need not be zero.

theorem EGZ.BalancedCombination.Coefficients.expansion_slack {d n : ℕ} {D : Data d} {ε θ μ : ℝ} (A : Coefficients D ε θ μ n) (size : ↥D.support → ℕ) {η γ δ : ℝ} (hη : 0 ≤ η) (hδμ : δ ≤ μ) (hδηγ : δ ≤ η * γ) (hsize : ∀ (q : ↥D.support), γ * ↑n ≤ ↑(size q)) (hupper : ∀ (q : ↥D.support), ↑(A.coeff q) ≤ (1 - η) * ↑(size q)) (q : ↥D.support) : δ * ↑n ≤ ↑(A.coeff q) ∧ ↑(A.coeff q) ≤ ↑(size q) - δ * ↑n

The slack used by relative expansion follows from a positive lower fraction, a proportional upper bound, and a positive lower bound on each available fibre size.

@[reducible, inline]

abbrev EGZ.BalancedCombination.BoundedConfiguration (d K W : ℕ) : Type

A finite encoding of all integer-weighted configurations in a fixed box: a support, weights at most W, and a center in the same box.

Equations

• EGZ.BalancedCombination.BoundedConfiguration d K W = ((S : ↥(EGZ.latticeBox d K).powerset) × (↥↑S → Fin (W + 1)) × ↥(EGZ.latticeBox d K))

def EGZ.BalancedCombination.BoundedConfiguration.support {d K W : ℕ} (Q : BoundedConfiguration d K W) : Finset (IntCoord d)

Underlying finite lattice support of the bounded configuration.

Equations

• Q.support = ↑Q.fst

def EGZ.BalancedCombination.BoundedConfiguration.weight {d K W : ℕ} (Q : BoundedConfiguration d K W) : ↥Q.support → ℝ

Real weights obtained from the bounded integer weights.

Equations

• Q.weight q = ↑↑(Q.snd.1 q)

def EGZ.BalancedCombination.BoundedConfiguration.center {d K W : ℕ} (Q : BoundedConfiguration d K W) : IntCoord d

Integral center encoded by the bounded configuration.

Equations

• Q.center = ↑Q.snd.2

def EGZ.BalancedCombination.BoundedConfiguration.Valid {d K W : ℕ} (Q : BoundedConfiguration d K W) : Prop

Geometric validity and positivity are checked before applying the balanced-combination statement. Centrality is deliberately absent.

Equations

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

def EGZ.BalancedCombination.BoundedConfiguration.data {d K W : ℕ} (Q : BoundedConfiguration d K W) (h : Q.Valid) : Data d

Construct balanced-combination data from a valid bounded configuration.

Equations

• Q.data h = { support := Q.support, support_nonempty := ⋯, weight := Q.weight, weight_pos := ⋯, center := Q.center, center_mem_span := ⋯, center_mem_interior := ⋯ }

def EGZ.BalancedCombination.BoundedConfiguration.ofWeights {d K W : ℕ} (S : Finset (IntCoord d)) (hS : S ⊆ latticeBox d K) (w : ↥S → ℕ) (hw : ∀ (q : ↥S), w q ≤ W) (c : IntCoord d) (hc : c ∈ latticeBox d K) : BoundedConfiguration d K W

Encode any support and positive bounded integer weights.

Equations

• EGZ.BalancedCombination.BoundedConfiguration.ofWeights S hS w hw c hc = ⟨⟨S, ⋯⟩, (fun (q : ↥↑⟨S, ⋯⟩) => ⟨w q, ⋯⟩, ⟨c, hc⟩)⟩

def EGZ.BalancedCombinationLemma : Prop

The finite balanced convex-combination lemma in integer lattice coordinates. This is a proposition interface, not an axiom or a proved theorem. In particular, both μ and N are independent of θ and n.

Equations

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

theorem EGZ.BalancedCombinationLemma.uniform_finite_family (h : BalancedCombinationLemma) {I : Type u_1} [Finite I] (d : I → ℕ) (D : (i : I) → BalancedCombination.Data (d i)) (ε : ℝ) (hε : 0 < ε) : ∃ (μ : ℝ) (N : ℕ), 0 < μ ∧ ∀ (i : I) (θ : ℝ), 0 < θ → BalancedCombination.IsCentral (D i).support (D i).weight θ (D i).center.real → ∀ (n : ℕ), N < n → Nonempty (BalancedCombination.Coefficients (D i) ε θ μ n)

A finite family admits common constants. Their dependence on centrality and on the eventual integer length remains absent.

theorem EGZ.BalancedCombinationLemma.uniform_bounded_configurations (h : BalancedCombinationLemma) (d K W : ℕ) (ε : ℝ) (hε : 0 < ε) : ∃ (μ : ℝ) (N : ℕ), 0 < μ ∧ ∀ (Q : BalancedCombination.BoundedConfiguration d K W) (hQ : Q.Valid) (θ : ℝ), 0 < θ → BalancedCombination.IsCentral Q.support Q.weight θ Q.center.real → ∀ (n : ℕ), N < n → Nonempty (BalancedCombination.Coefficients (Q.data hQ) ε θ μ n)

Bounded supports, bounded positive integer weights, and bounded lattice centers have common constants. No centrality parameter or length enters the choice of those constants.

theorem EGZ.BalancedCombinationLemma.uniform_bounded_dimensions (h : BalancedCombinationLemma) (d K W : ℕ) (ε : ℝ) (hε : 0 < ε) : ∃ (μ : ℝ) (N : ℕ), 0 < μ ∧ ∀ r ≤ d, ∀ (Q : BalancedCombination.BoundedConfiguration r K W) (hQ : Q.Valid) (θ : ℝ), 0 < θ → BalancedCombination.IsCentral Q.support Q.weight θ Q.center.real → ∀ (n : ℕ), N < n → Nonempty (BalancedCombination.Coefficients (Q.data hQ) ε θ μ n)

The same constants can be chosen for every coordinate rank at most the fixed ambient dimension.