OAI/Probability/FreeIsing/Ising/ConditionalCopyBounds.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.Problem367.IsingConditionalCopyBounds.CopySpace line 17
  2. def OAI.Problem367.IsingConditionalCopyBounds.graphLaw line 19
  3. instance OAI.Problem367.IsingConditionalCopyBounds.graphLaw_isProbabilityMeasure line 23
  4. theorem OAI.Problem367.IsingConditionalCopyBounds.hasLaw_observationLaw_eval line 30
  5. theorem OAI.Problem367.IsingConditionalCopyBounds.progressive_leftObservation line 63
  6. theorem OAI.Problem367.IsingConditionalCopyBounds.progressive_rightObservation line 81
  7. def OAI.Problem367.IsingConditionalCopyBounds.fieldDifference line 99
  8. theorem OAI.Problem367.IsingConditionalCopyBounds.measurePreserving_observation_copies line 109
  9. theorem OAI.Problem367.IsingConditionalCopyBounds.ae_innovationMap_copies line 126
  10. theorem OAI.Problem367.IsingConditionalCopyBounds.identDistrib_observation_copies line 142
  11. theorem OAI.Problem367.IsingConditionalCopyBounds.ae_all_innovation_identities line 159
  12. theorem OAI.Problem367.IsingConditionalCopyBounds.ae_initial_observation_eq line 175
  13. theorem OAI.Problem367.IsingConditionalCopyBounds.ae_initial_fieldDifference_zero line 186
  14. theorem OAI.Problem367.IsingConditionalCopyBounds.initial_fieldDifference_secondMoment_zero line 193
  15. theorem OAI.Problem367.IsingConditionalCopyBounds.ae_fieldDifference_bound line 201
  16. theorem OAI.Problem367.IsingConditionalCopyBounds.fieldDifference_secondMoment_bounds line 213
  17. theorem OAI.Problem367.IsingConditionalCopyBounds.fieldDifference_joint_bounds line 226
  18. theorem OAI.Problem367.IsingConditionalCopyBounds.canonical_fieldDifference_bound line 245