OAI/Combinatorics/Progressions/Estimates/PivotStageBoundary.lean

GitHub source file

37 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.expect_independent_product line 12
  2. theorem OAI.Erdos3.expect_common_shift_product line 17
  3. theorem OAI.Erdos3.expect_pivot_change line 26
  4. theorem OAI.Erdos3.pivot_even_moment line 39
  5. theorem OAI.Erdos3.twoSlopeMap_bijective line 67
  6. theorem OAI.Erdos3.expect_two_slopes line 97
  7. theorem OAI.Erdos3.expect_two_slope_product line 108
  8. theorem OAI.Erdos3.FiniteProbabilityWeights.mean_pow_two_pow_le line 124
  9. theorem OAI.Erdos3.weighted_dyadic_holder line 137
  10. theorem OAI.Erdos3.expect_single_slope line 197
  11. theorem OAI.Erdos3.product_near_one line 206
  12. theorem OAI.Erdos3.twoSlope_average_near_one line 220
  13. def OAI.Erdos3.pivotCellForm line 238
  14. def OAI.Erdos3.pivotGridFactor line 242
  15. def OAI.Erdos3.pivotRootFactor line 246
  16. def OAI.Erdos3.pivotKernelFactor line 250
  17. def OAI.Erdos3.pivotStageIntegrand line 256
  18. def OAI.Erdos3.pivotStageCount line 262
  19. theorem OAI.Erdos3.pivotGridFactor_root line 267
  20. theorem OAI.Erdos3.pivotRootFactor_nonneg line 271
  21. theorem OAI.Erdos3.pivotRootFactor_le_exp line 276
  22. theorem OAI.Erdos3.pivot_weighted_dyadic_step line 297
  23. def OAI.Erdos3.PivotCompatible line 326
  24. theorem OAI.Erdos3.PivotCompatible.cons_erase line 334
  25. theorem OAI.Erdos3.pivotCompatible_zero line 351
  26. theorem OAI.Erdos3.pivotCellForm_cons line 369
  27. theorem OAI.Erdos3.pivotGridFactor_cons line 377
  28. theorem OAI.Erdos3.pivotKernelFactor_cons line 387
  29. theorem OAI.Erdos3.pivotStageIntegrand_cons line 397
  30. theorem OAI.Erdos3.pivotStageIntegrand_peel line 406
  31. theorem OAI.Erdos3.pivotStageCount_cons line 417
  32. theorem OAI.Erdos3.pivotStageCount_cons_nonneg line 444
  33. theorem OAI.Erdos3.pivotStageCount_step line 454
  34. theorem OAI.Erdos3.pivotGridFactor_zero line 495
  35. theorem OAI.Erdos3.pivotKernelFactor_zero line 502
  36. theorem OAI.Erdos3.pivotStageCount_zero line 509
  37. theorem OAI.Erdos3.pivotStageCount_terminal line 518