OAI/InformationTheory/AmplitudeDamping/SequentialProjections.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.GAD.sequential_union_bound line 12

   Source documentation

   The elementary sequential-projector union bound.

   theorem sequential_union_bound {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
       (P : ℕ → E → E) (hP : ∀ i x y, ⟪P i x, y-P i y⟫_ℝ = 0)
       (u : ℕ → E) (hu : ∀ i, u (i+1)=P i (u i)) (n : ℕ) :
       ‖u 0‖^2-‖u n‖^2 ≤ 4 * ∑ i ∈ Finset.range n, ‖u 0-P i (u 0)‖^2 := by
   …