FiniteCoupling.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

A finite one-sided coupling estimate

This is a finite weighted probabilistic estimate. Equal marginals are expressed as equality of the weighted expectations of every real function. The increment bound is required only on the support of the nonnegative probability weights.

theorem OAI.LeanBlast.GotsmanLinial.weighted_abs_le_of_second_moment line 24

Source documentation

Weighted Cauchy--Schwarz bounds the first absolute moment by a bound on the second moment. Zero weights are allowed.

theorem weighted_abs_le_of_second_moment (w f : Ω → ℝ) (σ : ℝ)
    (hw : ∀ i, 0 ≤ w i) (hprob : ∑ i, w i = 1) (hσ : 0 ≤ σ)
    (hsecond : ∑ i, w i * (f i) ^ 2 ≤ σ ^ 2) :
    ∑ i, w i * |f i| ≤ σ := by
…

theorem OAI.LeanBlast.GotsmanLinial.weighted_abs_eq_twice_positive_part line 46
Source documentation
A weighted mean-zero variable has absolute first moment twice the first moment of its positive part. This identity does not need positivity of the weights.
```
theorem weighted_abs_eq_twice_positive_part (w z : Ω → ℝ)
    (hzero : ∑ i, w i * z i = 0) :
    ∑ i, w i * |z i| = 2 * ∑ i, w i * max (z i) 0 := by
…
```

theorem OAI.LeanBlast.GotsmanLinial.finite_one_sided_coupling_bound line 69

Source documentation

The finite one-sided coupling lemma: identical marginals and an upper bound a on V - U bound the mean square displacement by 8 * a * σ.

The center m may be arbitrary. Taking it to be the common mean recovers the variance bound with variance σ²; only the displayed second moment is used.

theorem finite_one_sided_coupling_bound (w U V : Ω → ℝ) (m σ a : ℝ)
    (hw : ∀ i, 0 ≤ w i) (hprob : ∑ i, w i = 1)
    (hsame : ∀ φ : ℝ → ℝ, ∑ i, w i * φ (U i) = ∑ i, w i * φ (V i))
    (hσ : 0 ≤ σ) (ha : 0 ≤ a)
    (hvariance : ∑ i, w i * (U i - m) ^ 2 = σ ^ 2)
    (hstep : ∀ i, w i ≠ 0 → V i - U i ≤ a) :
    ∑ i, w i * (U i - V i) ^ 2 ≤ 8 * a * σ := by
…