OAI/Probability/MemoryPrecision/WeightedImage.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.MemoryPrecision.space_finiteDimensional line 19

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

  2. def OAI.MemoryPrecision.WeightedBlock line 25

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

  3. lemma OAI.MemoryPrecision.measurable_weightedBlock line 45
  4. lemma OAI.MemoryPrecision.weightedBlock_le_one line 53
  5. lemma OAI.MemoryPrecision.weighted_image_finite line 65
  6. lemma OAI.MemoryPrecision.weighted_image_ball line 71
  7. lemma OAI.MemoryPrecision.projectionLaw_lintegral line 79
  8. lemma OAI.MemoryPrecision.weightedBlock_mass_identity line 89