OAI/Analysis/IntegralMeans/ExpectedTransport.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.Brennan.lintegral_Icc_inv line 26
  2. lemma OAI.Brennan.lintegral_transportBox_inv line 36
  3. def OAI.Brennan.rootJac line 54
  4. lemma OAI.Brennan.measurable_rootJac line 57
  5. lemma OAI.Brennan.rootJac_reroot line 61
  6. def OAI.Brennan.rootWindow line 65
  7. def OAI.Brennan.windowTest line 67
  8. lemma OAI.Brennan.measurableSet_rootWindow line 69
  9. lemma OAI.Brennan.measurable_windowTest line 72
  10. lemma OAI.Brennan.averagedDensity_window line 75
  11. def OAI.Brennan.rootException line 88
  12. def OAI.Brennan.exceptionTest line 91
  13. lemma OAI.Brennan.measurableSet_rootException line 93
  14. lemma OAI.Brennan.measurable_exceptionTest line 99
  15. lemma OAI.Brennan.averagedDensity_exception line 102
  16. lemma OAI.Brennan.exceptionTest_integral_zero line 116
  17. lemma OAI.Brennan.averagedDensity_box line 127
  18. lemma OAI.Brennan.setLIntegral_mul_indicator_one line 140
  19. lemma OAI.Brennan.transport_box_averaged line 148
  20. lemma OAI.Brennan.expected_transport_box line 182
  21. lemma OAI.Brennan.transport_ratio_tendsto line 200
  22. lemma OAI.Brennan.transport_box_limit line 207
  23. lemma OAI.Brennan.rootJac_integral_lt_top line 237
  24. lemma OAI.Brennan.windowTest_le line 247
  25. lemma OAI.Brennan.windowTest_integral_lt_top line 250
  26. lemma OAI.Brennan.windowTest_mono line 254
  27. lemma OAI.Brennan.iSup_windowTest line 264
  28. lemma OAI.Brennan.rootJac_eq_window_exception line 283
  29. lemma OAI.Brennan.jacobian_positive_le_negative line 294