FinitePacking.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.GAD.iid_coordinate line 14
theorem OAI.GAD.iid_pair line 25

theorem OAI.GAD.exists_le_weighted_average line 54

Source documentation

A finite average cannot be strictly below every sampled value.

theorem exists_le_weighted_average (q : α → ℝ) (hq : ∀ a, 0 ≤ q a)
    (hs : ∑ a, q a=1) (f : α → ℝ) : ∃ a, f a ≤ ∑ b, q b*f b := by
…

theorem OAI.GAD.packing_cross_bound line 78

theorem OAI.GAD.exists_packed_measurement line 110

Source documentation

Finite iid quantum packing, using an explicit sequential collective POVM.

theorem exists_packed_measurement (q : α → ℝ) (hq : ∀ a, 0 ≤ q a) (hs : ∑ a, q a=1)
    (A Q : α → Matrix ι ι ℂ) (hA : ∀ a, IsState (A a)) (hQ : ∀ a, IsProjection (Q a))
    (P : Matrix ι ι ℂ) (hP : IsProjection P) {a b c r : ℝ} (hc : 0 ≤ c) (hr0 : 0 ≤ r)
    (hga : (∑ x, q x*(1-(P*A x).trace.re)) ≤ a)
    (hcb : (∑ x, q x*(1-(Q x*A x).trace.re)) ≤ b)
    (hr : ∀ x, (Q x).trace.re ≤ r)
    (hcp : (c • P-P*(∑ x, q x • A x)*P).PosSemidef)
    (M : ℕ) (hM : 0 < M) :
    ∃ (x : Fin M → α) (D : Fin M → Matrix ι ι ℂ),
      (∀ m, (D m).PosSemidef) ∧ (∑ m, D m=1) ∧
      1-(∑ m, (D m*A (x m)).trace.re)/(M:ℝ) ≤ 9*a+8*b+4*(M:ℝ)*c*r := by
…

Mentions: OAI.GAD.IsState, OAI.GAD.IsProjection