OAI/Probability/MemoryPrecision/KernelEllipsoid.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.MemoryPrecision.Kernel.chord_real_coefficient line 19
  2. lemma OAI.MemoryPrecision.Kernel.chord_half_sphere_bound line 30
  3. lemma OAI.MemoryPrecision.Kernel.chord_half_ambient_bound line 53
  4. def OAI.MemoryPrecision.Kernel.BlockCount line 84

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

  5. def OAI.MemoryPrecision.Kernel.SourceEllipsoidStatement line 85

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

  6. theorem OAI.MemoryPrecision.Kernel.source_ellipsoid_success line 117