Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-03-04 02:11 8289518d

View on Github →

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

Estimated changes

Modified docs/references.bib

Modified src/algebra/star/basic.lean

Created src/algebra/star/chsh.lean

added theorem CHSH_inequality_of_comm

added structure is_CHSH_tuple

added theorem tsirelson_inequality.neg_two_gsmul_half_smul

added theorem tsirelson_inequality.smul_four

added theorem tsirelson_inequality.smul_two

added theorem tsirelson_inequality.sqrt_two_inv_mul_self

added theorem tsirelson_inequality.tsirelson_inequality_aux

added theorem tsirelson_inequality.two_gsmul_half_smul

added theorem tsirelson_inequality

Modified src/data/complex/basic.lean

Modified src/data/matrix/basic.lean

Modified src/data/real/basic.lean