LCS.MeasurementLemmas

LCS
MeasurementLemmas
          import LCS.Basic
-- Lemma 1: Projectors for the same question commute
lemma measurement_system_projectors_commute
  {R : Type*} [Ring R] [StarRing R]
  {I : Type*} [Fintype I] (f : I → R) (h : IsMeasurementSystem f)
  (x y : I) : f x * f y = f y * f x := byR:Type u_1inst✝²:Ring Rinst✝¹:StarRing RI:Type u_2inst✝:Fintype If:I → Rh:IsMeasurementSystem fx:Iy:I⊢ f x * f y = f y * f x
  by_cases hxy : x = yposR:Type u_1inst✝²:Ring Rinst✝¹:StarRing RI:Type u_2inst✝:Fintype If:I → Rh:IsMeasurementSystem fx:Iy:Ihxy:x = y⊢ f x * f y = f y * f xnegR:Type u_1inst✝²:Ring Rinst✝¹:StarRing RI:Type u_2inst✝:Fintype If:I → Rh:IsMeasurementSystem fx:Iy:Ihxy:¬x = y⊢ f x * f y = f y * f x
  ·posR:Type u_1inst✝²:Ring Rinst✝¹:StarRing RI:Type u_2inst✝:Fintype If:I → Rh:IsMeasurementSystem fx:Iy:Ihxy:x = y⊢ f x * f y = f y * f x rw [hxy]All goals completed! 🐙
  ·negR:Type u_1inst✝²:Ring Rinst✝¹:StarRing RI:Type u_2inst✝:Fintype If:I → Rh:IsMeasurementSystem fx:Iy:Ihxy:¬x = y⊢ f x * f y = f y * f x have h_orth_xy : f x * f y = 0 := h.orthogonal x y hxynegR:Type u_1inst✝²:Ring Rinst✝¹:StarRing RI:Type u_2inst✝:Fintype If:I → Rh:IsMeasurementSystem fx:Iy:Ihxy:¬x = yh_orth_xy:f x * f y = 0 := h.orthogonal x y hxy⊢ f x * f y = f y * f x
    have h_orth_yx : f y * f x = 0 := h.orthogonal y x (Ne.symm hxy)negR:Type u_1inst✝²:Ring Rinst✝¹:StarRing RI:Type u_2inst✝:Fintype If:I → Rh:IsMeasurementSystem fx:Iy:Ihxy:¬x = yh_orth_xy:f x * f y = 0 := h.orthogonal x y hxyh_orth_yx:f y * f x = 0 := h.orthogonal y x (Ne.symm hxy)⊢ f x * f y = f y * f x
    rw [h_orth_xy, h_orth_yx]All goals completed! 🐙

-- Lemma 2: Sums of commuting projectors commute
lemma sum_of_commuting_projectors_commute
  {R : Type*} [Ring R] [StarRing R]
  {I : Type*} [Fintype I] (f : I → R) (h : IsMeasurementSystem f)
  (S T : Finset I) : 
  (∑ x ∈ S, f x) * (∑ y ∈ T, f y) = (∑ y ∈ T, f y) * (∑ x ∈ S, f x) := byR:Type u_1inst✝²:Ring Rinst✝¹:StarRing RI:Type u_2inst✝:Fintype If:I → Rh:IsMeasurementSystem fS:Finset IT:Finset I⊢ (∑ x ∈ S, f x) * ∑ y ∈ T, f y = (∑ y ∈ T, f y) * ∑ x ∈ S, f x
  -- Use distributivity to expand both sides
  rw [Finset.sum_mul, Finset.mul_sum]R:Type u_1inst✝²:Ring Rinst✝¹:StarRing RI:Type u_2inst✝:Fintype If:I → Rh:IsMeasurementSystem fS:Finset IT:Finset I⊢ ∑ i ∈ S, f i * ∑ y ∈ T, f y = ∑ i ∈ S, (∑ y ∈ T, f y) * f i
  apply Finset.sum_congr rflR:Type u_1inst✝²:Ring Rinst✝¹:StarRing RI:Type u_2inst✝:Fintype If:I → Rh:IsMeasurementSystem fS:Finset IT:Finset I⊢ ∀ x ∈ S, f x * ∑ y ∈ T, f y = (∑ y ∈ T, f y) * f x
  intro x hxR:Type u_1inst✝²:Ring Rinst✝¹:StarRing RI:Type u_2inst✝:Fintype If:I → Rh:IsMeasurementSystem fS:Finset IT:Finset Ix:Ihx:x ∈ S⊢ f x * ∑ y ∈ T, f y = (∑ y ∈ T, f y) * f x
  rw [Finset.mul_sum, Finset.sum_mul]R:Type u_1inst✝²:Ring Rinst✝¹:StarRing RI:Type u_2inst✝:Fintype If:I → Rh:IsMeasurementSystem fS:Finset IT:Finset Ix:Ihx:x ∈ S⊢ ∑ i ∈ T, f x * f i = ∑ i ∈ T, f i * f x
  apply Finset.sum_congr rflR:Type u_1inst✝²:Ring Rinst✝¹:StarRing RI:Type u_2inst✝:Fintype If:I → Rh:IsMeasurementSystem fS:Finset IT:Finset Ix:Ihx:x ∈ S⊢ ∀ x_1 ∈ T, f x * f x_1 = f x_1 * f x
  intro y hyR:Type u_1inst✝²:Ring Rinst✝¹:StarRing RI:Type u_2inst✝:Fintype If:I → Rh:IsMeasurementSystem fS:Finset IT:Finset Ix:Ihx:x ∈ Sy:Ihy:y ∈ T⊢ f x * f y = f y * f x
  exact measurement_system_projectors_commute f h x yAll goals completed! 🐙

-- Main lemma: Alice_A observables commute
lemma alice_observables_commute
  {R : Type*} [Ring R] [StarRing R] [Algebra ℂ R]
  {G : LCSLayout}
  (strat : LCSStrategy R G) (i : Fin G.r) (j j' : G.V i) :
  (Alice_A strat i j) * (Alice_A strat i j') = (Alice_A strat i j') * (Alice_A strat i j) := byR:Type u_1inst✝²:Ring Rinst✝¹:StarRing Rinst✝:Algebra ℂ RG:LCSLayoutstrat:LCSStrategy R Gi:Fin G.rj:↥(G.V i)j':↥(G.V i)⊢ Alice_A strat i j * Alice_A strat i j' = Alice_A strat i j' * Alice_A strat i j
  unfold Alice_AR:Type u_1inst✝²:Ring Rinst✝¹:StarRing Rinst✝:Algebra ℂ RG:LCSLayoutstrat:LCSStrategy R Gi:Fin G.rj:↥(G.V i)j':↥(G.V i)⊢ (∑ x with x j = 0, strat.E i x - ∑ x with x j = 1, strat.E i x) *
    (∑ x with x j' = 0, strat.E i x - ∑ x with x j' = 1, strat.E i x) =
  (∑ x with x j' = 0, strat.E i x - ∑ x with x j' = 1, strat.E i x) *
    (∑ x with x j = 0, strat.E i x - ∑ x with x j = 1, strat.E i x)
  let A := ∑ x ∈ Finset.univ.filter (fun x => x j = 0), strat.E i xR:Type u_1inst✝²:Ring Rinst✝¹:StarRing Rinst✝:Algebra ℂ RG:LCSLayoutstrat:LCSStrategy R Gi:Fin G.rj:↥(G.V i)j':↥(G.V i)A:R := ∑ x with x j = 0, strat.E i x⊢ (∑ x with x j = 0, strat.E i x - ∑ x with x j = 1, strat.E i x) *
    (∑ x with x j' = 0, strat.E i x - ∑ x with x j' = 1, strat.E i x) =
  (∑ x with x j' = 0, strat.E i x - ∑ x with x j' = 1, strat.E i x) *
    (∑ x with x j = 0, strat.E i x - ∑ x with x j = 1, strat.E i x) -- x_j = 0
  let B := ∑ x ∈ Finset.univ.filter (fun x => x j = 1), strat.E i xR:Type u_1inst✝²:Ring Rinst✝¹:StarRing Rinst✝:Algebra ℂ RG:LCSLayoutstrat:LCSStrategy R Gi:Fin G.rj:↥(G.V i)j':↥(G.V i)A:R := ∑ x with x j = 0, strat.E i xB:R := ∑ x with x j = 1, strat.E i x⊢ (∑ x with x j = 0, strat.E i x - ∑ x with x j = 1, strat.E i x) *
    (∑ x with x j' = 0, strat.E i x - ∑ x with x j' = 1, strat.E i x) =
  (∑ x with x j' = 0, strat.E i x - ∑ x with x j' = 1, strat.E i x) *
    (∑ x with x j = 0, strat.E i x - ∑ x with x j = 1, strat.E i x) -- x_j = 1
  let C := ∑ x ∈ Finset.univ.filter (fun x => x j' = 0), strat.E i xR:Type u_1inst✝²:Ring Rinst✝¹:StarRing Rinst✝:Algebra ℂ RG:LCSLayoutstrat:LCSStrategy R Gi:Fin G.rj:↥(G.V i)j':↥(G.V i)A:R := ∑ x with x j = 0, strat.E i xB:R := ∑ x with x j = 1, strat.E i xC:R := ∑ x with x j' = 0, strat.E i x⊢ (∑ x with x j = 0, strat.E i x - ∑ x with x j = 1, strat.E i x) *
    (∑ x with x j' = 0, strat.E i x - ∑ x with x j' = 1, strat.E i x) =
  (∑ x with x j' = 0, strat.E i x - ∑ x with x j' = 1, strat.E i x) *
    (∑ x with x j = 0, strat.E i x - ∑ x with x j = 1, strat.E i x) -- x_j' = 0
  let D := ∑ x ∈ Finset.univ.filter (fun x => x j' = 1), strat.E i xR:Type u_1inst✝²:Ring Rinst✝¹:StarRing Rinst✝:Algebra ℂ RG:LCSLayoutstrat:LCSStrategy R Gi:Fin G.rj:↥(G.V i)j':↥(G.V i)A:R := ∑ x with x j = 0, strat.E i xB:R := ∑ x with x j = 1, strat.E i xC:R := ∑ x with x j' = 0, strat.E i xD:R := ∑ x with x j' = 1, strat.E i x⊢ (∑ x with x j = 0, strat.E i x - ∑ x with x j = 1, strat.E i x) *
    (∑ x with x j' = 0, strat.E i x - ∑ x with x j' = 1, strat.E i x) =
  (∑ x with x j' = 0, strat.E i x - ∑ x with x j' = 1, strat.E i x) *
    (∑ x with x j = 0, strat.E i x - ∑ x with x j = 1, strat.E i x) -- x_j' = 1
  change (A - B) * (C - D) = (C - D) * (A - B)R:Type u_1inst✝²:Ring Rinst✝¹:StarRing Rinst✝:Algebra ℂ RG:LCSLayoutstrat:LCSStrategy R Gi:Fin G.rj:↥(G.V i)j':↥(G.V i)A:R := ∑ x with x j = 0, strat.E i xB:R := ∑ x with x j = 1, strat.E i xC:R := ∑ x with x j' = 0, strat.E i xD:R := ∑ x with x j' = 1, strat.E i x⊢ (A - B) * (C - D) = (C - D) * (A - B)
  have h_AC : A * C = C * A := byR:Type u_1inst✝²:Ring Rinst✝¹:StarRing Rinst✝:Algebra ℂ RG:LCSLayoutstrat:LCSStrategy R Gi:Fin G.rj:↥(G.V i)j':↥(G.V i)⊢ Alice_A strat i j * Alice_A strat i j' = Alice_A strat i j' * Alice_A strat i j
    apply sum_of_commuting_projectors_commutehR:Type u_1inst✝²:Ring Rinst✝¹:StarRing Rinst✝:Algebra ℂ RG:LCSLayoutstrat:LCSStrategy R Gi:Fin G.rj:↥(G.V i)j':↥(G.V i)A:R := ∑ x with x j = 0, strat.E i xB:R := ∑ x with x j = 1, strat.E i xC:R := ∑ x with x j' = 0, strat.E i xD:R := ∑ x with x j' = 1, strat.E i x⊢ IsMeasurementSystem (strat.E i)
    exact strat.alice_ms iAll goals completed! 🐙
  have h_AD : A * D = D * A := byR:Type u_1inst✝²:Ring Rinst✝¹:StarRing Rinst✝:Algebra ℂ RG:LCSLayoutstrat:LCSStrategy R Gi:Fin G.rj:↥(G.V i)j':↥(G.V i)⊢ Alice_A strat i j * Alice_A strat i j' = Alice_A strat i j' * Alice_A strat i j
    apply sum_of_commuting_projectors_commutehR:Type u_1inst✝²:Ring Rinst✝¹:StarRing Rinst✝:Algebra ℂ RG:LCSLayoutstrat:LCSStrategy R Gi:Fin G.rj:↥(G.V i)j':↥(G.V i)A:R := ∑ x with x j = 0, strat.E i xB:R := ∑ x with x j = 1, strat.E i xC:R := ∑ x with x j' = 0, strat.E i xD:R := ∑ x with x j' = 1, strat.E i xh_AC:A * C = C * A := sum_of_commuting_projectors_commute (strat.E i) (strat.alice_ms i) {x | x j = 0} {x | x j' = 0}⊢ IsMeasurementSystem (strat.E i)
    exact strat.alice_ms iAll goals completed! 🐙
  have h_BC : B * C = C * B := byR:Type u_1inst✝²:Ring Rinst✝¹:StarRing Rinst✝:Algebra ℂ RG:LCSLayoutstrat:LCSStrategy R Gi:Fin G.rj:↥(G.V i)j':↥(G.V i)⊢ Alice_A strat i j * Alice_A strat i j' = Alice_A strat i j' * Alice_A strat i j
    apply sum_of_commuting_projectors_commutehR:Type u_1inst✝²:Ring Rinst✝¹:StarRing Rinst✝:Algebra ℂ RG:LCSLayoutstrat:LCSStrategy R Gi:Fin G.rj:↥(G.V i)j':↥(G.V i)A:R := ∑ x with x j = 0, strat.E i xB:R := ∑ x with x j = 1, strat.E i xC:R := ∑ x with x j' = 0, strat.E i xD:R := ∑ x with x j' = 1, strat.E i xh_AC:A * C = C * A := sum_of_commuting_projectors_commute (strat.E i) (strat.alice_ms i) {x | x j = 0} {x | x j' = 0}h_AD:A * D = D * A := sum_of_commuting_projectors_commute (strat.E i) (strat.alice_ms i) {x | x j = 0} {x | x j' = 1}⊢ IsMeasurementSystem (strat.E i)
    exact strat.alice_ms iAll goals completed! 🐙
  have h_BD : B * D = D * B := byR:Type u_1inst✝²:Ring Rinst✝¹:StarRing Rinst✝:Algebra ℂ RG:LCSLayoutstrat:LCSStrategy R Gi:Fin G.rj:↥(G.V i)j':↥(G.V i)⊢ Alice_A strat i j * Alice_A strat i j' = Alice_A strat i j' * Alice_A strat i j
    apply sum_of_commuting_projectors_commutehR:Type u_1inst✝²:Ring Rinst✝¹:StarRing Rinst✝:Algebra ℂ RG:LCSLayoutstrat:LCSStrategy R Gi:Fin G.rj:↥(G.V i)j':↥(G.V i)A:R := ∑ x with x j = 0, strat.E i xB:R := ∑ x with x j = 1, strat.E i xC:R := ∑ x with x j' = 0, strat.E i xD:R := ∑ x with x j' = 1, strat.E i xh_AC:A * C = C * A := sum_of_commuting_projectors_commute (strat.E i) (strat.alice_ms i) {x | x j = 0} {x | x j' = 0}h_AD:A * D = D * A := sum_of_commuting_projectors_commute (strat.E i) (strat.alice_ms i) {x | x j = 0} {x | x j' = 1}h_BC:B * C = C * B := sum_of_commuting_projectors_commute (strat.E i) (strat.alice_ms i) {x | x j = 1} {x | x j' = 0}⊢ IsMeasurementSystem (strat.E i)
    exact strat.alice_ms iAll goals completed! 🐙
  simp [mul_sub, sub_mul]R:Type u_1inst✝²:Ring Rinst✝¹:StarRing Rinst✝:Algebra ℂ RG:LCSLayoutstrat:LCSStrategy R Gi:Fin G.rj:↥(G.V i)j':↥(G.V i)A:R := ∑ x with x j = 0, strat.E i xB:R := ∑ x with x j = 1, strat.E i xC:R := ∑ x with x j' = 0, strat.E i xD:R := ∑ x with x j' = 1, strat.E i xh_AC:A * C = C * A := sum_of_commuting_projectors_commute (strat.E i) (strat.alice_ms i) {x | x j = 0} {x | x j' = 0}h_AD:A * D = D * A := sum_of_commuting_projectors_commute (strat.E i) (strat.alice_ms i) {x | x j = 0} {x | x j' = 1}h_BC:B * C = C * B := sum_of_commuting_projectors_commute (strat.E i) (strat.alice_ms i) {x | x j = 1} {x | x j' = 0}h_BD:B * D = D * B := sum_of_commuting_projectors_commute (strat.E i) (strat.alice_ms i) {x | x j = 1} {x | x j' = 1}⊢ A * C - B * C - (A * D - B * D) = C * A - D * A - (C * B - D * B)
  simp [h_AC, h_AD, h_BC, h_BD]R:Type u_1inst✝²:Ring Rinst✝¹:StarRing Rinst✝:Algebra ℂ RG:LCSLayoutstrat:LCSStrategy R Gi:Fin G.rj:↥(G.V i)j':↥(G.V i)A:R := ∑ x with x j = 0, strat.E i xB:R := ∑ x with x j = 1, strat.E i xC:R := ∑ x with x j' = 0, strat.E i xD:R := ∑ x with x j' = 1, strat.E i xh_AC:A * C = C * A := sum_of_commuting_projectors_commute (strat.E i) (strat.alice_ms i) {x | x j = 0} {x | x j' = 0}h_AD:A * D = D * A := sum_of_commuting_projectors_commute (strat.E i) (strat.alice_ms i) {x | x j = 0} {x | x j' = 1}h_BC:B * C = C * B := sum_of_commuting_projectors_commute (strat.E i) (strat.alice_ms i) {x | x j = 1} {x | x j' = 0}h_BD:B * D = D * B := sum_of_commuting_projectors_commute (strat.E i) (strat.alice_ms i) {x | x j = 1} {x | x j' = 1}⊢ C * A - C * B - (D * A - D * B) = C * A - D * A - (C * B - D * B)
  abelAll goals completed! 🐙