OAI/Probability/SwitchChain/SliceMoments.lean

GitHub source file

40 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Problem315.SliceMoments.average line 13
  2. def OAI.Problem315.SliceMoments.coord line 16
  3. theorem OAI.Problem315.SliceMoments.average_containment line 18
  4. theorem OAI.Problem315.SliceMoments.average_containment_all line 37
  5. theorem OAI.Problem315.SliceMoments.average_coord line 54
  6. theorem OAI.Problem315.SliceMoments.average_coord_mul line 61
  7. theorem OAI.Problem315.SliceMoments.coord_sq line 75
  8. theorem OAI.Problem315.SliceMoments.average_add line 79
  9. theorem OAI.Problem315.SliceMoments.average_mul_left line 85
  10. theorem OAI.Problem315.SliceMoments.average_sum line 91
  11. theorem OAI.Problem315.SliceMoments.average_linear line 98
  12. theorem OAI.Problem315.SliceMoments.average_linear_sq line 113
  13. theorem OAI.Problem315.SliceMoments.average_linear_zero_sum line 174
  14. theorem OAI.Problem315.SliceMoments.average_linear_sq_zero_sum line 179
  15. theorem OAI.Problem315.SliceMoments.average_congr line 197
  16. theorem OAI.Problem315.SliceMoments.average_const line 205
  17. theorem OAI.Problem315.SliceMoments.average_sub line 213
  18. def OAI.Problem315.SliceMoments.equalIndicator line 218
  19. theorem OAI.Problem315.SliceMoments.equalIndicator_eq line 221
  20. theorem OAI.Problem315.SliceMoments.equalIndicator_sq line 225
  21. def OAI.Problem315.SliceMoments.equalMean line 230
  22. theorem OAI.Problem315.SliceMoments.average_equalIndicator line 235
  23. def OAI.Problem315.SliceMoments.centeredEqual line 257
  24. theorem OAI.Problem315.SliceMoments.average_centeredEqual line 260
  25. theorem OAI.Problem315.SliceMoments.average_centeredEqual_sq line 268
  26. theorem OAI.Problem315.SliceMoments.average_map_embedding line 284
  27. theorem OAI.Problem315.SliceMoments.coord_map_embedding line 290
  28. theorem OAI.Problem315.SliceMoments.equalIndicator_map_embedding line 295
  29. theorem OAI.Problem315.SliceMoments.equalMean_map_embedding line 301
  30. theorem OAI.Problem315.SliceMoments.centeredEqual_map_embedding line 307
  31. theorem OAI.Problem315.SliceMoments.average_permute line 312
  32. theorem OAI.Problem315.SliceMoments.centeredEqual_covariance_map line 317
  33. theorem OAI.Problem315.SliceMoments.average_sq_eq_zero_iff line 326
  34. theorem OAI.Problem315.SliceMoments.centeredEqual_eq_zero_of_degenerate_mean line 348
  35. theorem OAI.Problem315.SliceMoments.centeredEqual_eq_zero_of_boundary line 356
  36. abbrev OAI.Problem315.SliceMoments.State line 384
  37. theorem OAI.Problem315.SliceMoments.average_eq_fintype_sum line 387
  38. def OAI.Problem315.SliceMoments.vector line 392
  39. theorem OAI.Problem315.SliceMoments.vector_norm_sq line 395
  40. theorem OAI.Problem315.SliceMoments.vector_inner line 404