OAI/Analysis/IntegralMeans/BoundaryEscape.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.Brennan.halfPlane_ball_subset line 24
  2. lemma OAI.Brennan.omitted_quarter_bound line 33
  3. lemma OAI.Brennan.class_omitted_cell_bound line 46
  4. def OAI.Brennan.closedPositiveSuperlevel line 81
  5. lemma OAI.Brennan.interior_positive_superlevel_height line 84
  6. lemma OAI.Brennan.positive_superlevel_compact line 118
  7. def OAI.Brennan.realCell line 162
  8. lemma OAI.Brennan.realCell_disjoint line 164
  9. lemma OAI.Brennan.measure_realCell line 176
  10. lemma OAI.Brennan.mem_realCell_floor line 182
  11. lemma OAI.Brennan.realCell_length_bound line 187
  12. lemma OAI.Brennan.cell_target_cover_bound line 192
  13. lemma OAI.Brennan.summable_geometric_ofReal line 223
  14. lemma OAI.Brennan.ae_eventually_outside_geometric_covers line 234
  15. def OAI.Brennan.dyadicHeight line 243
  16. lemma OAI.Brennan.dyadicHeight_pos line 245
  17. lemma OAI.Brennan.dyadicHeight_le_one line 247
  18. lemma OAI.Brennan.exists_dyadic_slab line 249
  19. lemma OAI.Brennan.dyadicHeight_antitone line 258
  20. lemma OAI.Brennan.small_height_dyadic_slab line 262
  21. lemma OAI.Brennan.slab_power_bound line 269
  22. def OAI.Brennan.omittedTargets line 276
  23. lemma OAI.Brennan.omitted_targets_cover line 280
  24. lemma OAI.Brennan.ae_omitted_positive_superlevel_height line 338
  25. lemma OAI.Brennan.ae_positive_superlevel_height line 363
  26. lemma OAI.Brennan.ae_positive_superlevel_compact line 399
  27. lemma OAI.Brennan.class_ae_compact_superlevels line 417