Rounding bounded weights before choosing balanced coefficients

Dividing by a common scale and taking natural floors changes every positive fibre weight by only a prescribed relative fraction. Consequently centrality and coefficient upper bounds transfer quantitatively. Bounded rounded weights belong to a finite family before the prime or original masses are fixed.

noncomputable def EGZ.BalancedCombination.roundedWeight {I : Type u_1} (m : I → ℕ) (H : ℝ) (q : I) : ℕ

Round each weight down after division by the common scale.

Equations

• EGZ.BalancedCombination.roundedWeight m H q = ⌊↑(m q) / H⌋₊

theorem EGZ.BalancedCombination.roundedWeight_upper {I : Type u_1} (m : I → ℕ) {H : ℝ} (hH : 0 < H) (q : I) : ↑(roundedWeight m H q) ≤ ↑(m q) / H

theorem EGZ.BalancedCombination.roundedWeight_lower {I : Type u_1} (m : I → ℕ) {H η : ℝ} (hH : 0 < H) (hsmall : ∀ (q : I), H ≤ η * ↑(m q)) (q : I) : (1 - η) * (↑(m q) / H) ≤ ↑(roundedWeight m H q)

theorem EGZ.BalancedCombination.roundedWeight_pos {I : Type u_1} (m : I → ℕ) {H η : ℝ} (hH : 0 < H) (hη : η ≤ 1) (hsmall : ∀ (q : I), H ≤ η * ↑(m q)) (q : I) : 0 < roundedWeight m H q

theorem EGZ.BalancedCombination.roundedWeight_le_bound {I : Type u_1} (m : I → ℕ) {H B : ℝ} (q : I) (hB : ↑(m q) / H ≤ B) : roundedWeight m H q ≤ ⌈B⌉₊

theorem EGZ.BalancedCombination.roundedWeight_sum_bounds {I : Type u_1} (m : I → ℕ) {H η : ℝ} (hH : 0 < H) (hsmall : ∀ (q : I), H ≤ η * ↑(m q)) (T : Finset I) : (1 - η) * ((∑ q ∈ T, ↑(m q)) / H) ≤ ∑ q ∈ T, ↑(roundedWeight m H q) ∧ ∑ q ∈ T, ↑(roundedWeight m H q) ≤ (∑ q ∈ T, ↑(m q)) / H

Relative rounding bounds hold on every finite subset, not only the whole support or halfspaces.

theorem EGZ.BalancedCombination.IsCentral.rounded {d : ℕ} {S : Finset (IntCoord d)} (m : ↥S → ℕ) {H η θ : ℝ} {c : RealCoord d} (h : IsCentral S (fun (q : ↥S) => ↑(m q)) θ c) (hH : 0 < H) (hη : η ≤ 1) (hθ : 0 ≤ θ) (hsmall : ∀ (q : ↥S), H ≤ η * ↑(m q)) : IsCentral S (fun (q : ↥S) => ↑(roundedWeight m H q)) ((1 - η) * θ) c

The rounded weight is central at the multiplicatively decreased parameter (1 - η) * θ.

theorem EGZ.BalancedCombination.rounded_coefficient_upper {I : Type u_1} [Fintype I] (m a : I → ℕ) {H η θ : ℝ} {n : ℕ} (hH : 0 < H) (hη : η < 1) (hθ : 0 < θ) (hmass : 0 < ∑ q : I, ↑(m q)) (hsmall : ∀ (q : I), H ≤ η * ↑(m q)) (hε : 0 ≤ 1 + η) (ha : ∀ (q : I), ↑(a q) ≤ (1 + η) * ↑n * ↑(roundedWeight m H q) / ((1 - η) * θ * ∑ r : I, ↑(roundedWeight m H r))) (q : I) : ↑(a q) ≤ (1 + η) / (1 - η) ^ 2 * ↑n * ↑(m q) / (θ * ∑ r : I, ↑(m r))

Transfer the balanced upper bound back from the rounded weights.

theorem EGZ.BalancedCombination.uniform_rounded_coefficients (hBalanced : BalancedCombinationLemma) (d K : ℕ) (C γ η : ℝ) (hγ : 0 < γ) (hη : 0 < η) (hηone : η < 1) : ∃ (μ : ℝ) (N : ℕ), 0 < μ ∧ ∀ r ≤ d, ∀ S ⊆ latticeBox r K, S.Nonempty → ∀ c ∈ latticeBox r K, c ∈ affineSpan ℤ ↑S → c.real ∈ intrinsicInterior ℝ ((convexHull ℝ) (IntCoord.real '' ↑S)) → ∀ (m : ↥S → ℕ) (p : ℕ), N < p → (∀ (q : ↥S), γ * ↑p ≤ ↑(m q)) → ∑ q : ↥S, ↑(m q) ≤ C * ↑p → ∀ (θ : ℝ), 0 < θ → IsCentral S (fun (q : ↥S) => ↑(m q)) θ c.real → ∃ (a : ↥S → ℕ), ∑ q : ↥S, a q = p ∧ ∑ q : ↥S, a q • ↑q = p • c ∧ (∀ (q : ↥S), μ * ↑p ≤ ↑(a q)) ∧ ∀ (q : ↥S), ↑(a q) ≤ (1 + η) / (1 - η) ^ 2 * ↑p * ↑(m q) / (θ * ∑ s : ↥S, ↑(m s))

Uniform balanced coefficients for bounded lattice fibres. The original integer masses and the length may vary without bound: rounding places them in a finite family using only d, K, C, γ, and η. Both witnesses are chosen before the original masses, the centrality parameter, and the length. The only unproved ingredient is the explicitly supplied balanced lemma.