OAI/Analysis/SymmetricDomains/DivisibleBochnerCoordinate.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Release061.compact_holomorphic_average_derivative line 37
  2. theorem OAI.Release061.compact_holomorphic_average_analytic line 72
  3. def OAI.Release061.Biholomorph.bochnerIntegrand line 91
  4. theorem OAI.Release061.Biholomorph.bochnerIntegrand_continuous line 97
  5. theorem OAI.Release061.Biholomorph.bochnerIntegrand_hasFDerivAt line 111
  6. theorem OAI.Release061.Biholomorph.bochnerIntegrand_analytic line 119
  7. theorem OAI.Release061.Biholomorph.bochnerIntegrand_derivative_continuous line 125
  8. theorem OAI.Release061.Biholomorph.bochnerIntegrand_uniform_bound line 137
  9. def OAI.Release061.Biholomorph.bochnerMap line 157
  10. theorem OAI.Release061.Biholomorph.bochnerMap_analytic line 160
  11. theorem OAI.Release061.Biholomorph.bochnerMap_center line 169
  12. theorem OAI.Release061.Biholomorph.bochnerIntegrand_center_fderiv line 180
  13. theorem OAI.Release061.Biholomorph.bochnerMap_center_derivative line 187
  14. theorem OAI.Release061.Biholomorph.bochnerIntegrand_mul line 202
  15. theorem OAI.Release061.Biholomorph.bochnerMap_equivariant line 216
  16. theorem OAI.Release061.Biholomorph.exists_bochner_coordinate line 229
  17. theorem OAI.Release061.Biholomorph.divisible_bochner_coordinate line 259