OAI/Geometry/Cannon/Modulus/Clip.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.CannonAnnular.weighted_open_interval_cover line 27
  2. theorem OAI.CannonAnnular.interval_energy_cover line 54
  3. theorem OAI.CannonAnnular.overlap_energy line 65
  4. theorem OAI.CannonAnnular.annular_energy_transfer line 99
  5. theorem OAI.CannonAnnular.finite_charge_cover line 128
  6. theorem OAI.CannonAnnular.interval_cover_of_charging line 152
  7. theorem OAI.CannonAnnular.annular_net_charge line 174
  8. theorem OAI.CannonAnnular.charged_center_in_annulus line 208
  9. theorem OAI.CannonCapacity.bin_interval_detection line 230
  10. theorem OAI.CannonCapacity.mixed_capacity_of_detection line 269
  11. theorem OAI.CannonCapacity.weighted_separated_subset line 345
  12. def OAI.CannonCapacity.clip line 402
  13. lemma OAI.CannonCapacity.clip_mono line 404
  14. lemma OAI.CannonCapacity.mem_clipped_iff line 408
  15. lemma OAI.CannonCapacity.clip_difference line 426
  16. theorem OAI.CannonCapacity.clipped_bin_detection line 442
  17. theorem OAI.CannonCapacity.separated_capacity_of_detection line 479
  18. theorem OAI.CannonAnnular.radial_subinterval line 526
  19. theorem OAI.CannonAnnular.radial_subpath line 568
  20. theorem OAI.CannonAnnular.continuum_neighborhood_path line 590
  21. theorem OAI.CannonAnnular.annular_path_near_continuum line 605