OAI/Probability/MemoryPrecision/CoefficientStep.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.MemoryPrecision.Sphere line 19

    Also declared: ComparatorChallenges/MemoryPrecision.lean:314 (same declaration text).

  2. def OAI.MemoryPrecision.SpherePrior line 20

    Also declared: ComparatorChallenges/MemoryPrecision.lean:316 (same declaration text).

  3. def OAI.MemoryPrecision.SphereBallBound line 23

    Also declared: ComparatorChallenges/MemoryPrecision.lean:319 (same declaration text).

  4. def OAI.MemoryPrecision.SphereBlock line 27

    Also declared: ComparatorChallenges/MemoryPrecision.lean:349 (same declaration text).

  5. def OAI.MemoryPrecision.CoefficientStepStatement line 31

    Also declared: ComparatorChallenges/MemoryPrecision.lean:692 (same declaration text).

  6. theorem OAI.MemoryPrecision.coefficient_step line 44