OAI/Probability/MemoryPrecision/MeasurableTests.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.MemoryPrecision.original_le_completion line 21
  2. lemma OAI.MemoryPrecision.trim_completion line 25
  3. lemma OAI.MemoryPrecision.lintegral_completion line 32
  4. lemma OAI.MemoryPrecision.eLpNorm_completion line 41
  5. lemma OAI.MemoryPrecision.density_test_bound line 51
  6. lemma OAI.MemoryPrecision.density_set_bound line 90
  7. lemma OAI.MemoryPrecision.withDensity_completion_apply line 100
  8. def OAI.MemoryPrecision.MeasurableTestStatement line 109

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

  9. theorem OAI.MemoryPrecision.measurable_test line 139