import PhysicsLogic.Framework.CoarseGrainedScaling

set_option autoImplicit false
noncomputable section

open MeasureTheory PhysicsLogic.Framework.StatisticalCoarseGraining

universe u v w p
variable {Micro : Type u} {Retained : Type v} {Further : Type w} {Parameter : Type p}
  [MeasurableSpace Micro] [MeasurableSpace Retained] [MeasurableSpace Further]

example (law : Measure Micro) (retain : Micro -> Retained) :
    (Data.mk law retain : Data Micro Retained).microscopicLaw = law ∧
      (Data.mk law retain : Data Micro Retained).retain = retain := ⟨rfl, rfl⟩

example (data : Data Micro Retained) :
    data.retainedLaw = data.microscopicLaw.map data.retain := rfl

example (data : Data Micro Retained) (microscopic : Micro -> Real) :
    data.RetainedObservableAt microscopic ↔
      ∃ observable : Retained -> Real, Measurable observable ∧
        microscopic = observable ∘ data.retain := Iff.rfl

example (data : Data Micro Retained) (family : Parameter -> Measure Retained) :
    data.ClosedInModelFamilyAt family ↔ ∃ parameter, family parameter = data.retainedLaw := Iff.rfl

example (data : Data Micro Retained) (observable : Retained -> Real) :
    data.NonvacuousRetainedPredictionAt observable ↔
      IsProbabilityMeasure data.microscopicLaw ∧ Measurable data.retain ∧
        Measurable observable ∧ IsProbabilityMeasure (data.retainedLaw.map observable) ∧
          data.retainedLaw.map observable = data.microscopicLaw.map (observable ∘ data.retain) := Iff.rfl

example (data : Data Micro Retained) (retainFurther : Retained -> Further) :
    data.followedBy retainFurther =
      (Data.mk data.microscopicLaw (retainFurther ∘ data.retain) : Data Micro Further) := rfl