OAI/Probability/StrongRayleigh/FiniteFieldTilt.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Problem336AdditiveD139.finiteFieldWeight line 15
  2. def OAI.Problem336AdditiveD139.finiteFieldMean line 19
  3. theorem OAI.Problem336AdditiveD139.measurable_boolReal line 24
  4. theorem OAI.Problem336AdditiveD139.measurable_finiteFieldWeight line 27
  5. theorem OAI.Problem336AdditiveD139.measurable_finiteFieldWeight_joint line 34
  6. theorem OAI.Problem336AdditiveD139.finiteFieldWeight_pos line 42
  7. theorem OAI.Problem336AdditiveD139.integrable_finiteFieldWeight line 45
  8. theorem OAI.Problem336AdditiveD139.finiteFieldWeight_integral_pos line 58
  9. theorem OAI.Problem336AdditiveD139.finiteField_boolReal_bounds line 70
  10. theorem OAI.Problem336AdditiveD139.integrable_finiteFieldMean_numerator line 74
  11. theorem OAI.Problem336AdditiveD139.finiteFieldMean_mem_unitInterval line 89
  12. theorem OAI.Problem336AdditiveD139.measurable_finiteFieldMean line 106
  13. theorem OAI.Problem336AdditiveD139.finiteFieldWeight_translate line 116
  14. theorem OAI.Problem336AdditiveD139.integral_leftTranslate_of_invariant line 128
  15. theorem OAI.Problem336AdditiveD139.finiteFieldMean_translate line 137