TupleGeometric.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

A finite geometric bound for nonzero tuples

Every finite family of tuples lies in a finite coordinate box. Factoring the sum over this box reduces the estimate to ordinary finite geometric sums. Adding the zero tuple contributes exactly one, so removing it gives the selector's budget of strictly less than 1 / 20.

theorem OAI.TalagrandThreshold.finite_geom_sum_mul_one_sub line 24
theorem OAI.TalagrandThreshold.finite_geom_sum_le_inverse line 32

theorem OAI.TalagrandThreshold.finite_tuple_sum_le_inverse_product line 41

Source documentation

A finite tuple family is bounded by the product of geometric bounds.

theorem finite_tuple_sum_le_inverse_product {ι : Type*} [Fintype ι]
    (T : Finset (ι → ℕ)) (c : ι → ℝ)
    (hc0 : ∀ i, 0 ≤ c i) (hc1 : ∀ i, c i < 1) :
    (∑ t ∈ T, ∏ i, (c i) ^ (t i)) ≤ ∏ i, (1 - c i)⁻¹ := by
…

theorem OAI.TalagrandThreshold.finite_tuple_sum_le_inverse_one_sub_sum line 70

Source documentation

The sum of coefficients controls every finite tuple family.

theorem finite_tuple_sum_le_inverse_one_sub_sum {ι : Type*} [Fintype ι]
    (T : Finset (ι → ℕ)) (c : ι → ℝ)
    (hc0 : ∀ i, 0 ≤ c i) (hc1 : ∀ i, c i < 1)
    (hsum : (∑ i, c i) < 1) :
    (∑ t ∈ T, ∏ i, (c i) ^ (t i)) ≤ (1 - ∑ i, c i)⁻¹ := by
…

theorem OAI.TalagrandThreshold.tuple_geometric_sum_lt_one_twentieth line 85
Source documentation
The actual selector coefficients give a strict budget for every finite family of nonzero tuples, without an infinite-series argument.
```
theorem tuple_geometric_sum_lt_one_twentieth {s : ℕ}
    (T : Finset (Fin s → ℕ)) (hT : ∀ t ∈ T, t ≠ 0) :
    (∑ t ∈ T, ∏ i : Fin s, ((3 : ℝ) / 64 ^ (i.val + 1)) ^ (t i)) < 1 / 20 := by
…
```
theorem OAI.TalagrandThreshold.tuple_geometric_sum_le_one_twentieth line 108

theorem OAI.TalagrandThreshold.tuple_geometric_sum_lt_one_twentieth_of_pos_total line 114

Source documentation

A positive total degree is the form supplied by a nonempty changed set.

theorem tuple_geometric_sum_lt_one_twentieth_of_pos_total {s : ℕ}
    (T : Finset (Fin s → ℕ)) (hT : ∀ t ∈ T, 0 < ∑ i, t i) :
    (∑ t ∈ T, ∏ i : Fin s, ((3 : ℝ) / 64 ^ (i.val + 1)) ^ (t i)) < 1 / 20 := by
…