OAI/Geometry/Cannon/Topology/PlaneBox.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CannonPlane.realProd_to_complex_norm line 36
  2. lemma OAI.CannonPlane.realProd_to_complex_opNorm line 44
  3. def OAI.CannonPlane.planeBox line 47
  4. lemma OAI.CannonPlane.planeBox_compact line 49
  5. lemma OAI.CannonPlane.closedBall_subset_planeBox line 52
  6. lemma OAI.CannonPlane.coordinate_energy_bound line 59
  7. theorem OAI.CannonPlane.plane_continuum_capacity line 86
  8. lemma OAI.CannonPlane.smoothTransition_deriv_zero line 130
  9. lemma OAI.CannonPlane.smoothTransition_deriv_bound line 142
  10. def OAI.CannonPlane.annularCutoff line 154
  11. lemma OAI.CannonPlane.annularCutoff_inner line 157
  12. lemma OAI.CannonPlane.annularCutoff_outer line 164
  13. lemma OAI.CannonPlane.annularCutoff_contDiff line 171
  14. lemma OAI.CannonPlane.annularCutoff_fderiv_zero_inner line 185
  15. lemma OAI.CannonPlane.annularCutoff_fderiv_zero_outer line 192
  16. lemma OAI.CannonPlane.annularCutoff_fderiv_bound line 199