OAI/Combinatorics/Progressions/Estimates/NativeAbsorbedIntervals.lean

GitHub source file

34 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.Erdos3.NativeMultilinearIntervalFamily line 13
  2. def OAI.Erdos3.NativeMultilinearIntervalFamily.intervalSet line 50
  3. def OAI.Erdos3.NativeMultilinearIntervalFamily.delta line 53
  4. def OAI.Erdos3.NativeMultilinearIntervalFamily.sample line 55
  5. def OAI.Erdos3.NativeMultilinearIntervalFamily.rankProduct line 58
  6. def OAI.Erdos3.NativeMultilinearIntervalFamily.lowerProduct line 64
  7. def OAI.Erdos3.NativeMultilinearIntervalFamily.residual line 71
  8. theorem OAI.Erdos3.NativeMultilinearIntervalFamily.product_factorization line 74
  9. theorem OAI.Erdos3.NativeMultilinearIntervalFamily.mixed_correlation line 100
  10. theorem OAI.Erdos3.exists_native_multilinear_interval_family line 126
  11. structure OAI.Erdos3.NativeRetainedMultilinearIntervalFamily line 179
  12. theorem OAI.Erdos3.exists_native_retained_multilinear_interval_family line 185
  13. theorem OAI.Erdos3.NativeMultilinearIntervalFamily.intervalSet_nonempty line 242
  14. theorem OAI.Erdos3.NativeMultilinearIntervalFamily.sample_update line 246
  15. def OAI.Erdos3.NativeMultilinearIntervalFamily.lowerProductExpansion line 263
  16. theorem OAI.Erdos3.NativeMultilinearIntervalFamily.reduce_mixed line 294
  17. structure OAI.Erdos3.NativeReducedIntervalFamily line 334
  18. theorem OAI.Erdos3.NativeMultilinearIntervalFamily.reduce_with_budget line 362
  19. def OAI.Erdos3.NativeReducedIntervalFamily.localLower line 402
  20. def OAI.Erdos3.NativeReducedIntervalFamily.globalExpansion line 407
  21. def OAI.Erdos3.NativeReducedIntervalFamily.localExpansion line 412
  22. theorem OAI.Erdos3.NativeReducedIntervalFamily.rank_correlation line 426
  23. theorem OAI.Erdos3.NativeReducedIntervalFamily.interval_length_ratio line 433
  24. def OAI.Erdos3.NativeReducedIntervalFamily.retainedTriples line 437
  25. theorem OAI.Erdos3.NativeReducedIntervalFamily.retainedTriples_card line 440
  26. theorem OAI.Erdos3.NativeReducedIntervalFamily.retainedTriples_subset line 443
  27. theorem OAI.Erdos3.exists_native_reduced_interval_family line 456
  28. theorem OAI.Erdos3.NativeReducedIntervalFamily.exists_fixed_global_term line 497
  29. theorem OAI.Erdos3.NativeMultilinearIntervalFamily.rankProduct_norm line 549
  30. theorem OAI.Erdos3.NativeReducedIntervalFamily.localLower_norm line 566
  31. theorem OAI.Erdos3.NativeReducedIntervalFamily.scalar_norm line 570
  32. def OAI.Erdos3.IntervalGlobalReductionStatement line 588
  33. theorem OAI.Erdos3.exists_interval_global_reduction line 615
  34. theorem OAI.Erdos3.exists_absorbed_interval_family line 679