CHSH

📁 Source: Mathlib/Algebra/Star/CHSH.lean

Statistics

Metric	Count
Definitions IsCHSHTuple	1
Theorems CHSH_id, CHSH_inequality_of_comm, A₀B₀_commutes, A₀B₁_commutes, A₀_inv, A₀_sa, A₁B₀_commutes, A₁B₁_commutes, A₁_inv, A₁_sa, B₀_inv, B₀_sa, B₁_inv, B₁_sa, sqrt_two_inv_mul_self, tsirelson_inequality	16
Total	17

IsCHSHTuple

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
A₀B₀_commutes 📖	mathematical	IsCHSHTuple	MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass	—	—
A₀B₁_commutes 📖	mathematical	IsCHSHTuple	MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass	—	—
A₀_inv 📖	mathematical	IsCHSHTuple	Monoid.toNatPow MulOne.toOne MulOneClass.toMulOne Monoid.toMulOneClass	—	—
A₀_sa 📖	mathematical	IsCHSHTuple	Star.star InvolutiveStar.toStar StarMul.toInvolutiveStar MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass	—	—
A₁B₀_commutes 📖	mathematical	IsCHSHTuple	MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass	—	—
A₁B₁_commutes 📖	mathematical	IsCHSHTuple	MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass	—	—
A₁_inv 📖	mathematical	IsCHSHTuple	Monoid.toNatPow MulOne.toOne MulOneClass.toMulOne Monoid.toMulOneClass	—	—
A₁_sa 📖	mathematical	IsCHSHTuple	Star.star InvolutiveStar.toStar StarMul.toInvolutiveStar MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass	—	—
B₀_inv 📖	mathematical	IsCHSHTuple	Monoid.toNatPow MulOne.toOne MulOneClass.toMulOne Monoid.toMulOneClass	—	—
B₀_sa 📖	mathematical	IsCHSHTuple	Star.star InvolutiveStar.toStar StarMul.toInvolutiveStar MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass	—	—
B₁_inv 📖	mathematical	IsCHSHTuple	Monoid.toNatPow MulOne.toOne MulOneClass.toMulOne Monoid.toMulOneClass	—	—
B₁_sa 📖	mathematical	IsCHSHTuple	Star.star InvolutiveStar.toStar StarMul.toInvolutiveStar MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass	—	—

TsirelsonInequality

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
sqrt_two_inv_mul_self 📖	mathematical	—	Real Real.instMul Real.instInv Real.sqrt instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat	—	Nat.instAtLeastTwoHAddOfNat mul_inv Real.mul_self_sqrt Real.instIsOrderedRing

(root)

Definitions

Name	Category	Theorems
IsCHSHTuple 📖	CompData	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
CHSH_id 📖	mathematical	Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing	Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Distrib.toAdd SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup instOfNatAtLeastTwo AddMonoidWithOne.toNatCast Nat.instAtLeastTwoHAddOfNat	—	—
CHSH_inequality_of_comm 📖	mathematical	IsCHSHTuple MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring StarRing.toStarMul NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring	Preorder.toLE PartialOrder.toPreorder SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne CommRing.toRing Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Distrib.toMul instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Nat.instAtLeastTwoHAddOfNat	—	Nat.instAtLeastTwoHAddOfNat CHSH_id IsCHSHTuple.A₀_inv IsCHSHTuple.A₁_inv IsCHSHTuple.B₀_inv IsCHSHTuple.B₁_inv Algebra.smul_def map_ofNat RingHom.instRingHomClass SemigroupAction.mul_smul one_div inv_mul_cancel₀ IsStrictOrderedRing.toCharZero Real.instIsStrictOrderedRing one_smul StarAddMonoid.star_add star_sub star_ofNat StarMul.star_mul IsCHSHTuple.B₀_sa IsCHSHTuple.A₀_sa mul_comm IsCHSHTuple.B₁_sa IsCHSHTuple.A₁_sa smul_nonneg IsOrderedModule.toPosSMulMono PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsOrderedRing star_mul_self_nonneg le_of_sub_nonneg covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono IsOrderedCancelAddMonoid.toIsOrderedAddMonoid IsOrderedAddMonoid.toIsOrderedCancelAddMonoid StarOrderedRing.toIsOrderedAddMonoid sub_add_eq_sub_sub
tsirelson_inequality 📖	mathematical	IsCHSHTuple MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring StarRing.toStarMul NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring	Preorder.toLE PartialOrder.toPreorder SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Distrib.toMul Real Algebra.toSMul Real.instCommSemiring Monoid.toNatPow Real.instMonoid Real.sqrt instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne	—	Int.cast_smul_eq_zsmul SemigroupAction.mul_smul Nat.instAtLeastTwoHAddOfNat smul_add sq mul_sub mul_add Distrib.leftDistribClass sub_mul add_mul Distrib.rightDistribClass smul_sub Algebra.mul_smul_comm Algebra.smul_mul_assoc TsirelsonInequality.sqrt_two_inv_mul_self IsCHSHTuple.A₁_inv IsCHSHTuple.A₀_inv IsCHSHTuple.B₀_inv IsCHSHTuple.B₁_inv IsCHSHTuple.A₁B₀_commutes IsCHSHTuple.A₀B₀_commutes IsCHSHTuple.A₁B₁_commutes IsCHSHTuple.A₀B₁_commutes Mathlib.Tactic.Abel.subst_into_addg Mathlib.Tactic.Abel.unfold_sub Mathlib.Tactic.Abel.term_atomg Mathlib.Tactic.Abel.subst_into_negg Mathlib.Tactic.Abel.term_neg neg_zero Mathlib.Tactic.Abel.term_add_constg zero_add Mathlib.Tactic.Abel.termg_eq one_zsmul add_zero Mathlib.Tactic.Abel.const_add_termg Mathlib.Tactic.Abel.term_add_termg Mathlib.Meta.NormNum.IsNat.to_eq Mathlib.Meta.NormNum.isNat_add Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_neg Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.IsInt.neg_to_eq Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Abel.zero_termg neg_smul one_smul add_comm add_left_comm add_assoc Int.cast_ofNat Int.cast_neg neg_mul mul_inv_cancel_of_invertible IsStrictOrderedRing.toCharZero Real.instIsStrictOrderedRing star_sub StarModule.star_smul StarAddMonoid.star_add IsCHSHTuple.A₁_sa IsCHSHTuple.A₀_sa IsCHSHTuple.B₀_sa IsCHSHTuple.B₁_sa star_mul_self_nonneg Mathlib.Meta.Positivity.smul_nonneg_of_pos_of_nonneg IsOrderedModule.toPosSMulMono inv_pos_of_pos PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.sqrt_pos_of_pos Mathlib.Meta.Positivity.pos_of_isNat Real.instIsOrderedRing Real.instNontrivial Mathlib.Meta.NormNum.instAtLeastTwo add_nonneg IsOrderedAddMonoid.toAddLeftMono IsOrderedCancelAddMonoid.toIsOrderedAddMonoid IsOrderedAddMonoid.toIsOrderedCancelAddMonoid StarOrderedRing.toIsOrderedAddMonoid le_of_sub_nonneg covariant_swap_add_of_covariant_add sub_add_eq_sub_sub

---

← Back to Index