OAI/Analysis/Steinitz/Rearrangement.lean

GitHub source file

79 declarations, 0 contain sorry, 0 declared as axioms

Vertical Steiner rearrangement and shifted section geometry.

  1. def OAI.ShiftedSections.sectionDomain line 14
  2. lemma OAI.ShiftedSections.section_open line 17
  3. lemma OAI.ShiftedSections.section_mix line 32
  4. lemma OAI.ShiftedSections.section_convex line 54
  5. lemma OAI.ShiftedSections.line_segment_mem line 61
  6. lemma OAI.ShiftedSections.section_symmetric line 69
  7. lemma OAI.ShiftedSections.shifted_step line 77
  8. lemma OAI.ShiftedSections.zero_mem_of_symmetric_convex line 90
  9. lemma OAI.VerticalRearrangement.layer_pair line 111
  10. def OAI.VerticalRearrangement.layer line 129
  11. lemma OAI.VerticalRearrangement.layer_measurable line 132
  12. lemma OAI.VerticalRearrangement.layer_pair_sets line 137
  13. lemma OAI.VerticalRearrangement.measure_inter_eq_min_of_nested line 160
  14. def OAI.VerticalRearrangement.centered line 166
  15. lemma OAI.VerticalRearrangement.centered_measurable line 169
  16. lemma OAI.VerticalRearrangement.measure_centered line 172
  17. lemma OAI.VerticalRearrangement.centered_mono line 180
  18. lemma OAI.VerticalRearrangement.centered_inter line 184
  19. def OAI.VerticalRearrangement.heightMeasure line 190
  20. instance OAI.VerticalRearrangement.(instance at line 193) line 193
  21. lemma OAI.VerticalRearrangement.integral_abs_symmetric line 197
  22. lemma OAI.VerticalRearrangement.heightMeasure_centered line 219
  23. lemma OAI.VerticalRearrangement.heightMeasure_centered_inter line 236
  24. lemma OAI.VerticalRearrangement.measure_family_measurable line 246
  25. def OAI.VerticalRearrangement.rearranged line 256
  26. lemma OAI.VerticalRearrangement.centered_family_measurable line 259
  27. lemma OAI.VerticalRearrangement.rearranged_measurable line 265
  28. lemma OAI.VerticalRearrangement.rearranged_pair line 269
  29. lemma OAI.VerticalRearrangement.rearranged_inner_ge line 279
  30. lemma OAI.VerticalRearrangement.rearranged_square line 292
  31. lemma OAI.VerticalRearrangement.rearranged_height line 300
  32. lemma OAI.VerticalRearrangement.prod_family_measurable line 319
  33. lemma OAI.VerticalRearrangement.rearranged_height_pair line 325
  34. lemma OAI.VerticalRearrangement.rearranged_eq_zero_of_bound line 339
  35. def OAI.VerticalRearrangement.superlevel line 352
  36. lemma OAI.VerticalRearrangement.superlevel_measurable line 354
  37. lemma OAI.VerticalRearrangement.layer_superlevel line 360
  38. lemma OAI.VerticalRearrangement.superlevel_nested line 369
  39. lemma OAI.VerticalRearrangement.layer_superlevel_prod line 380
  40. lemma OAI.VerticalRearrangement.function_rearranged_height line 391
  41. lemma OAI.VerticalRearrangement.ae_finite_of_square line 411
  42. lemma OAI.VerticalRearrangement.toReal_memLp line 418
  43. lemma OAI.VerticalRearrangement.integral_toReal_square line 424
  44. lemma OAI.VerticalRearrangement.lintegral_mul_ne_top_of_squares line 430
  45. lemma OAI.VerticalRearrangement.integral_toReal_mul line 441
  46. lemma OAI.VerticalRearrangement.integral_sub_sq line 452
  47. lemma OAI.VerticalRearrangement.rearranged_real_memLp line 476
  48. lemma OAI.VerticalRearrangement.rearranged_real_square line 481
  49. lemma OAI.VerticalRearrangement.rearranged_real_inner line 489
  50. lemma OAI.VerticalRearrangement.rearranged_real_difference line 502
  51. def OAI.VerticalRearrangement.fiberStar line 526
  52. lemma OAI.VerticalRearrangement.fiberLength_measurable line 529
  53. lemma OAI.VerticalRearrangement.fiberStar_measurable line 536
  54. lemma OAI.VerticalRearrangement.superlevel_measure_ne_top_of_strip line 547
  55. lemma OAI.VerticalRearrangement.fiberStar_square line 560
  56. lemma OAI.VerticalRearrangement.fiberStar_total_square line 570
  57. lemma OAI.VerticalRearrangement.fiberStar_toReal_memLp line 579
  58. lemma OAI.VerticalRearrangement.fiberStar_total_real_square line 586
  59. lemma OAI.VerticalRearrangement.fiberStar_eq_zero_of_measure_le line 597
  60. lemma OAI.VerticalRearrangement.ofReal_square_integral_ne_top line 609
  61. lemma OAI.VerticalRearrangement.fiberStar_difference line 614
  62. lemma OAI.VerticalRearrangement.fiberStar_memLp line 633
  63. lemma OAI.VerticalRearrangement.fiberStar_total_difference line 639
  64. lemma OAI.ShiftedSections.line_interval_mem line 672
  65. lemma OAI.ShiftedSections.section_mono line 682
  66. lemma OAI.ShiftedSections.section_of_fiber_pair line 689
  67. lemma OAI.ShiftedSections.fiber_measure_le_of_not_section line 700
  68. lemma OAI.ShiftedSections.section_bounded line 714
  69. lemma OAI.ShiftedSections.fiberStar_supported line 734
  70. lemma OAI.EuclideanSteinitz.convex_supporting_line line 760
  71. def OAI.ShiftedSections.sectionNorm line 801
  72. def OAI.ShiftedSections.sectionRate line 807
  73. def OAI.ShiftedSections.activeHeights line 811
  74. lemma OAI.ShiftedSections.activeHeights_convex line 814
  75. lemma OAI.ShiftedSections.sectionNorm_pos line 820
  76. lemma OAI.ShiftedSections.sectionNorm_le_one line 829
  77. lemma OAI.ShiftedSections.sectionRate_nonneg line 833
  78. lemma OAI.ShiftedSections.sectionRate_monotone line 839
  79. lemma OAI.ShiftedSections.sectionRate_convex line 847