OAI/Probability/MemoryPrecision/RadialMixture.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MemoryPrecision.UnitBallVolume line 18

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

  2. def OAI.MemoryPrecision.CoordinateUnit line 31

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

  3. lemma OAI.MemoryPrecision.gaussianVariance_nonneg line 37

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

  4. def OAI.MemoryPrecision.GaussianKernel line 39

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

  5. def OAI.MemoryPrecision.RadialMixture line 46

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

  6. def OAI.MemoryPrecision.GaussianAmplitude line 49
  7. lemma OAI.MemoryPrecision.coordinateUnit_norm line 52
  8. lemma OAI.MemoryPrecision.gaussianKernel_radial line 65
  9. lemma OAI.MemoryPrecision.gaussianKernel_nonneg line 78
  10. lemma OAI.MemoryPrecision.gaussianKernel_continuous line 82
  11. lemma OAI.MemoryPrecision.unitBallVolume_pos line 88
  12. lemma OAI.MemoryPrecision.volume_ball_eq line 92
  13. lemma OAI.MemoryPrecision.gaussianKernel_radial_line line 102
  14. lemma OAI.MemoryPrecision.gaussianRadial_deriv line 108
  15. lemma OAI.MemoryPrecision.gaussianRadial_tendsto line 118
  16. lemma OAI.MemoryPrecision.gaussianRadial_tail line 127
  17. lemma OAI.MemoryPrecision.gaussianKernel_integral line 137
  18. lemma OAI.MemoryPrecision.gaussianKernel_lintegral line 148
  19. lemma OAI.MemoryPrecision.gaussianRadial_integrable line 155
  20. lemma OAI.MemoryPrecision.gaussianRadial_ltail line 163
  21. lemma OAI.MemoryPrecision.gaussianKernel_ball_mixture line 172
  22. lemma OAI.MemoryPrecision.radialMixture_nonneg line 190
  23. lemma OAI.MemoryPrecision.radialMixture_measurable line 196
  24. lemma OAI.MemoryPrecision.radialMixture_lintegral line 202
  25. lemma OAI.MemoryPrecision.radialMixture_integral line 236
  26. lemma OAI.MemoryPrecision.radialMixture_tail line 243