OAI/Probability/GammaPassage/AnalyticCore.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.GammaFPP.Analytic.swapPlane line 15
  2. lemma OAI.GammaFPP.Analytic.swapPlane_zero line 18
  3. lemma OAI.GammaFPP.Analytic.swapPlane_one line 20
  4. lemma OAI.GammaFPP.Analytic.swapPlane_swap line 22
  5. theorem OAI.GammaFPP.Analytic.plane_coordinate_le_norm line 25
  6. theorem OAI.GammaFPP.Analytic.timeConstantNorm_lipschitz_bound line 28
  7. theorem OAI.GammaFPP.Analytic.timeConstantNorm_continuous line 54
  8. theorem OAI.GammaFPP.Analytic.norm_direction_pos line 67
  9. lemma OAI.GammaFPP.Analytic.norm_differentiable_smul line 75
  10. lemma OAI.GammaFPP.Analytic.convex_continuous_deriv line 86
  11. lemma OAI.GammaFPP.Analytic.convex_contDiff_one line 116
  12. lemma OAI.GammaFPP.Analytic.plane_direction_representation line 120
  13. lemma OAI.GammaFPP.Analytic.contDiff_direction line 126
  14. def OAI.GammaFPP.Analytic.sphereChart line 133
  15. def OAI.GammaFPP.Analytic.directionRatio line 135
  16. lemma OAI.GammaFPP.Analytic.sphereChart_coordinates line 137
  17. lemma OAI.GammaFPP.Analytic.sphereChart_ratio line 141
  18. lemma OAI.GammaFPP.Analytic.sphereChart_mem line 149
  19. lemma OAI.GammaFPP.Analytic.sphereChart_reconstruct line 160
  20. lemma OAI.GammaFPP.Analytic.sphereChart_contDiff line 183
  21. lemma OAI.GammaFPP.Analytic.sphereChart_regular line 188
  22. lemma OAI.GammaFPP.Analytic.sphere_horizontal_chart line 209
  23. theorem OAI.GammaFPP.Analytic.norm_ball_frontier line 222
  24. lemma OAI.GammaFPP.Analytic.chart_preimage_isometry line 239