OAI/Analysis/SymmetricDomains/AnalyticNhdDifferentiableAffine.lean

GitHub source file

35 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Release061.gaussian_peak_square_bound line 11
  2. abbrev OAI.Release061.RadiusCircle line 37
  3. instance OAI.Release061.radiusCircleCompact line 39
  4. def OAI.Release061.circleExtend line 42
  5. theorem OAI.Release061.circleExtend_on line 46
  6. theorem OAI.Release061.continuousOn_circleExtend line 50
  7. def OAI.Release061.circleIntegralLM line 55
  8. def OAI.Release061.circleIntegralCLM line 69
  9. theorem OAI.Release061.circleIntegralCLM_apply line 76
  10. def OAI.Release061.cauchyFunctional line 80
  11. theorem OAI.Release061.cauchyFunctional_apply line 84
  12. def OAI.Release061.curryCLM line 89
  13. theorem OAI.Release061.continuousMap_ringInverse_apply line 96
  14. def OAI.Release061.joinTorus line 106
  15. def OAI.Release061.iteratedCauchyFunctional line 116
  16. theorem OAI.Release061.iteratedCauchyFunctional_zero line 125
  17. theorem OAI.Release061.iteratedCauchyFunctional_succ line 129
  18. lemma OAI.Release061.fin_cons_continuous line 135
  19. lemma OAI.Release061.fin_cons_differentiable line 145
  20. lemma OAI.Release061.fin_cons_mem_closedBall line 157
  21. theorem OAI.Release061.iteratedCauchy_formula line 168
  22. def OAI.Release061.torusVal line 223
  23. lemma OAI.Release061.torusVal_mem_closedBall line 227
  24. def OAI.Release061.torusBoundary line 233
  25. def OAI.Release061.torusCoordinate line 238
  26. def OAI.Release061.torusResolvent line 241
  27. lemma OAI.Release061.torus_difference_ne_zero line 245
  28. lemma OAI.Release061.torusResolvent_apply line 256
  29. lemma OAI.Release061.analyticAt_torusResolvent line 261
  30. def OAI.Release061.cauchyTransform line 277
  31. lemma OAI.Release061.analyticAt_cauchyTransform line 281
  32. lemma OAI.Release061.cauchyTransform_eq line 289
  33. theorem OAI.Release061.analyticAt_of_differentiableOn_closedBall line 298
  34. theorem OAI.Release061.analyticOnNhd_of_differentiableOn_finite line 305
  35. theorem OAI.Release061.analyticOnNhd_of_differentiableOn_affine line 323