OAI/Geometry/Anticanonical/CompactSections.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Equicontinuity and finite-dimensionality of holomorphic sections on compact manifolds.

  1. theorem OAI.CompactSections.equicontinuousAt_of_ball_bound line 16
  2. theorem OAI.CompactSections.equicontinuousAt_clm_apply line 46
  3. theorem OAI.CompactSections.equicontinuousAt_of_local_holomorphic_bound line 95
  4. abbrev OAI.CompactSections.HolSections line 146
  5. def OAI.CompactSections.sectionProfile line 149
  6. theorem OAI.CompactSections.sectionProfile_injective line 169
  7. theorem OAI.CompactSections.sectionProfiles_equicontinuous line 182
  8. theorem OAI.CompactSections.finiteDimensional_of_compact_cover line 221
  9. theorem OAI.CompactSections.finiteDimensional_holomorphic_sections line 282