diff --git a/docs/references.bib b/docs/references.bib index c8a86e1f14e79..02636ef768ace 100644 --- a/docs/references.bib +++ b/docs/references.bib @@ -1,6 +1,13 @@ + # To normalize: -# bibtool --preserve.key.case=on --preserve.keys=on --print.use.tab=off -s -i docs/references.bib -o docs/references.bib +# bibtool --preserve.key.case=on --preserve.keys=on --pass.comments=on --print.use.tab=off -s -i docs/references.bib -o docs/references.bib + +# https://www.zbmath.org/ and https://mathscinet.ams.org/mathscinet +# (or the free tool https://mathscinet.ams.org/mrlookup) +# are good sources of complete bibtex entries for mathematics +# To link to an entry in `references.bib`, use the following formats: +# [Author, *Title* (optional location)][bibkey] @Article{ ahrens2017, author = {Benedikt Ahrens and Peter LeFanu Lumsdaine}, year = {2019}, @@ -559,6 +566,22 @@ @Article{ MR32592 url = {https://doi.org/10.1090/S0002-9904-1949-09344-8} } +@Article{ MR3790629, + author = {Bell, J. S.}, + title = {On the {E}instein {P}odolsky {R}osen paradox}, + journal = {Phys. Phys. Fiz.}, + fjournal = {Physics Physique Fizika}, + volume = {1}, + year = {1964}, + number = {3}, + pages = {195--200}, + issn = {0554-128X}, + mrclass = {DML}, + mrnumber = {3790629}, + doi = {10.1103/PhysicsPhysiqueFizika.1.195}, + url = {https://doi.org/10.1103/PhysicsPhysiqueFizika.1.195} +} + @Article{ MR399081, author = {Hiblot, Jean-Jacques}, title = {Des anneaux euclidiens dont le plus petit algorithme n'est @@ -590,6 +613,24 @@ @InCollection{ MR541021 mrreviewer = {Daniel Lazard} } +@Article{ MR577178, + author = {Cirel\cprime son, B. S.}, + title = {Quantum generalizations of {B}ell's inequality}, + journal = {Lett. Math. Phys.}, + fjournal = {Letters in Mathematical Physics. A Journal for the Rapid + Dissemination of Short Contributions in the Field of + Mathematical Physics}, + volume = {4}, + year = {1980}, + number = {2}, + pages = {93--100}, + issn = {0377-9017}, + mrclass = {81B05}, + mrnumber = {577178}, + doi = {10.1007/BF00417500}, + url = {https://doi.org/10.1007/BF00417500} +} + @Misc{ ponton2020chebyshev, title = {Roots of {C}hebyshev polynomials: a purely algebraic approach}, @@ -746,3 +787,22 @@ @Misc{ wedhorn_adic year = {2019}, eprint = {arXiv:1910.05934} } + +@Article{ zbMATH06785026, + author = {John F. {Clauser} and Michael A. {Horne} and Abner + {Shimony} and Richard A. {Holt}}, + title = {{Proposed experiment to test local hidden-variable + theories}}, + fjournal = {{Physical Review Letters}}, + journal = {{Phys. Rev. Lett.}}, + issn = {0031-9007; 1079-7114/e}, + volume = {23}, + pages = {880--883}, + year = {1969}, + publisher = {American Physical Society (APS), New York, NY}, + language = {English}, + msc2010 = {81-05}, + zbl = {1371.81014}, + doi = {10.1103/PhysRevLett.23.880}, + url = {https://doi.org/10.1103/PhysRevLett.23.880} +} diff --git a/src/algebra/star/basic.lean b/src/algebra/star/basic.lean index 8c5b1b2840671..b7dbb0850fa2b 100644 --- a/src/algebra/star/basic.lean +++ b/src/algebra/star/basic.lean @@ -55,7 +55,7 @@ lemma star_injective [has_involutive_star R] : function.injective (star : R → has_involutive_star.star_involutive.injective /-- -A *-monoid is a monoid `R` with an involutive operations `star` +A `*`-monoid is a monoid `R` with an involutive operations `star` so `star (r * s) = star s * star r`. -/ class star_monoid (R : Type u) [monoid R] extends has_involutive_star R := @@ -82,8 +82,8 @@ end variables {R} /-- -A *-ring `R` is a (semi)ring with an involutive `star` operation which is additive -which makes `R` with its multiplicative structure into a *-monoid +A `*`-ring `R` is a (semi)ring with an involutive `star` operation which is additive +which makes `R` with its multiplicative structure into a `*`-monoid (i.e. `star (r * s) = star s * star r`). -/ class star_ring (R : Type u) [semiring R] extends star_monoid R := @@ -136,7 +136,7 @@ by simp [bit0] by simp [bit1] /-- -Any commutative semiring admits the trivial *-structure. +Any commutative semiring admits the trivial `*`-structure. -/ def star_ring_of_comm {R : Type*} [comm_semiring R] : star_ring R := { star := id, @@ -152,12 +152,12 @@ local attribute [instance] star_ring_of_comm end /-- -An ordered *-ring is a ring which is both an ordered ring and a *-ring, +An ordered `*`-ring is a ring which is both an ordered ring and a `*`-ring, and `0 ≤ star r * r` for every `r`. (In a Banach algebra, the natural ordering is given by the positive cone which is the closure of the sums of elements `star r * r`. -This ordering makes the Banach algebra an ordered *-ring.) +This ordering makes the Banach algebra an ordered `*`-ring.) -/ class star_ordered_ring (R : Type u) [ordered_semiring R] extends star_ring R := (star_mul_self_nonneg : ∀ r : R, 0 ≤ star r * r) diff --git a/src/algebra/star/chsh.lean b/src/algebra/star/chsh.lean new file mode 100644 index 0000000000000..eba51d6804c5f --- /dev/null +++ b/src/algebra/star/chsh.lean @@ -0,0 +1,274 @@ +/- +Copyright (c) 2020 Scott Morrison. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Scott Morrison. +-/ +import algebra.star.algebra +import algebra.algebra.ordered +import analysis.special_functions.pow + +/-! +# The Clauser-Horne-Shimony-Holt inequality and Tsirelson's inequality. + +We establish a version of the Clauser-Horne-Shimony-Holt (CHSH) inequality +(which is a generalization of Bell's inequality). +This is a foundational result which implies that +quantum mechanics is not a local hidden variable theory. + +As usually stated the CHSH inequality requires substantial language from physics and probability, +but it is possible to give a statement that is purely about ordered `*`-algebras. +We do that here, to avoid as many practical and logical dependencies as possible. +Since the algebra of observables of any quantum system is an ordered `*`-algebra +(in particular a von Neumann algebra) this is a strict generalization of the usual statement. + +Let `R` be a `*`-ring. + +A CHSH tuple in `R` consists of +* four elements `A₀ A₁ B₀ B₁ : R`, such that +* each `Aᵢ` and `Bⱼ` is a self-adjoint involution, and +* the `Aᵢ` commute with the `Bⱼ`. + +The physical interpretation is that the four elements are observables (hence self-adjoint) +that take values ±1 (hence involutions), and that the `Aᵢ` are spacelike separated from the `Bⱼ` +(and hence commute). + +The CHSH inequality says that when `R` is an ordered `*`-ring +(that is, a `*`-ring which is ordered, and for every `r : R`, `0 ≤ star r * r`), +which is moreover *commutative*, we have +`A₀ * B₀ + A₀ * B₁ + A₁ * B₀ - A₁ * B₁ ≤ 2` + +On the other hand, Tsirelson's inequality says that for any ordered `*`-ring we have +`A₀ * B₀ + A₀ * B₁ + A₁ * B₀ - A₁ * B₁ ≤ 2√2` + +(A caveat: in the commutative case we need 2⁻¹ in the ring, +and in the noncommutative case we need √2 and √2⁻¹. +To keep things simple we just assume our rings are ℝ-algebras.) + +The proofs I've seen in the literature either +assume a significant framework for quantum mechanics, +or assume the ring is a `C^*`-algebra. +In the `C^*`-algebra case, +the order structure is completely determined by the `*`-algebra structure: +`0 ≤ A` iff there exists some `B` so `A = star B * B`. +There's a nice proof of both bounds in this setting at +https://en.wikipedia.org/wiki/Tsirelson%27s_bound +The proof given here is purely algebraic. + +## Future work + +One can show that Tsirelson's inequality is tight. +In the `*`-ring of n-by-n complex matrices, if `A ≤ λ I` for some `λ : ℝ`, +then every eigenvalue has absolute value at most `λ`. +There is a CHSH tuple in 4-by-4 matrices such that +`A₀ * B₀ + A₀ * B₁ + A₁ * B₀ - A₁ * B₁` has `2√2` as an eigenvalue. + +## References + +* [Clauser, Horne, Shimony, Holt, + *Proposed experiment to test local hidden-variable theories*][zbMATH06785026] +* [Bell, *On the Einstein Podolsky Rosen Paradox*][MR3790629] +* [Tsirelson, *Quantum generalizations of Bell's inequality*][MR577178] + +-/ + +universes u + +/-- +A CHSH tuple in a `star_monoid R` consists of 4 self-adjoint involutions `A₀ A₁ B₀ B₁` such that +the `Aᵢ` commute with the `Bⱼ`. + +The physical interpretation is that `A₀` and `A₁` are a pair of boolean observables which +are spacelike separated from another pair `B₀` and `B₁` of boolean observables. +-/ +@[nolint has_inhabited_instance] +structure is_CHSH_tuple {R} [monoid R] [star_monoid R] (A₀ A₁ B₀ B₁ : R) := +(A₀_inv : A₀^2 = 1) (A₁_inv : A₁^2 = 1) (B₀_inv : B₀^2 = 1) (B₁_inv : B₁^2 = 1) +(A₀_sa : star A₀ = A₀) (A₁_sa : star A₁ = A₁) (B₀_sa : star B₀ = B₀) (B₁_sa : star B₁ = B₁) +(A₀B₀_commutes : A₀ * B₀ = B₀ * A₀) +(A₀B₁_commutes : A₀ * B₁ = B₁ * A₀) +(A₁B₀_commutes : A₁ * B₀ = B₀ * A₁) +(A₁B₁_commutes : A₁ * B₁ = B₁ * A₁) + +variables {R : Type u} + +/-- +Given a CHSH tuple (A₀, A₁, B₀, B₁) in a *commutative* ordered `*`-algebra over ℝ, +`A₀ * B₀ + A₀ * B₁ + A₁ * B₀ - A₁ * B₁ ≤ 2`. + +(We could work over ℤ[⅟2] if we wanted to!) +-/ +lemma CHSH_inequality_of_comm + [ordered_comm_ring R] [star_ordered_ring R] [algebra ℝ R] [ordered_semimodule ℝ R] + (A₀ A₁ B₀ B₁ : R) (T : is_CHSH_tuple A₀ A₁ B₀ B₁) : + A₀ * B₀ + A₀ * B₁ + A₁ * B₀ - A₁ * B₁ ≤ 2 := +begin + let P := (2 - A₀ * B₀ - A₀ * B₁ - A₁ * B₀ + A₁ * B₁), + have i₁ : 0 ≤ P, + { have idem : P * P = 4 * P, + { -- If we had a Gröbner basis algorithm, this would be trivial. + -- Without one, it is somewhat tedious! + dsimp [P], + simp only [add_mul, mul_add, sub_mul, mul_sub, mul_comm, mul_assoc, add_assoc], + repeat { conv in (B₀ * (A₀ * B₀)) + { rw [T.A₀B₀_commutes, ←mul_assoc B₀ B₀ A₀, ←pow_two, T.B₀_inv, one_mul], } }, + repeat { conv in (B₀ * (A₁ * B₀)) + { rw [T.A₁B₀_commutes, ←mul_assoc B₀ B₀ A₁, ←pow_two, T.B₀_inv, one_mul], } }, + repeat { conv in (B₁ * (A₀ * B₁)) + { rw [T.A₀B₁_commutes, ←mul_assoc B₁ B₁ A₀, ←pow_two, T.B₁_inv, one_mul], } }, + repeat { conv in (B₁ * (A₁ * B₁)) + { rw [T.A₁B₁_commutes, ←mul_assoc B₁ B₁ A₁, ←pow_two, T.B₁_inv, one_mul], } }, + conv in (A₀ * (B₀ * (A₀ * B₁))) + { rw [←mul_assoc, T.A₀B₀_commutes, mul_assoc, ←mul_assoc A₀, ←pow_two, T.A₀_inv, one_mul], }, + conv in (A₀ * (B₁ * (A₀ * B₀))) + { rw [←mul_assoc, T.A₀B₁_commutes, mul_assoc, ←mul_assoc A₀, ←pow_two, T.A₀_inv, one_mul], }, + conv in (A₁ * (B₀ * (A₁ * B₁))) + { rw [←mul_assoc, T.A₁B₀_commutes, mul_assoc, ←mul_assoc A₁, ←pow_two, T.A₁_inv, one_mul], }, + conv in (A₁ * (B₁ * (A₁ * B₀))) + { rw [←mul_assoc, T.A₁B₁_commutes, mul_assoc, ←mul_assoc A₁, ←pow_two, T.A₁_inv, one_mul], }, + simp only [←pow_two, T.A₀_inv, T.A₁_inv], + simp only [mul_comm A₁ A₀, mul_comm B₁ B₀, mul_left_comm A₁ A₀, mul_left_comm B₁ B₀, + mul_left_comm B₀ A₀, mul_left_comm B₀ A₁, mul_left_comm B₁ A₀, mul_left_comm B₁ A₁], + norm_num, + simp only [mul_comm _ (2 : R), mul_comm _ (4 : R), + mul_left_comm _ (2 : R), mul_left_comm _ (4 : R)], + abel, + simp only [neg_mul_eq_neg_mul_symm, mul_one, int.cast_bit0, one_mul, int.cast_one, + gsmul_eq_mul, int.cast_neg], + simp only [←mul_assoc, ←add_assoc], + norm_num, }, + have idem' : P = (1 / 4 : ℝ) • (P * P), + { have h : 4 * P = (4 : ℝ) • P := by simp [algebra.smul_def], + rw [idem, h, ←mul_smul], + norm_num, }, + have sa : star P = P, + { dsimp [P], + simp only [star_add, star_sub, star_mul, star_bit0, star_one, + T.A₀_sa, T.A₁_sa, T.B₀_sa, T.B₁_sa, mul_comm B₀, mul_comm B₁], }, + rw idem', + conv_rhs { congr, skip, congr, rw ←sa, }, + convert smul_le_smul_of_nonneg (star_mul_self_nonneg : 0 ≤ star P * P) _, + { simp, }, + { apply_instance, }, + { norm_num, }, }, + apply le_of_sub_nonneg, + simpa only [sub_add_eq_sub_sub, ←sub_add] using i₁, +end + +/-! +We now prove some rather specialized lemmas in preparation for the Tsirelson inequality, +which we hide in a namespace as they are unlikely to be useful elsewhere. +-/ +local notation `√2` := (real.sqrt 2 : ℝ) + +namespace tsirelson_inequality + +/-! +We next need some lemmas about numerals in modules and algebras. +The awkward appearance of both `•ℤ` and `•` seems unavoidable because later calculations by `abel` +will introduce `•ℤ`. +If anyone sees how to obtain these from general statements, please improve this! +-/ + +lemma two_gsmul_half_smul {α : Type*} [add_comm_group α] [module ℝ α] {X : α} : + 2 •ℤ (2⁻¹ : ℝ) • X = X := +by { rw [gsmul_eq_smul_cast ℝ, ←mul_smul]; norm_num, } + +lemma neg_two_gsmul_half_smul {α : Type*} [add_comm_group α] [module ℝ α] {X : α} : + (-2) •ℤ (2⁻¹ : ℝ) • X = - X := +by { rw [gsmul_eq_smul_cast ℝ, ←mul_smul]; norm_num, } + +lemma smul_two {α : Type*} [ring α] [algebra ℝ α] {x : ℝ} : + x • (2 : α) = (2 * x) • 1 := +by { rw [mul_comm 2 x, mul_smul], simp, } + +lemma smul_four {α : Type*} [ring α] [algebra ℝ α] {x : ℝ} : + x • (4 : α) = (4 * x) • 1 := +by { rw [mul_comm 4 x, mul_smul], simp, } + +/-! +Before proving Tsirelson's bound, +we prepare some easy lemmas about √2. +-/ + +-- This calculation, which we need for Tsirelson's bound, +-- defeated me. Thanks for the rescue from Shing Tak Lam! +lemma tsirelson_inequality_aux : √2 * √2 ^ 3 = √2 * (2 * √2⁻¹ + 4 * (√2⁻¹ * 2⁻¹)) := +begin + ring, + rw [mul_assoc, inv_mul_cancel, real.sqrt_eq_rpow, ←real.rpow_nat_cast, ←real.rpow_mul], + { norm_num, + rw show (2 : ℝ) ^ (2 : ℝ) = (2 : ℝ) ^ (2 : ℕ), by { rw ←real.rpow_nat_cast, norm_num }, + norm_num }, + { norm_num, }, + { norm_num, }, +end + +lemma sqrt_two_inv_mul_self : √2⁻¹ * √2⁻¹ = (2⁻¹ : ℝ) := +by { rw [←mul_inv'], norm_num, } + +end tsirelson_inequality +open tsirelson_inequality + +/-- +In a noncommutative ordered `*`-algebra over ℝ, +Tsirelson's bound for a CHSH tuple (A₀, A₁, B₀, B₁) is +`A₀ * B₀ + A₀ * B₁ + A₁ * B₀ - A₁ * B₁ ≤ 2^(3/2) • 1`. + +We prove this by providing an explicit sum-of-squares decomposition +of the difference. + +(We could work over `ℤ[2^(1/2), 2^(-1/2)]` if we really wanted to!) +-/ +lemma tsirelson_inequality + [ordered_ring R] [star_ordered_ring R] + [algebra ℝ R] [ordered_semimodule ℝ R] [star_algebra ℝ R] + (A₀ A₁ B₀ B₁ : R) (T : is_CHSH_tuple A₀ A₁ B₀ B₁) : + A₀ * B₀ + A₀ * B₁ + A₁ * B₀ - A₁ * B₁ ≤ √2^3 • 1 := +begin + let P := √2⁻¹ • (A₁ + A₀) - B₀, + let Q := √2⁻¹ • (A₁ - A₀) + B₁, + have w : √2^3 • 1 - A₀ * B₀ - A₀ * B₁ - A₁ * B₀ + A₁ * B₁ = √2⁻¹ • (P^2 + Q^2), + { dsimp [P, Q], + -- distribute out all the powers and products appearing on the RHS + simp only [pow_two, sub_mul, mul_sub, add_mul, mul_add, smul_add, smul_sub], + -- pull all coefficients out to the front, and combine `√2`s where possible + simp only [algebra.mul_smul_comm, algebra.smul_mul_assoc, ←mul_smul, sqrt_two_inv_mul_self], + -- replace Aᵢ * Aᵢ = 1 and Bᵢ * Bᵢ = 1 + simp only [←pow_two, T.A₀_inv, T.A₁_inv, T.B₀_inv, T.B₁_inv], + -- move Aᵢ to the left of Bᵢ + simp only [←T.A₀B₀_commutes, ←T.A₀B₁_commutes, ←T.A₁B₀_commutes, ←T.A₁B₁_commutes], + -- collect terms, simplify coefficients, and collect terms again: + abel, + simp only [two_gsmul_half_smul, neg_two_gsmul_half_smul], + abel, + -- these are identical, except the `_ • 1` terms don't quite match up + congr, + -- collect terms by hand, as we don't have an analogue of `abel` for modules + simp only [mul_one, int.cast_bit0, algebra.mul_smul_comm, int.cast_one, gsmul_eq_mul], + rw [smul_two, smul_four, ←add_smul], + -- just look at the coefficients now: + congr, + exact mul_left_cancel' (by norm_num) tsirelson_inequality_aux, }, + have pos : 0 ≤ √2⁻¹ • (P^2 + Q^2), { + have P_sa : star P = P, + { dsimp [P], + simp only [star_smul, star_add, star_sub, star_id_of_comm, + T.A₀_sa, T.A₁_sa, T.B₀_sa, T.B₁_sa], }, + have Q_sa : star Q = Q, + { dsimp [Q], + simp only [star_smul, star_add, star_sub, star_id_of_comm, + T.A₀_sa, T.A₁_sa, T.B₀_sa, T.B₁_sa], }, + have P2_nonneg : 0 ≤ P^2, + { rw [pow_two], + conv { congr, skip, congr, rw ←P_sa, }, + convert (star_mul_self_nonneg : 0 ≤ star P * P), }, + have Q2_nonneg : 0 ≤ Q^2, + { rw [pow_two], + conv { congr, skip, congr, rw ←Q_sa, }, + convert (star_mul_self_nonneg : 0 ≤ star Q * Q), }, + convert smul_le_smul_of_nonneg (add_nonneg P2_nonneg Q2_nonneg) + (le_of_lt (show 0 < √2⁻¹, by norm_num)), -- `norm_num` can't directly show `0 ≤ √2⁻¹` + simp, }, + apply le_of_sub_nonneg, + simpa only [sub_add_eq_sub_sub, ←sub_add, w] using pos, +end diff --git a/src/data/complex/basic.lean b/src/data/complex/basic.lean index 6c3807f097084..2cbb0bddfd908 100644 --- a/src/data/complex/basic.lean +++ b/src/data/complex/basic.lean @@ -615,8 +615,8 @@ With `z ≤ w` iff `w - z` is real and nonnegative, `ℂ` is a star ordered ring (That is, an ordered ring in which every element of the form `star z * z` is nonnegative.) In fact, the nonnegative elements are precisely those of this form. -This hold in any C*-algebra, e.g. `ℂ`, -but we don't yet have C*-algebras in mathlib. +This hold in any `C^*`-algebra, e.g. `ℂ`, +but we don't yet have `C^*`-algebras in mathlib. -/ def complex_star_ordered_ring : star_ordered_ring ℂ := { star_mul_self_nonneg := λ z, diff --git a/src/data/matrix/basic.lean b/src/data/matrix/basic.lean index 36937978b7391..dbaa30f51bcb1 100644 --- a/src/data/matrix/basic.lean +++ b/src/data/matrix/basic.lean @@ -801,7 +801,7 @@ section star_ring variables [decidable_eq n] {R : Type*} [semiring R] [star_ring R] /-- -When `R` is a *-(semi)ring, `matrix n n R` becomes a *-(semi)ring with +When `R` is a `*`-(semi)ring, `matrix n n R` becomes a `*`-(semi)ring with the star operation given by taking the conjugate, and the star of each entry. -/ instance : star_ring (matrix n n R) := diff --git a/src/data/real/basic.lean b/src/data/real/basic.lean index bb5e5168ef7d0..026b37aa748d3 100644 --- a/src/data/real/basic.lean +++ b/src/data/real/basic.lean @@ -84,7 +84,7 @@ instance : semigroup ℝ := by apply_instance instance : has_sub ℝ := by apply_instance instance : inhabited ℝ := ⟨0⟩ -/-- The real numbers are a *-ring, with the trivial *-structure. -/ +/-- The real numbers are a `*`-ring, with the trivial `*`-structure. -/ instance : star_ring ℝ := star_ring_of_comm /-- Coercion `ℚ` → `ℝ` as a `ring_hom`. Note that this @@ -218,7 +218,7 @@ noncomputable instance : linear_ordered_semiring ℝ := by apply_instance instance : domain ℝ := { .. real.nontrivial, .. real.comm_ring, .. linear_ordered_ring.to_domain } -/-- The real numbers are an ordered *-ring, with the trivial *-structure. -/ +/-- The real numbers are an ordered `*`-ring, with the trivial `*`-structure. -/ instance : star_ordered_ring ℝ := { star_mul_self_nonneg := λ r, mul_self_nonneg r, }