BinomialMoments.lean`

23 declarations, 0 contain sorry, 0 declared as axioms

Exact finite moments of the symmetric binomial weights. These identities provide the grading multiplicities and the variance used in the finite coupling estimate. No probabilistic assumptions or measures enter the statements.

theorem OAI.LeanBlast.GotsmanLinial.binomialDenominator_pos line 21
Source documentation
The normalizing denominator is positive, also when n = 0.
```
theorem binomialDenominator_pos (n : ℕ) : 0 < (2 : ℝ) ^ n :=
…
```
theorem OAI.LeanBlast.GotsmanLinial.binomialDenominator_ne_zero line 24
theorem OAI.LeanBlast.GotsmanLinial.sum_choose_range line 28
Source documentation
The real sum of one row of Pascal's triangle.
```
theorem sum_choose_range (n : ℕ) :
    (∑ k ∈ Finset.range (n + 1), (n.choose k : ℝ)) = (2 : ℝ) ^ n := by
…
```

theorem OAI.LeanBlast.GotsmanLinial.sum_choose_succ line 33

Source documentation

Pascal recursion for an arbitrary real function of the binomial index.

theorem sum_choose_succ (n : ℕ) (f : ℕ → ℝ) :
    (∑ k ∈ Finset.range (n + 2), ((n + 1).choose k : ℝ) * f k) =
      (∑ k ∈ Finset.range (n + 1), (n.choose k : ℝ) * f k) +
        ∑ k ∈ Finset.range (n + 1), (n.choose k : ℝ) * f (k + 1) :=
…

theorem OAI.LeanBlast.GotsmanLinial.sum_choose_mul_index_range line 40

Source documentation

The first raw binomial moment, with a formula valid at n = 0.

theorem sum_choose_mul_index_range (n : ℕ) :
    (∑ k ∈ Finset.range (n + 1), (n.choose k : ℝ) * (k : ℝ)) =
      (n : ℝ) * (2 : ℝ) ^ n / 2 := by
…

theorem OAI.LeanBlast.GotsmanLinial.sum_choose_mul_index_sq_range line 53

Source documentation

The second raw binomial moment, with a formula valid at n = 0.

theorem sum_choose_mul_index_sq_range (n : ℕ) :
    (∑ k ∈ Finset.range (n + 1), (n.choose k : ℝ) * (k : ℝ) ^ 2) =
      (n : ℝ) * ((n : ℝ) + 1) * (2 : ℝ) ^ n / 4 := by
…

theorem OAI.LeanBlast.GotsmanLinial.sum_choose_centered_sq_range line 75

Source documentation

Exact centered second moment before dividing by 2^n.

theorem sum_choose_centered_sq_range (n : ℕ) :
    (∑ k ∈ Finset.range (n + 1),
      (n.choose k : ℝ) * ((k : ℝ) - (n : ℝ) / 2) ^ 2) =
      (n : ℝ) * (2 : ℝ) ^ n / 4 := by
…

theorem OAI.LeanBlast.GotsmanLinial.sum_choose line 93
Source documentation
The same total mass on the grading-index type.
```
theorem sum_choose (n : ℕ) :
    (∑ k : Fin (n + 1), (n.choose k.val : ℝ)) = (2 : ℝ) ^ n := by
…
```
theorem OAI.LeanBlast.GotsmanLinial.sum_choose_mul_index line 98
theorem OAI.LeanBlast.GotsmanLinial.sum_choose_mul_index_sq line 104
theorem OAI.LeanBlast.GotsmanLinial.sum_choose_centered_sq line 110
def OAI.LeanBlast.GotsmanLinial.binomialWeight line 119
Source documentation
The symmetric binomial probability weights, presented as a finite real function.
```
noncomputable def binomialWeight (n : ℕ) (k : Fin (n + 1)) : ℝ :=
…
```
theorem OAI.LeanBlast.GotsmanLinial.binomialWeight_nonneg line 122
theorem OAI.LeanBlast.GotsmanLinial.sum_binomialWeight line 126
theorem OAI.LeanBlast.GotsmanLinial.binomialWeight_mean line 130
theorem OAI.LeanBlast.GotsmanLinial.binomialWeight_variance line 137
theorem OAI.LeanBlast.GotsmanLinial.choose_reflect line 146
Source documentation
The binomial coefficients are invariant under reflection about n/2.
```
theorem choose_reflect (n : ℕ) (k : Fin (n + 1)) :
    n.choose (n - k.val) = n.choose k.val :=
…
```
theorem OAI.LeanBlast.GotsmanLinial.choose_rev line 150
theorem OAI.LeanBlast.GotsmanLinial.binomialWeight_rev line 154
theorem OAI.LeanBlast.GotsmanLinial.index_rev_real line 158

theorem OAI.LeanBlast.GotsmanLinial.binomialWeight_reflect line 163

Source documentation

Reflecting a binomial index preserves every real finite expectation.

theorem binomialWeight_reflect (n : ℕ) (φ : ℝ → ℝ) :
    (∑ k : Fin (n + 1), binomialWeight n k * φ ((n : ℝ) - (k.val : ℝ))) =
      ∑ k : Fin (n + 1), binomialWeight n k * φ (k.val : ℝ) := by
…

Mentions: OAI.LeanBlast.GotsmanLinial.binomialWeight

theorem OAI.LeanBlast.GotsmanLinial.binomialSigma_sq line 172
Source documentation
Standard deviation corresponding to the preceding finite variance identity.
```
theorem binomialSigma_sq (n : ℕ) : (Real.sqrt (n : ℝ) / 2) ^ 2 = (n : ℝ) / 4 := by
…
```
theorem OAI.LeanBlast.GotsmanLinial.binomialSigma_nonneg line 176