OAI/Combinatorics/SumProduct/Alignment/WeightedBoxes01.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ConstructedWordPlan.GlobalWordPlan.jump line 20
  2. lemma OAI.ConstructedWordPlan.GlobalWordPlan.exactRun_snd line 27
  3. def OAI.WeightedBoxes.StrictDegree line 50
  4. def OAI.WeightedBoxes.coeffNorm line 54
  5. lemma OAI.WeightedBoxes.coeffNorm_nonneg line 57
  6. lemma OAI.WeightedBoxes.monomial_bound line 60
  7. lemma OAI.WeightedBoxes.eval_bound line 72
  8. theorem OAI.WeightedBoxes.uniform_displacement_bound line 90
  9. def OAI.WeightedBoxes.LowerDependency line 103
  10. theorem OAI.WeightedBoxes.measurePreserving_triangular line 108
  11. lemma OAI.WeightedBoxes.polynomial_lowerDependency line 171
  12. theorem OAI.WeightedBoxes.measurePreserving_polynomialShear line 184
  13. def OAI.WeightedBoxes.rect line 200
  14. lemma OAI.WeightedBoxes.mem_rect_iff line 203
  15. lemma OAI.WeightedBoxes.measurableSet_rect line 207
  16. lemma OAI.WeightedBoxes.rect_volume line 209
  17. lemma OAI.WeightedBoxes.rect_finite line 217
  18. lemma OAI.WeightedBoxes.rect_volume_pos line 220
  19. lemma OAI.WeightedBoxes.rect_smul_volume line 225
  20. lemma OAI.WeightedBoxes.symmDiff_bound line 233
  21. lemma OAI.WeightedBoxes.preimage_symmDiff_bound line 249
  22. def OAI.WeightedBoxes.weightedBox line 266
  23. def OAI.WeightedBoxes.boundaryError line 269
  24. lemma OAI.WeightedBoxes.boundaryError_nonneg line 273
  25. theorem OAI.WeightedBoxes.boundaryError_bound line 277
  26. theorem OAI.WeightedBoxes.boundaryError_tendsto line 317
  27. def OAI.WeightedBoxes.normalizedRestriction line 333
  28. lemma OAI.WeightedBoxes.normalizedRestriction_real line 336
  29. theorem OAI.WeightedBoxes.normalizedRestriction_variation line 345
  30. theorem OAI.WeightedBoxes.weightedBoxLaw_invariance line 375