def definition def or abbrev

`quantumCorrelation`

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

formal statement (Lean)

  68noncomputable def quantumCorrelation (θ_A θ_B : ℝ) : ℝ :=

Definition body.

  69  -Real.cos (θ_A - θ_B)
  70
  71/-- The CHSH Bell inequality. -/

From the project-wide theorem graph. These declarations reference this one in their body.

chshCombination in IndisputableMonolith.Quantum.BellInequality decl_use
optimal_chsh_value in IndisputableMonolith.Quantum.BellInequality decl_use
perfect_anticorrelation in IndisputableMonolith.Quantum.BellInequality decl_use
quantumCorrelation in IndisputableMonolith.Quantum.BellInequality decl_use
quantum_correlation_bounded in IndisputableMonolith.Quantum.BellInequality decl_use

Lean names referenced from this declaration's body.