TupleCoefficients.lean`

11 declarations, 0 contain sorry, 0 declared as axioms

Coefficients for the finite tuple estimate

Replacing e by 3 gives the coefficients 3 / 64^(i+1). Their finite sum has an explicit positive remainder below 1 / 21. A finite product inequality then bounds the product of their complements from below.

def OAI.TalagrandThreshold.tupleCoefficient line 24
Source documentation
The convenient rational upper bound on the selector's coefficient.
```
noncomputable def tupleCoefficient (i : ℕ) : ℝ :=
…
```
theorem OAI.TalagrandThreshold.tupleCoefficient_eq line 27
theorem OAI.TalagrandThreshold.tupleCoefficient_pos line 33
theorem OAI.TalagrandThreshold.tupleCoefficient_nonneg line 37
theorem OAI.TalagrandThreshold.tupleCoefficient_le_first line 40
theorem OAI.TalagrandThreshold.tupleCoefficient_lt_one line 46
theorem OAI.TalagrandThreshold.sum_tupleCoefficient_add_remainder line 50
Source documentation
The exact finite geometric identity, including the empty sum.
```
theorem sum_tupleCoefficient_add_remainder (s : ℕ) :
    (∑ i : Fin s, tupleCoefficient i.val) +
      (1 / 21 : ℝ) * (1 / 64 : ℝ) ^ s = 1 / 21 := by
…
```
Mentions: OAI.TalagrandThreshold.tupleCoefficient
theorem OAI.TalagrandThreshold.sum_tupleCoefficient_lt line 61
theorem OAI.TalagrandThreshold.sum_tupleCoefficient_le line 66

theorem OAI.TalagrandThreshold.one_sub_sum_le_prod_one_sub line 71

Source documentation

A finite product loses at most the sum of its factors' deficits.

theorem one_sub_sum_le_prod_one_sub {ι : Type*} [Fintype ι]
    (c : ι → ℝ) (h0 : ∀ i, 0 ≤ c i) (h1 : ∀ i, c i ≤ 1) :
    1 - ∑ i, c i ≤ ∏ i, (1 - c i) := by
…

theorem OAI.TalagrandThreshold.prod_one_sub_tupleCoefficient_gt line 88