OAI/Analysis/SymmetricDomains/OneParameterDifferentiableZero.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Release061.finite_measure_holomorphic_average_derivative line 37
  2. theorem OAI.Release061.finite_measure_holomorphic_average_analytic line 71
  3. def OAI.Release061.Biholomorph.shortTimeAverage line 91
  4. theorem OAI.Release061.Biholomorph.oneParameter_evaluation_continuous line 96
  5. theorem OAI.Release061.Biholomorph.shortTimeAverage_derivative line 100
  6. theorem OAI.Release061.Biholomorph.shortTimeAverage_analytic line 121
  7. theorem OAI.Release061.Biholomorph.shortTimeAverage_linear_tendsto line 127
  8. theorem OAI.Release061.Biholomorph.shortTimeAverage_orbit_derivative line 139
  9. theorem OAI.Release061.Biholomorph.exists_regular_shortTimeAverage line 166
  10. theorem OAI.Release061.Biholomorph.oneParameter_hasDerivAt_of_regular_average line 187
  11. theorem OAI.Release061.Biholomorph.oneParameter_differentiableAt_zero line 209