import PhysicsLogicConsumer.WorkSamplingTail

open PhysicsLogic.Framework PhysicsLogicConsumer.WorkSamplingTail MeasureTheory
open scoped BigOperators

local instance : MeasurableSpace Bool := ⊤

example : initial = FiniteCanonicalData.mk 1 (fun s : Bool => if s then Real.log 999999 else 0) := rfl
example : finalState = FiniteCanonicalData.mk 1
    (fun s : Bool => initial.energy s - if s then 20 else 0) := rfl
example : work = fun s : Bool => finalState.energy s - initial.energy s := rfl
example : law = initial.law := rfl
example : freeEnergy = finalState.freeEnergy - initial.freeEnergy := rfl
example : referenceMean = ∫ s, Real.exp (-work s) ∂law := rfl
example (n : Nat) (s : Fin n -> Bool) : sampleMean s = (∑ i, Real.exp (-work (s i))) / n := rfl
example (n : Nat) (s : Fin n -> Bool) : sampleFreeEnergy s = -Real.log (sampleMean s) := rfl
example (n : Nat) : sampleLaw n = Measure.pi (fun _ : Fin n => law) := rfl
example (n : Nat) : failureEvent n = {s | referenceMean / 4 < |sampleMean s - referenceMean|} := rfl