OAI/Dynamics/EntropyCounterexample/SphereChartLimits.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Problem340.SphereChartLimits.north_eq line 13
  2. theorem OAI.Problem340.SphereChartLimits.chart_sphereOfComplex line 18
  3. theorem OAI.Problem340.SphereChartLimits.sphereToComplex_eq_chart line 32
  4. theorem OAI.Problem340.SphereChartLimits.sphereOfComplex_chart line 39
  5. theorem OAI.Problem340.SphereChartLimits.update_sphereOfComplex line 44
  6. theorem OAI.Problem340.SphereChartLimits.tendsto_sphereOfComplex_north line 54
  7. theorem OAI.Problem340.SphereChartLimits.tendsto_north_of_chart_norm line 66
  8. theorem OAI.Problem340.SphereChartLimits.tendsto_sphereOfComplex line 76
  9. theorem OAI.Problem340.SphereChartLimits.zero_eq_south line 81
  10. theorem OAI.Problem340.SphereChartLimits.tendsto_south_of_chart_zero line 86