OAI/Probability/LatticeSurface/Moments/Averages.lean

GitHub source file

42 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MacroscopicAverages.coordinateBox line 1125
  2. def OAI.MacroscopicAverages.statistic line 1128
  3. def OAI.MacroscopicAverages.cell line 1139
  4. def OAI.MacroscopicAverages.cellSites line 1141
  5. def OAI.MacroscopicAverages.weight line 1144
  6. lemma OAI.MacroscopicAverages.cell_remainder line 1147
  7. lemma OAI.MacroscopicAverages.mem_cellSites line 1159
  8. lemma OAI.MacroscopicAverages.card_cellSites line 1170
  9. lemma OAI.MacroscopicAverages.cell_mem_square line 1173
  10. lemma OAI.MacroscopicAverages.sum_weight line 1183
  11. lemma OAI.MacroscopicAverages.sum_weight_abs line 1197
  12. lemma OAI.MacroscopicAverages.weight_bound line 1204
  13. lemma OAI.MacroscopicAverages.representative_close line 1219
  14. lemma OAI.MacroscopicAverages.representative_error line 1228
  15. lemma OAI.MacroscopicAverages.ediv_adj line 1251
  16. lemma OAI.MacroscopicAverages.adj_cell line 1261
  17. lemma OAI.MacroscopicAverages.connected_image_stutter line 1272
  18. lemma OAI.MacroscopicAverages.anchor_connected line 1300
  19. lemma OAI.MacroscopicAverages.pin_cell_not_ordinary line 1305
  20. lemma OAI.MacroscopicAverages.anchor_diameter line 1313
  21. lemma OAI.MacroscopicAverages.continuous_statistic line 1359
  22. lemma OAI.MacroscopicAverages.law_ae_body line 1364
  23. lemma OAI.MacroscopicAverages.deterministic_statistic line 1368
  24. lemma OAI.MacroscopicAverages.nonnegative_distance line 1387
  25. lemma OAI.MacroscopicAverages.mgf_transfer line 1395
  26. lemma OAI.MacroscopicAverages.mgf_bounded line 1414
  27. lemma OAI.MacroscopicAverages.finite_in_box line 1424
  28. lemma OAI.MacroscopicAverages.coarseFunctional_height line 1434
  29. lemma OAI.MacroscopicAverages.coarse_scale line 1448
  30. theorem OAI.MacroscopicAverages.nonnegative_moments line 1499
  31. def OAI.MacroscopicAverages.shift line 1616
  32. def OAI.MacroscopicAverages.shifted line 1618
  33. lemma OAI.MacroscopicAverages.mem_shifted line 1620
  34. def OAI.MacroscopicAverages.shiftIndex line 1629
  35. def OAI.MacroscopicAverages.shiftHeights line 1637
  36. lemma OAI.MacroscopicAverages.shiftHeights_apply line 1640
  37. lemma OAI.MacroscopicAverages.height_shift line 1644
  38. lemma OAI.MacroscopicAverages.shift_body line 1651
  39. lemma OAI.MacroscopicAverages.preserving_shift_law line 1662
  40. lemma OAI.MacroscopicAverages.latticeDist_shift line 1670
  41. lemma OAI.MacroscopicAverages.shifted_disjoint line 1675
  42. theorem OAI.MacroscopicAverages.zero_pinned_exponential_moments line 1688