OAI/Analysis/Steinitz/LiftedRearrangement.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

Lifted fiber rearrangement and overlap estimates.

  1. def OAI.VerticalRearrangement.shear line 16
  2. lemma OAI.VerticalRearrangement.shear_preserving line 24
  3. def OAI.VerticalRearrangement.liftFunction line 34
  4. lemma OAI.VerticalRearrangement.lift_measurable line 37
  5. lemma OAI.VerticalRearrangement.lift_strip line 47
  6. lemma OAI.VerticalRearrangement.lift_nonneg line 54
  7. lemma OAI.VerticalRearrangement.lift_square_eq line 59
  8. lemma OAI.VerticalRearrangement.lift_memLp line 70
  9. lemma OAI.VerticalRearrangement.lift_total_square line 78
  10. lemma OAI.VerticalRearrangement.lift_difference_eq line 92
  11. lemma OAI.VerticalRearrangement.lift_total_difference line 100
  12. lemma OAI.VerticalRearrangement.fiberStar_horizontal_difference line 120
  13. lemma OAI.VerticalRearrangement.lifted_star_supported line 155
  14. lemma OAI.VerticalRearrangement.fiberStar_total_height line 180
  15. lemma OAI.VerticalRearrangement.fiberStar_strip line 207
  16. lemma OAI.VerticalRearrangement.fiberStar_height_integrable line 225
  17. lemma OAI.VerticalRearrangement.fiberStar_total_height_lower line 240
  18. lemma OAI.VerticalRearrangement.fiberStar_total_real_height line 276
  19. lemma OAI.VerticalRearrangement.min_square_lower line 304
  20. lemma OAI.VerticalRearrangement.min_square_integrable line 312
  21. lemma OAI.VerticalRearrangement.min_square_integral_lower line 321
  22. lemma OAI.VerticalRearrangement.translate_pair_square line 337
  23. lemma OAI.VerticalRearrangement.translate_min_square_lower line 343
  24. lemma OAI.VerticalRearrangement.lift_min_square line 372
  25. lemma OAI.VerticalRearrangement.lift_height_lower line 379
  26. lemma OAI.ShiftedSections.lifted_test line 439