OAI/Combinatorics/Progressions/Estimates/CenteredFiniteSliceResidualEnvelope.lean

GitHub source file

36 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.normalizedSliceTest line 12
  2. theorem OAI.Erdos3.normalizedSliceTest_norm_le line 16
  3. theorem OAI.Erdos3.normalizedSliceTest_mean line 26
  4. def OAI.Erdos3.sampledTestLinearMap line 53
  5. def OAI.Erdos3.sampledSingleTestSeminorm line 60
  6. theorem OAI.Erdos3.sampledSingleTestSeminorm_le line 64
  7. def OAI.Erdos3.sampledTestSeminorm line 75
  8. theorem OAI.Erdos3.sampledSingleTestSeminorm_bddAbove line 86
  9. theorem OAI.Erdos3.sampledTestSeminorm_apply line 96
  10. theorem OAI.Erdos3.sampledTestSeminorm_le_siteLaw line 106
  11. def OAI.Erdos3.sampledSliceSeminorm line 129
  12. theorem OAI.Erdos3.sampledSliceSeminorm_apply line 134
  13. theorem OAI.Erdos3.sampledSliceSeminorm_le_siteLaw line 147
  14. def OAI.Erdos3.centeredFiniteMarginal line 173
  15. theorem OAI.Erdos3.centeredFiniteMarginal_mean line 180
  16. theorem OAI.Erdos3.centeredFiniteMarginal_sampledSliceSeminorm line 187
  17. theorem OAI.Erdos3.exists_center_of_sampledSliceSeminorm line 195
  18. theorem OAI.Erdos3.integral_norm_le_centeredFiniteMarginal line 214
  19. theorem OAI.Erdos3.integral_selected_slice_residual_le line 241
  20. theorem OAI.Erdos3.productive_mass_mul_le_sampledSliceSeminorm line 282
  21. theorem OAI.Erdos3.exists_sampled_slice_model line 336
  22. theorem OAI.Erdos3.sampledSliceSeminorm_congr_values line 370
  23. theorem OAI.Erdos3.sampledSliceSeminorm_finiteSiteExtension line 384
  24. theorem OAI.Erdos3.exists_nearly_maximizing_sampled_slice_tests line 406
  25. theorem OAI.Erdos3.centeredFinite_excessMass_integrable line 445
  26. theorem OAI.Erdos3.centeredFiniteMarginal_excessMass_le line 452
  27. theorem OAI.Erdos3.centeredFiniteMarginal_excessMass_le_of_ae line 474
  28. theorem OAI.Erdos3.centeredFiniteMarginal_excessMass_le_of_uniform line 482
  29. theorem OAI.Erdos3.centeredFinite_siteLaw_weight_measurable line 493
  30. theorem OAI.Erdos3.centeredFiniteMarginal_siteLaw line 506
  31. theorem OAI.Erdos3.centeredFiniteMarginal_siteLaw_excessMass_le line 528
  32. theorem OAI.Erdos3.centeredFiniteMarginal_siteLaw_mass_le line 535
  33. def OAI.Erdos3.centeredFiniteSliceResidualEnvelope line 559
  34. theorem OAI.Erdos3.centeredFiniteSliceResidualEnvelope_nonneg line 566
  35. theorem OAI.Erdos3.centeredFiniteSliceResidualEnvelope_dominates line 573
  36. theorem OAI.Erdos3.centeredFiniteSliceResidualEnvelope_joint line 596