OAI/Combinatorics/SumProduct/Alignment/FinitePiece01.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ConvexDiscrepancy.average line 27
  2. lemma OAI.ConvexDiscrepancy.weight_error line 29
  3. lemma OAI.ConvexDiscrepancy.positive_piece line 45
  4. theorem OAI.ConvexDiscrepancy.select_piece line 81
  5. theorem OAI.ConvexDiscrepancy.select_after_freezing line 95
  6. def OAI.FinitePieceAverages.fiber line 125
  7. def OAI.FinitePieceAverages.weight line 127
  8. def OAI.FinitePieceAverages.mean line 129
  9. lemma OAI.FinitePieceAverages.weight_nonneg line 133
  10. lemma OAI.FinitePieceAverages.sum_weights line 136
  11. lemma OAI.FinitePieceAverages.decomposition line 144
  12. lemma OAI.FinitePieceAverages.norm_mean_le line 163
  13. lemma OAI.FinitePieceAverages.mean_difference line 179
  14. lemma OAI.FinitePieceAverages.mean_error line 185
  15. theorem OAI.FinitePieceAverages.select line 192
  16. def OAI.RoughSamplingWeights.boxIndices line 226
  17. lemma OAI.RoughSamplingWeights.mem_boxIndices line 229
  18. lemma OAI.RoughSamplingWeights.card_boxIndices line 233
  19. def OAI.RoughSamplingWeights.refinedSet line 239
  20. lemma OAI.RoughSamplingWeights.affine_injective line 244
  21. lemma OAI.RoughSamplingWeights.card_refinedSet line 251
  22. lemma OAI.RoughSamplingWeights.mem_refinedSet line 258
  23. lemma OAI.RoughSamplingWeights.refined_subset line 284
  24. lemma OAI.RoughSamplingWeights.refined_mass line 296
  25. lemma OAI.RoughSamplingWeights.box_nonempty line 305