OAI/Analysis/IntegralMeans/TransportBoxes.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Brennan.displacementWindow line 24
  2. def OAI.Brennan.transportWindow line 27
  3. lemma OAI.Brennan.measurableSet_transportWindow line 31
  4. lemma OAI.Brennan.displacementWindow_affine line 50
  5. lemma OAI.Brennan.transportWindow_root line 59
  6. lemma OAI.Brennan.displacementWindow_mono line 76
  7. lemma OAI.Brennan.exists_displacementWindow line 83
  8. lemma OAI.Brennan.transportWindow_mono line 91
  9. lemma OAI.Brennan.iUnion_transportWindow line 97
  10. def OAI.Brennan.transportSlice line 108
  11. lemma OAI.Brennan.transportSlice_iff line 113
  12. lemma OAI.Brennan.measurableSet_transportSlice line 117
  13. def OAI.Brennan.transportBox line 126
  14. lemma OAI.Brennan.measurableSet_transportBox line 128
  15. lemma OAI.Brennan.pair_mem_enlargedBox line 133
  16. lemma OAI.Brennan.fiberSum_mul_indicator line 145
  17. lemma OAI.Brennan.transport_box line 156
  18. lemma OAI.Brennan.measurableSet_exceptionSlice line 188
  19. lemma OAI.Brennan.exceptional_transport_zero line 196