OAI/Analysis/SymmetricDomains/DiscRelationCompactLocal.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Release061.coordinateEnergy line 15
  2. def OAI.Release061.peakLinear line 17
  3. theorem OAI.Release061.peakLinear_re line 20
  4. theorem OAI.Release061.coordinateEnergy_nonneg line 31
  5. theorem OAI.Release061.sq_norm_le_coordinateEnergy line 34
  6. theorem OAI.Release061.coordinateEnergy_continuous line 42
  7. theorem OAI.Release061.peakLinear_analytic line 46
  8. theorem OAI.Release061.peak_norm_identity line 52
  9. theorem OAI.Release061.polynomial_compact_peak_energy line 62
  10. theorem OAI.Release061.polynomial_compact_peak line 93
  11. theorem OAI.Release061.HolomorphicOnSubset.entire_scalar_comp line 105
  12. def OAI.Release061.actionBiholomorph line 114
  13. theorem OAI.Release061.cocompact_bounded_affine_smooth line 122
  14. def OAI.Release061.DiscRelation line 192
  15. theorem OAI.Release061.discRelation_symm line 196
  16. theorem OAI.Release061.discRelation_refl line 201
  17. theorem OAI.Release061.discRelation_dist_le line 206
  18. theorem OAI.Release061.bounded_disc_relation_compact_local line 236