import PhysicsLogic.Paradigm.CosmologicalInference

open PhysicsLogic.Paradigm.CosmologicalInference

universe u v w z
variable {Model : Type u} {Realization : Type v} {Observable : Type w} {Estimate : Type z}

example (context : EnsembleSamplingContext Model Realization Observable Estimate)
    (model : Model) (observable : Observable) :
    context.SamplingVariationAt model observable =
      (∃ first second, context.possibleUnder first model ∧ context.possibleUnder second model ∧
        context.observableIn observable first ∧ context.observableIn observable second ∧
          context.estimateFrom first observable ≠ context.estimateFrom second observable) := rfl

example (context : EnsembleSamplingContext Model Realization Observable Estimate)
    (model : Model) (observable : Observable) :
    context.RecoversEnsembleTargetFromEveryRealization model observable =
      (∀ sample, context.possibleUnder sample model → context.observableIn observable sample →
        context.estimateFrom sample observable = context.ensembleTarget model observable) := rfl

open Countermodels

example (reading : Nat) (upper : Bool) :
    separatedReadingModels.possibleUnder reading upper =
      (if upper then reading = 4 ∨ reading = 6 else reading = 0 ∨ reading = 2) := rfl

example (reading : Nat) : separatedReadingModels.observableIn () reading =
    (reading = 0 ∨ reading = 2 ∨ reading = 4 ∨ reading = 6) := rfl

example (reading : Nat) : separatedReadingModels.estimateFrom reading () = reading := rfl

example (upper : Bool) : separatedReadingModels.ensembleTarget upper () =
    (if upper then 5 else 1) := rfl