OAI/Probability/FirstPassage/SphereCharts.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PlanarFPP.HasC1CurveChart line 9

    Also declared: ComparatorChallenges/PlanarFirstPassage.lean:84 (same declaration text).

  2. lemma OAI.PlanarFPP.contDiff_direction line 16
  3. def OAI.PlanarFPP.sphereChart line 23
  4. def OAI.PlanarFPP.directionRatio line 25
  5. lemma OAI.PlanarFPP.sphereChart_coordinates line 27
  6. lemma OAI.PlanarFPP.sphereChart_ratio line 31
  7. lemma OAI.PlanarFPP.sphereChart_mem line 39
  8. lemma OAI.PlanarFPP.sphereChart_reconstruct line 50
  9. lemma OAI.PlanarFPP.sphereChart_contDiff line 73
  10. lemma OAI.PlanarFPP.sphereChart_regular line 78
  11. lemma OAI.PlanarFPP.sphere_horizontal_chart line 99