OAI/Probability/Renewal/Centered.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.HoneycombLocal.natMean line 10
  2. def OAI.HoneycombLocal.natVariance line 12
  3. def OAI.HoneycombLocal.natThird line 14
  4. lemma OAI.HoneycombLocal.natMean_nonneg line 16
  5. lemma OAI.HoneycombLocal.natVariance_nonneg line 17
  6. lemma OAI.HoneycombLocal.natThird_nonneg line 18
  7. lemma OAI.HoneycombLocal.nat_memLp line 20
  8. lemma OAI.HoneycombLocal.natVariance_eq_sub line 26
  9. lemma OAI.HoneycombLocal.natVariance_le_second line 34
  10. lemma OAI.HoneycombLocal.integrable_pair_square line 40
  11. lemma OAI.HoneycombLocal.two_copy_variance line 50
  12. lemma OAI.HoneycombLocal.rectangle_variance_bound line 65
  13. lemma OAI.HoneycombLocal.natThird_le_raw line 81
  14. def OAI.HoneycombLocal.centeredMeasure line 101
  15. instance OAI.HoneycombLocal.centeredMeasure_probability line 103
  16. lemma OAI.HoneycombLocal.centered_integral line 107
  17. lemma OAI.HoneycombLocal.centered_mean line 111
  18. lemma OAI.HoneycombLocal.centered_variance line 117
  19. lemma OAI.HoneycombLocal.centered_third line 120
  20. lemma OAI.HoneycombLocal.centered_memLp line 123
  21. lemma OAI.HoneycombLocal.centered_char line 129