Completing a nearby submeasurement #
The paper's lem:replace-with-measurement, with the explicit estimate
2 δ + 4 sqrt δ for the squared state norm. The outcome alphabet contributes no factor.
Stated for a state model (Phase 4 of planning/mipco-track.md), with the positivity of the
families on the represented operators, as in StateModel.qform_sum_ge_of_close: the joint
algebra of a model need not be ordered.
theorem
MIPRE.Introspection.submeasurement_completion_mass
{𝒞 : Type u_1}
[Ring 𝒞]
[StarRing 𝒞]
[Algebra ℂ 𝒞]
(Ψ : StateModel 𝒞)
{A : Type u_2}
[Fintype A]
(hΨ : ‖Ψ.ψ‖ = 1)
(B C : A → 𝒞)
(hB : ∀ (a : A), 0 ≤ Ψ.π (B a))
(hC : ∀ (a : A), 0 ≤ Ψ.π (C a))
(hCsum : ∑ a : A, C a = 1)
(hBC : ∀ (a : A), Ψ.π (B a) ≤ Ψ.π (C a))
:
Completing a positive submeasurement dominated by a POVM costs at most its missing mass.
theorem
MIPRE.Introspection.submeasurement_completion_dist
{𝒞 : Type u_1}
[Ring 𝒞]
[StarRing 𝒞]
[Algebra ℂ 𝒞]
(Ψ : StateModel 𝒞)
{A : Type u_2}
[Fintype A]
(hΨ : ‖Ψ.ψ‖ = 1)
(P B C : A → 𝒞)
(hP : IsPVMIn P)
(hB : ∀ (a : A), 0 ≤ Ψ.π (B a))
(hC : ∀ (a : A), 0 ≤ Ψ.π (C a))
(hCsum : ∑ a : A, C a = 1)
(hBC : ∀ (a : A), Ψ.π (B a) ≤ Ψ.π (C a))
{δ : ℝ}
(hclose : ∑ a : A, Ψ.snorm (P a - B a) ^ 2 ≤ δ)
:
A POVM completing a nearby submeasurement stays close to the original PVM.
theorem
MIPRE.Introspection.submeasurement_completion_dist_avg
{𝒞 : Type u_1}
[Ring 𝒞]
[StarRing 𝒞]
[Algebra ℂ 𝒞]
(Ψ : StateModel 𝒞)
{A : Type u_2}
[Fintype A]
{X : Type u_3}
[Fintype X]
(D : X → ℝ)
(hD0 : ∀ (x : X), 0 ≤ D x)
(hD1 : ∑ x : X, D x = 1)
(hΨ : ‖Ψ.ψ‖ = 1)
(P B C : X → A → 𝒞)
(hP : ∀ (x : X), IsPVMIn (P x))
(hB : ∀ (x : X) (a : A), 0 ≤ Ψ.π (B x a))
(hC : ∀ (x : X) (a : A), 0 ≤ Ψ.π (C x a))
(hCsum : ∀ (x : X), ∑ a : A, C x a = 1)
(hBC : ∀ (x : X) (a : A), Ψ.π (B x a) ≤ Ψ.π (C x a))
{δ : ℝ}
(hclose : ∑ x : X, D x * ∑ a : A, Ψ.snorm (P x a - B x a) ^ 2 ≤ δ)
:
Averaging preserves the completion estimate, by concavity of the square root.