OAI/Probability/FirstPassage/Target.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.PlanarFPP.Plane line 14

    Also declared: ComparatorChallenges/GammaPassage.lean:43 (same declaration text), ComparatorChallenges/PlanarFirstPassage.lean:44 (same declaration text).

  2. def OAI.PlanarFPP.latticeFloor line 16

    Also declared: ComparatorChallenges/GammaPassage.lean:45 (same declaration text), ComparatorChallenges/PlanarFirstPassage.lean:46 (same declaration text).

  3. def OAI.PlanarFPP.passageTime line 18

    Also declared: ComparatorChallenges/GammaPassage.lean:47 (same declaration text), ComparatorChallenges/PlanarFirstPassage.lean:48 (same declaration text).

  4. structure OAI.PlanarFPP.TimeConstantNorm line 21

    Also declared: ComparatorChallenges/GammaPassage.lean:50 (same declaration text), ComparatorChallenges/PlanarFirstPassage.lean:51 (same declaration text).

  5. structure OAI.PlanarFPP.ExponentialEnvironment line 27

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

  6. def OAI.PlanarFPP.IsTimeConstant line 34

    Also declared: ComparatorChallenges/GammaPassage.lean:56 (same declaration text), ComparatorChallenges/PlanarFirstPassage.lean:64 (same declaration text).

  7. def OAI.PlanarFPP.DifferentiableAwayFromOrigin line 40

    Also declared: ComparatorChallenges/GammaPassage.lean:62 (same declaration text), ComparatorChallenges/PlanarFirstPassage.lean:70 (same declaration text).

  8. def OAI.PlanarFPP.UniqueNormalizedSupports line 43

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

  9. def OAI.PlanarFPP.C1UnitSphere line 47

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

  10. def OAI.PlanarFPP.MainDifferentiabilityTarget line 54