OAI/Probability/FreeIsing/Trees/InnovationPathMap.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Problem367.stronglyMeasurable_joint_of_isStronglyProgressive line 14
  2. theorem OAI.Problem367.measurable_nnrealTimePrimitive_of_progressive line 39
  3. theorem OAI.Problem367.nnrealTimePrimitive_congr_on_Iic line 51
  4. def OAI.Problem367.innovationPath line 61
  5. theorem OAI.Problem367.innovationPath_apply line 70
  6. theorem OAI.Problem367.innovationPath_zero line 77
  7. theorem OAI.Problem367.measurable_innovationPath line 85
  8. theorem OAI.Problem367.measurable_innovationPath_array line 98
  9. theorem OAI.Problem367.innovationPath_array_equivariant line 110
  10. theorem OAI.Problem367.innovationPath_array_causal line 125
  11. theorem OAI.Problem367.nnrealTimePrimitive_ae_eq_of_jointlyMeasurable line 144
  12. theorem OAI.Problem367.innovationPath_array_ae_equivariant line 166
  13. theorem OAI.Problem367.stronglyAdapted_causal_of_past_comap line 203
  14. theorem OAI.Problem367.innovationPath_array_causal_of_past_comap line 224