OAI/Combinatorics/SumProduct/Alignment/RoughSampling01.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.RoughSamplingWeights.indices line 25
  2. lemma OAI.RoughSamplingWeights.mem_indices line 28
  3. lemma OAI.RoughSamplingWeights.count_error line 41
  4. lemma OAI.RoughSamplingWeights.indices_subset line 57
  5. lemma OAI.RoughSamplingWeights.ratio_error line 66
  6. theorem OAI.RoughSamplingWeights.subinterval_weight line 95
  7. lemma OAI.RoughSamplingWeights.product_error line 112
  8. def OAI.RoughSamplingWeights.boxWeight line 138
  9. theorem OAI.RoughSamplingWeights.box_weight_error line 143
  10. theorem OAI.RoughSamplingWeights.compare_box_weights line 161
  11. lemma OAI.RoughSamplingWeights.refined_card_le line 179
  12. theorem OAI.RoughSamplingWeights.refined_interval_weight line 198
  13. def OAI.RoughSamplingWeights.refinedBoxWeight line 225
  14. theorem OAI.RoughSamplingWeights.refined_box_weight_error line 232
  15. theorem OAI.RoughSamplingWeights.compare_refined_box_weights line 255
  16. theorem OAI.RoughSamplingWeights.total_weight_error line 274
  17. theorem OAI.RoughSamplingWeights.residue_parameter line 292
  18. theorem OAI.RoughSamplingWeights.residue_sample line 311