OAI/Probability/StrongRayleigh/GeneratingSlice.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Problem336AdditiveD139.GeneratingSlice.countExcept line 18
  2. def OAI.Problem336AdditiveD139.GeneratingSlice.weight line 22
  3. def OAI.Problem336AdditiveD139.GeneratingSlice.slice line 25
  4. lemma OAI.Problem336AdditiveD139.GeneratingSlice.weight_nonneg line 30
  5. lemma OAI.Problem336AdditiveD139.GeneratingSlice.countExcept_cast line 33
  6. lemma OAI.Problem336AdditiveD139.GeneratingSlice.countExcept_add_bit line 41
  7. lemma OAI.Problem336AdditiveD139.GeneratingSlice.monomial_except line 47
  8. lemma OAI.Problem336AdditiveD139.GeneratingSlice.monomial_slice line 56
  9. lemma OAI.Problem336AdditiveD139.GeneratingSlice.slice_eval line 72
  10. lemma OAI.Problem336AdditiveD139.GeneratingSlice.slice_eval_one line 81
  11. lemma OAI.Problem336AdditiveD139.GeneratingSlice.slice_aeval line 85
  12. lemma OAI.Problem336AdditiveD139.GeneratingSlice.slice_derivative_eval_one line 94
  13. lemma OAI.Problem336AdditiveD139.GeneratingSlice.slice_coeff_nonneg line 103
  14. lemma OAI.Problem336AdditiveD139.GeneratingSlice.slice_eval_one_add line 114
  15. lemma OAI.Problem336AdditiveD139.GeneratingSlice.slice_generating_identity line 122
  16. lemma OAI.Problem336AdditiveD139.GeneratingSlice.slice_stable line 134
  17. lemma OAI.Problem336AdditiveD139.GeneratingSlice.slice_true_eval_one line 144
  18. lemma OAI.Problem336AdditiveD139.GeneratingSlice.slice_derivative_add line 151
  19. lemma OAI.Problem336AdditiveD139.GeneratingSlice.slice_true_derivative_add line 159
  20. lemma OAI.Problem336AdditiveD139.GeneratingSlice.slice_total_derivative_add line 169
  21. lemma OAI.Problem336AdditiveD139.GeneratingSlice.slice_sum_eq_partition line 179
  22. lemma OAI.Problem336AdditiveD139.GeneratingSlice.tiltMean_eq_slice line 188
  23. lemma OAI.Problem336AdditiveD139.GeneratingSlice.sum_tiltMean_eq_slice line 197
  24. lemma OAI.Problem336AdditiveD139.GeneratingSlice.sum_tiltSecondMoment_eq_slice line 210
  25. theorem OAI.Problem336AdditiveD139.GeneratingSlice.covariance_row_eq_slice line 223
  26. theorem OAI.Problem336AdditiveD139.GeneratingSlice.covariance_row_nonneg_of_slice_bound line 238