Bell's Common Probability Law

Exact root statement

∀ {HiddenState : Type v} [inst : MeasurableSpace HiddenState] (distribution : MeasureTheory.Measure HiddenState)
  (left right : { direction // ∑ i, direction i * direction i = 1 } → HiddenState → ℝ),
  distribution Set.univ = 1 →
    (∀ (setting : { direction // ∑ i, direction i * direction i = 1 }),
        MeasureTheory.AEStronglyMeasurable (left setting) distribution ∧
          MeasureTheory.AEStronglyMeasurable (right setting) distribution) →
      (∀ (setting : { direction // ∑ i, direction i * direction i = 1 }) (state : HiddenState),
          (left setting state = 1 ∨ left setting state = -1) ∧ (right setting state = 1 ∨ right setting state = -1)) →
        ¬∀ (a b : { direction // ∑ i, direction i * direction i = 1 }),
            ∫ (state : HiddenState), left a state * right b state ∂distribution = -∑ i, ↑a i * ↑b i