OAI/Combinatorics/Progressions/Estimates/PeelingDecomposition.lean

GitHub source file

37 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.abs_expect_le_of_bound line 10
  2. theorem OAI.Erdos3.abs_expect_sub_expect_le line 19
  3. theorem OAI.Erdos3.abs_weighted_expect_sub_le line 25
  4. def OAI.Erdos3.Peeling.remainder line 49
  5. def OAI.Erdos3.Peeling.slice line 51
  6. def OAI.Erdos3.Peeling.positiveSupport line 53
  7. theorem OAI.Erdos3.Peeling.remainder_nonneg line 56
  8. theorem OAI.Erdos3.Peeling.remainder_le line 61
  9. theorem OAI.Erdos3.Peeling.remainder_supported line 66
  10. theorem OAI.Erdos3.Peeling.remainder_add_slice line 72
  11. theorem OAI.Erdos3.Peeling.sum_slice line 76
  12. theorem OAI.Erdos3.Peeling.sum_remainder_add line 79
  13. theorem OAI.Erdos3.Peeling.expect_eq_total_div line 85
  14. theorem OAI.Erdos3.Peeling.expect_remainder line 91
  15. theorem OAI.Erdos3.Peeling.positiveSupport_remainder_subset line 102
  16. theorem OAI.Erdos3.Peeling.positiveSupport_remainder_card_lt line 110
  17. theorem OAI.Erdos3.Peeling.expect_slice_scale line 135
  18. def OAI.Erdos3.CellRefinement.bilinearIntegral line 150
  19. theorem OAI.Erdos3.CellRefinement.bilinearIntegral_swap line 153
  20. theorem OAI.Erdos3.CellRefinement.bilinearIntegral_le line 163
  21. theorem OAI.Erdos3.CellRefinement.bilinearIntegral_peeling line 181
  22. theorem OAI.Erdos3.CellRefinement.bilinearIntegral_slice_scale line 194
  23. theorem OAI.Erdos3.LocalConvolution.convolution_nonneg line 219
  24. theorem OAI.Erdos3.LocalConvolution.convolution_le_of_mass line 224
  25. theorem OAI.Erdos3.LocalConvolution.normalized_mass_one line 236
  26. inductive OAI.Erdos3.Peeling.Chain line 256
  27. theorem OAI.Erdos3.Peeling.Chain.bounds line 272
  28. theorem OAI.Erdos3.Peeling.Chain.supported line 282
  29. theorem OAI.Erdos3.Peeling.Chain.admissible_mem line 291
  30. theorem OAI.Erdos3.Peeling.Chain.final_eq_foldl line 301
  31. theorem OAI.Erdos3.Peeling.Chain.length_le_support line 307
  32. theorem OAI.Erdos3.Peeling.exists_terminal_chain line 328
  33. theorem OAI.Erdos3.Peeling.exists_bounded_terminal_chain line 355
  34. def OAI.Erdos3.Peeling.removedWeight line 375
  35. theorem OAI.Erdos3.Peeling.Chain.decomposition line 380
  36. theorem OAI.Erdos3.Peeling.removedWeight_nonneg line 391
  37. theorem OAI.Erdos3.Peeling.Chain.sum_mul_decomposition line 400