import PhysicsLogicConsumer.PeriodicSampling

open PhysicsLogicConsumer.PeriodicSampling
open PhysicsLogic.Framework
open scoped BigOperators

example (state : Bool) : target state = (1 : Real) / 2 := rfl

example (initial state : Bool) : prepared initial state = (if state = initial then 1 else 0 : Real) := rfl

example (switching : Real) : update switching = ({
    transition := fun initial final => if final = initial then 1 - switching else switching
  } : FiniteTransitionKernel Bool) := rfl

example (state : Bool) : signal state = (if state then 1 else -1 : Real) := rfl

example (initial : Bool) : trajectory initial 0 = initial := rfl

example (initial : Bool) (steps : Nat) : trajectory initial (steps + 1) = !(trajectory initial steps) := rfl

example (initial : Bool) (count : Nat) : sampleMean initial count =
    (∑ step ∈ Finset.range count, (if trajectory initial step then 1 else -1 : Real)) / (count : Real) := rfl