OAI/Analysis/DiamondDistortion/FiniteAverage.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.DiamondDistortion.FiniteAverage.jensen_sq line 16
2. lemma OAI.DiamondDistortion.FiniteAverage.sum_mul_sq_le line 35
3. lemma OAI.DiamondDistortion.FiniteAverage.double_product line 44
4. lemma OAI.DiamondDistortion.FiniteAverage.norm_mean_le_sqrt line 55
5. lemma OAI.DiamondDistortion.FiniteAverage.pooled_mass line 70

   Source documentation

   Averaged opposite-sign cancellation, including the error's gate energy.

   lemma pooled_mass {κ : Type*} [Fintype κ]
       (w : Ω → ℝ) (hw : ∀ ω, 0 ≤ w ω) (hs : ∑ ω,w ω = 1)
       (b W : Ω → κ → ℝ) (V L : Ω → ℝ)
       (hmean : ∀ g, (∑ ω,w ω*b ω g) = -(∑ ω,w ω*W ω g))
       (hW : ∀ ω, (∑ g,W ω g ^ 2) ≤ V ω)
       (hopp : ∀ ω ν, (∑ g, (|b ω g| * |b ν g| - b ω g*b ν g)) ≤ L ω + L ν) :
       (∑ g, (∑ ω,w ω* |b ω g|)^2) ≤ (∑ ω,w ω*V ω) + 2*(∑ ω,w ω*L ω) := by
   …

6. lemma OAI.DiamondDistortion.FiniteAverage.joint_budget line 127
7. lemma OAI.DiamondDistortion.FiniteAverage.sqrt_pooled line 163