OAI/Combinatorics/Progressions/Estimates/RepresentativeWindowPatch.lean

GitHub source file

39 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.regularizedTentPartition line 16
  2. theorem OAI.Erdos3.regularizedTentPartition_range line 19
  3. theorem OAI.Erdos3.regularizedTentPartition_sum line 26
  4. theorem OAI.Erdos3.regularizedTentPartition_zero line 36
  5. theorem OAI.Erdos3.regularizedTentPartition_lipschitz line 40
  6. def OAI.Erdos3.intervalSiteCount line 71
  7. def OAI.Erdos3.intervalSiteCenter line 73
  8. def OAI.Erdos3.intervalSiteWeight line 76
  9. theorem OAI.Erdos3.intervalSiteCenter_bound line 79
  10. theorem OAI.Erdos3.intervalSiteWeight_range line 83
  11. theorem OAI.Erdos3.intervalSiteWeight_sum line 88
  12. theorem OAI.Erdos3.intervalSiteWeight_near line 97
  13. theorem OAI.Erdos3.intervalSiteWeight_lipschitz line 102
  14. theorem OAI.Erdos3.regularizedTentPartition_sum_le line 124
  15. theorem OAI.Erdos3.regularizedTentPartition_approx line 130
  16. theorem OAI.Erdos3.FiniteProbabilityWeights.norm_complexMean_cutoff_error line 177
  17. theorem OAI.Erdos3.FiniteProbabilityWeights.cutoff_bias_lower line 187
  18. theorem OAI.Erdos3.FiniteProbabilityWeights.mean_one_sub line 197
  19. theorem OAI.Erdos3.FiniteProbabilityWeights.pi_cutoff_loss line 201
  20. theorem OAI.Erdos3.bounded_weight_cutoff_lipschitz line 224
  21. theorem OAI.Erdos3.FiniteProbabilityWeights.norm_complexMean_weighted_cutoff_error line 245
  22. theorem OAI.Erdos3.FiniteProbabilityWeights.weighted_cutoff_bias_lower line 263
  23. theorem OAI.Erdos3.FiniteProbabilityWeights.pi_bad_event_mass_le line 288
  24. theorem OAI.Erdos3.FiniteProbabilityWeights.pi_remove_bad_event_error line 319
  25. theorem OAI.Erdos3.FiniteProbabilityWeights.pi_lowWeightFibers_mass line 330
  26. theorem OAI.Erdos3.FiniteProbabilityWeights.pi_remove_lowWeightFibers_error line 343
  27. structure OAI.Erdos3.RepresentativeWindow line 368
  28. def OAI.Erdos3.representativeWindowCount line 378
  29. theorem OAI.Erdos3.representativeWindowCount_pos line 380
  30. def OAI.Erdos3.representativeWindowPartitionLip line 384
  31. def OAI.Erdos3.localizedRepresentativeWindow line 387
  32. theorem OAI.Erdos3.localizedRepresentativeWindow_sum line 419
  33. theorem OAI.Erdos3.exists_localizedRepresentativeWindow_score line 427
  34. def OAI.Erdos3.RepresentativeWindow.kernel line 460
  35. def OAI.Erdos3.RepresentativeWindow.patch line 478
  36. theorem OAI.Erdos3.RepresentativeWindow.patch_term line 485
  37. theorem OAI.Erdos3.RepresentativeWindow.patch_value line 495
  38. theorem OAI.Erdos3.RepresentativeWindow.patch_contributing_lift line 512
  39. theorem OAI.Erdos3.RepresentativeWindow.patch_lip line 522