OAI/Analysis/PathSelection/ParameterIntegrals.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Analytic parameter integrals over compact sets and circles.

  1. lemma OAI.PathSelection.ParameterPreparation.differentiableAt_integral_compact line 16
  2. theorem OAI.PathSelection.ParameterPreparation.differentiableOn_circleIntegral line 55
  3. theorem OAI.PathSelection.ParameterPreparation.analyticOnNhd_circleIntegral_one_parameter line 97
  4. theorem OAI.PathSelection.ParameterPreparation.hasFPowerSeriesOnBall_integral line 106
  5. lemma OAI.PathSelection.ParameterPreparation.changeOrigin_uniform_majorant line 149
  6. theorem OAI.PathSelection.ParameterPreparation.analyticAt_integral_shift_piece line 170
  7. lemma OAI.PathSelection.ParameterPreparation.analyticAt_integral_finite_cover line 228
  8. theorem OAI.PathSelection.ParameterPreparation.analyticOnNhd_integral_compact line 268
  9. theorem OAI.PathSelection.ParameterPreparation.analyticOnNhd_circleIntegral line 336