import PhysicsLogic.Papers.Bell1964.CommonProbabilityLaw

set_option autoImplicit false
noncomputable section
open MeasureTheory PhysicsLogic.Papers.Bell1964
open PhysicsLogic.Papers.Bell1964.BellFramework
open PhysicsLogic.Papers.Bell1964.CommonProbabilityLaw
universe u v
variable {S : Type u} {H : Type v} [MeasurableSpace H] (data : CommonProbabilityLaw S H)

example : CommonProbabilityLaw S H → Measure H := CommonProbabilityLaw.distribution
example : CommonProbabilityLaw S H → LocalResponses S H := CommonProbabilityLaw.responses
example : data = { distribution := data.distribution, responses := data.responses } := rfl
example (outcome : Outcome) : singleSpinOutcomeValue outcome =
    match outcome with | .plus => 1 | .minus => -1 := by cases outcome <;> rfl
example : data.Normalized ↔ data.distribution Set.univ = 1 := Iff.rfl
example : data.MeasurableResponses ↔ ∀ s,
    AEStronglyMeasurable (fun h => singleSpinOutcomeValue (data.responses.left s h)) data.distribution ∧
    AEStronglyMeasurable (fun h => singleSpinOutcomeValue (data.responses.right s h)) data.distribution := Iff.rfl
example (a b : S) : data.correlation a b = ∫ h,
    singleSpinOutcomeValue (data.responses.left a h) *
      singleSpinOutcomeValue (data.responses.right b h) ∂data.distribution := rfl
example (s : S) : data.OppositeAlmostEverywhereAt s ↔ ∀ᵐ h ∂data.distribution,
    singleSpinOutcomeValue (data.responses.left s h) =
      -singleSpinOutcomeValue (data.responses.right s h) := Iff.rfl
example : data.PerfectAnticorrelation ↔ ∀ s, data.correlation s s = -1 := Iff.rfl
example : UnitSetting = {direction : SpinDirection // direction.dot direction = 1} := rfl
example (spinData : CommonProbabilityLaw UnitSetting H) : spinData.ReproducesSinglet ↔
    ∀ a b, spinData.correlation a b = -(a.val.dot b.val) := Iff.rfl