import PhysicsLogicConsumer.BellLocality

open PhysicsLogic.Framework.DeterministicLocalResponse
open PhysicsLogicConsumer.BellLocality.Averaging

noncomputable section

example (r : LocalResponses Bool Bool Bool) : r = ⟨r.left, r.right⟩ := rfl
example (r : BipartiteResponses Bool Bool Bool) : r = ⟨r.left, r.right⟩ := rfl
example (r : BipartiteResponses Bool Bool Bool) (l : LocalResponses Bool Bool Bool) :
    Factorizes r l ↔ ∀ a b h, r.left a b h = l.left a h ∧ r.right a b h = l.right b h := Iff.rfl
example (r : BipartiteResponses Bool Bool Bool) (a b h x y : Bool) :
    (responsePossibility r).possible a b h x y ↔ r.left a b h = x ∧ r.right a b h = y := Iff.rfl
example (r : BipartiteResponses Bool Bool Bool) : AdmitsLocalFactorization r ↔
    ∃ l : LocalResponses Bool Bool Bool, ∀ a b h, r.left a b h = l.left a h ∧ r.right a b h = l.right b h := Iff.rfl
example (r : BipartiteResponses Bool Bool Bool) (law : PMF Bool) (a b : Bool) :
    outcomeLaw r law a b = law.map (fun h => (r.left a b h, r.right a b h)) := rfl
example : fairCoin = PMF.bernoulli (1 / 2) (by norm_num) := rfl
example : remotePermutation = ({
    left := fun _ b h => Bool.xor b h
    right := fun _ _ h => h } : BipartiteResponses Bool Bool Bool) := rfl
example : localRealization = ({
    left := fun _ _ h => h
    right := fun _ b h => Bool.xor b h } : BipartiteResponses Bool Bool Bool) := rfl

end