feat(algebra/star): the Bell/CHSH/Tsirelson inequalities (#4687)

Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
Co-authored-by: Rob Lewis <Rob.y.lewis@gmail.com>

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}
+}

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)