OAI/Probability/FreeIsing/Ising/ObservationInnovation.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.Problem367.IsingObservationInnovation.Paths line 12
  2. def OAI.Problem367.IsingObservationInnovation.evaluation line 14
  3. theorem OAI.Problem367.IsingObservationInnovation.measurable_evaluation line 16
  4. def OAI.Problem367.IsingObservationInnovation.filtration line 20
  5. def OAI.Problem367.IsingObservationInnovation.posterior line 23
  6. theorem OAI.Problem367.IsingObservationInnovation.posterior_progressive line 26
  7. theorem OAI.Problem367.IsingObservationInnovation.posterior_norm_le_one line 34
  8. def OAI.Problem367.IsingObservationInnovation.innovationMap line 38
  9. theorem OAI.Problem367.IsingObservationInnovation.innovationMap_apply line 42
  10. theorem OAI.Problem367.IsingObservationInnovation.measurable_innovationMap line 46
  11. theorem OAI.Problem367.IsingObservationInnovation.innovationMap_zero line 51
  12. theorem OAI.Problem367.IsingObservationInnovation.innovationMap_causal line 55
  13. def OAI.Problem367.IsingObservationInnovation.uniformObservation line 66
  14. theorem OAI.Problem367.IsingObservationInnovation.measurable_uniformObservation line 71
  15. theorem OAI.Problem367.IsingObservationInnovation.innovationMap_uniformObservation line 82
  16. theorem OAI.Problem367.IsingObservationInnovation.uniformObservation_relabel line 87
  17. def OAI.Problem367.IsingObservationInnovation.observationLaw line 92
  18. theorem OAI.Problem367.IsingObservationInnovation.map_innovationMap_observationLaw line 95
  19. theorem OAI.Problem367.IsingObservationInnovation.innovationMap_relabel_ae line 110