OAI/Analysis/StrictMeans/BoundaryEscape.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.StrictInverseFirstPower.dyadicHeight_rpow line 100
  2. lemma OAI.StrictInverseFirstPower.ae_eventually_dyadic_cover line 105
  3. lemma OAI.StrictInverseFirstPower.dyadic_band_after line 120
  4. def OAI.StrictInverseFirstPower.boundaryEscape line 135
  5. lemma OAI.StrictInverseFirstPower.boundaryBadScale_ae_eventually line 139
  6. theorem OAI.StrictInverseFirstPower.ae_omitted_boundary_escape line 146
  7. lemma OAI.StrictInverseFirstPower.image_target_separated_near_boundary line 179
  8. lemma OAI.StrictInverseFirstPower.image_target_boundary_escape line 212
  9. lemma OAI.StrictInverseFirstPower.ae_boundary_escape line 228
  10. lemma OAI.StrictInverseFirstPower.norm_image_at_infinity_in_strip line 236
  11. lemma OAI.StrictInverseFirstPower.translated_escape_at_infinity_in_strip line 249
  12. def OAI.StrictInverseFirstPower.potentialSuperlevel line 276
  13. lemma OAI.StrictInverseFirstPower.bounded_strip_superlevel line 279
  14. lemma OAI.StrictInverseFirstPower.compact_superlevels_of_boundary_escape line 301
  15. theorem OAI.StrictInverseFirstPower.ae_compact_positive_superlevels line 328
  16. theorem OAI.StrictInverseFirstPower.affine_law_ae_compact_superlevels line 335