OAI/Probability/FreeIsing/Trees/CutContinuationChannels.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.Problem367.CutContinuationChannels.ConeSample line 14
  2. def OAI.Problem367.CutContinuationChannels.globalCone line 17
  3. def OAI.Problem367.CutContinuationChannels.restrictCone line 21
  4. theorem OAI.Problem367.CutContinuationChannels.measurable_globalCone line 25
  5. theorem OAI.Problem367.CutContinuationChannels.measurable_restrictCone line 29
  6. def OAI.Problem367.CutContinuationChannels.globalFactors line 34
  7. def OAI.Problem367.CutContinuationChannels.continuationChannel line 38
  8. theorem OAI.Problem367.CutContinuationChannels.measurable_continuationChannel line 45
  9. theorem OAI.Problem367.CutContinuationChannels.continuationChannel_mem_Icc line 54
  10. theorem OAI.Problem367.CutContinuationChannels.continuationChannel_globalCone line 63
  11. def OAI.Problem367.CutContinuationChannels.averageChannel line 70
  12. theorem OAI.Problem367.CutContinuationChannels.measurable_averageChannel line 75
  13. theorem OAI.Problem367.CutContinuationChannels.averageChannel_mem_Icc line 81
  14. theorem OAI.Problem367.CutContinuationChannels.averageChannel_globalCone line 98
  15. theorem OAI.Problem367.CutContinuationChannels.path_average_le_averageChannel line 108
  16. theorem OAI.Problem367.CutContinuationChannels.integral_averageChannel_le line 120
  17. theorem OAI.Problem367.CutContinuationChannels.measure_path_average_ge_le line 155
  18. theorem OAI.Problem367.CutContinuationChannels.measure_restricted_path_average_ge_le_double_exp line 181