OAI/Probability/MemoryPrecision/JointL1.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MemoryPrecision.UniformSphere line 19

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

  2. def OAI.MemoryPrecision.GaussianRegularization line 32

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

  3. lemma OAI.MemoryPrecision.gaussianPDF_zero_sub_comm line 51
  4. lemma OAI.MemoryPrecision.GaussianRegularization_eq_toReal line 57
  5. lemma OAI.MemoryPrecision.GaussianRegularization_ae_eq_average line 76
  6. lemma OAI.MemoryPrecision.memLp_density_of_finite line 106
  7. lemma OAI.MemoryPrecision.density_ae_unique_real line 121
  8. def OAI.MemoryPrecision.JointL1Statement line 132

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

  9. theorem OAI.MemoryPrecision.joint_l1 line 158