OAI/Geometry/Cannon/Energy/RawFunction.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CannonApprox.rawFunction line 31
  2. def OAI.CannonApprox.Admissible line 34
  3. theorem OAI.CannonApprox.rawFunction_properties line 39
  4. def OAI.CannonApprox.initial line 48
  5. def OAI.CannonApprox.scalar line 51
  6. lemma OAI.CannonApprox.initial_properties line 54
  7. theorem OAI.CannonApprox.scalar_properties line 63
  8. theorem OAI.CannonApprox.scalar_level line 76
  9. theorem OAI.CannonApprox.exists_mesh line 86
  10. theorem OAI.CannonApprox.scalar_local_oscillation line 92
  11. abbrev OAI.CannonRectangle.Middle line 119
  12. def OAI.CannonRectangle.normalize line 121
  13. lemma OAI.CannonRectangle.continuous_normalize line 127
  14. lemma OAI.CannonRectangle.normalize_injective line 131
  15. def OAI.CannonRectangle.leftRight line 141
  16. def OAI.CannonRectangle.topBottom line 145
  17. lemma OAI.CannonRectangle.leftRight_nonempty line 149
  18. lemma OAI.CannonRectangle.leftRight_members_nonempty line 156
  19. lemma OAI.CannonRectangle.crossings_intersect line 161
  20. theorem OAI.CannonRectangle.exists_dual_weights line 187