OAI/Probability/GaussianReplacement/FiberModel.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CurrentProjection.fiberObservationLaw line 16

    Also declared: ComparatorChallenges/GaussianReplacement.lean:350 (same declaration text).

  2. lemma OAI.CurrentProjection.measurable_fiberObservationMap line 20
  3. instance OAI.CurrentProjection.uniformSphere_finite line 24

    Also declared: ComparatorChallenges/GaussianReplacement.lean:354 (same declaration text).

  4. instance OAI.CurrentProjection.fiberObservationLaw_finite line 30

    Also declared: ComparatorChallenges/GaussianReplacement.lean:360 (same declaration text).

  5. lemma OAI.CurrentProjection.sphere_standardBorel line 34

    Also declared: ComparatorChallenges/GaussianReplacement.lean:364 (same declaration text).

  6. def OAI.CurrentProjection.sphericalFiberKernel line 37

    Also declared: ComparatorChallenges/GaussianReplacement.lean:367 (same declaration text).

  7. instance OAI.CurrentProjection.sphericalFiberKernel_markov line 43

    Also declared: ComparatorChallenges/GaussianReplacement.lean:373 (same declaration text).

  8. def OAI.CurrentProjection.fiberTwoPointLeft line 49

    Also declared: ComparatorChallenges/GaussianReplacement.lean:378 (same declaration text).

  9. def OAI.CurrentProjection.perpendicularRow line 57

    Also declared: ComparatorChallenges/GaussianReplacement.lean:385 (same declaration text).

  10. lemma OAI.CurrentProjection.measurable_perpendicularRow line 62
  11. def OAI.CurrentProjection.perpendicularRowsKernel line 67

    Also declared: ComparatorChallenges/GaussianReplacement.lean:390 (same declaration text).

  12. def OAI.CurrentProjection.fiberTwoPointConstant line 72

    Also declared: ComparatorChallenges/GaussianReplacement.lean:394 (same declaration text).

  13. def OAI.CurrentProjection.fiberDistanceWeight line 79

    Also declared: ComparatorChallenges/GaussianReplacement.lean:401 (same declaration text).

  14. def OAI.CurrentProjection.fiberTwoPointRight line 83

    Also declared: ComparatorChallenges/GaussianReplacement.lean:404 (same declaration text).

  15. def OAI.CurrentProjection.FiberTwoPointMain line 93

    Also declared: ComparatorChallenges/GaussianReplacement.lean:425 (same declaration text).