import PhysicsLogicConsumer.RejectedMoves

open PhysicsLogicConsumer.RejectedMoves
open PhysicsLogic.Framework
open scoped BigOperators

example (state : Bool) : energy state = (if state then Real.log 2 else 0) := rfl
example (state : Bool) : target state = (if state then 1 / 3 else 2 / 3 : Real) := rfl
example (q : Real) (before after : Bool) :
    proposal q before after = (if after = before then 1 - q else q) := rfl
example (before after : Bool) :
    acceptance before after = min 1 (Real.exp (energy before - energy after)) := rfl
example (q : Real) (before after : Bool) :
    acceptedMass q before after = proposal q before after * acceptance before after := rfl
example (q : Real) (before : Bool) :
    acceptanceRate q before = ∑ after, proposal q before after * acceptance before after := rfl

example (q : Real) : attempts q = ({
    transition := fun before after => acceptedMass q before after +
      if after = before then 1 - (∑ next, acceptedMass q before next) else 0
  } : FiniteTransitionKernel Bool) := rfl

example (q : Real) : retained q = ({
    transition := fun before after => acceptedMass q before after / ∑ next, acceptedMass q before next
  } : FiniteTransitionKernel Bool) := rfl

example (q : Real) (state : Bool) : retainedLaw q state =
    target state * acceptanceRate q state / ∑ next, target next * acceptanceRate q next := rfl

example (q : Real) (before after : Bool) (count : Nat) : firstAcceptedBy q before after count =
    ∑ rejected ∈ Finset.range count,
      (1 - acceptanceRate q before) ^ rejected * (proposal q before after * acceptance before after) := rfl

example (q : Real) (state : Bool) : reweightedLaw q state =
    (retainedLaw q state / acceptanceRate q state) /
      ∑ next, retainedLaw q next / acceptanceRate q next := rfl
example (state : Bool) : prepared state = (if state then 0 else 1 : Real) := rfl