OAI/Geometry/KahlerSplitting/PolydiskAxes.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.UnitPolydisk.discShift line 11
  2. lemma OAI.UnitPolydisk.denominator_ne_zero line 13
  3. lemma OAI.UnitPolydisk.normSq_difference line 22
  4. lemma OAI.UnitPolydisk.discShift_mem line 29
  5. lemma OAI.UnitPolydisk.discShift_zero line 41
  6. lemma OAI.UnitPolydisk.discShift_neg_self line 43
  7. lemma OAI.UnitPolydisk.discShift_inverse line 46
  8. lemma OAI.UnitPolydisk.differentiableOn_discShift line 57
  9. def OAI.UnitPolydisk.shift line 63
  10. lemma OAI.UnitPolydisk.norm_coord_lt_one line 65
  11. lemma OAI.UnitPolydisk.shift_mem line 68
  12. lemma OAI.UnitPolydisk.shift_zero line 73
  13. lemma OAI.UnitPolydisk.shift_inverse line 75
  14. lemma OAI.UnitPolydisk.differentiableOn_shift line 80
  15. theorem OAI.UniversalCoverSplitting.polydisk_axes line 100
  16. lemma OAI.UniversalCoverSplitting.IsBlockBox.unique_polydisk line 134
  17. def OAI.UniversalCoverSplitting.IsDiskHorizontal line 167
  18. def OAI.UniversalCoverSplitting.IsDiskVertical line 170
  19. def OAI.UniversalCoverSplitting.IsDiskTile line 173
  20. lemma OAI.UniversalCoverSplitting.IsDiskTile.horizontal line 177
  21. lemma OAI.UniversalCoverSplitting.IsDiskTile.vertical line 183
  22. lemma OAI.UniversalCoverSplitting.IsDiskTile.plaqueBox line 189
  23. lemma OAI.UniversalCoverSplitting.disk_fill line 196
  24. theorem OAI.UniversalCoverSplitting.holomorphic_grid line 210