OAI/Combinatorics/Progressions/Estimates/ProductiveFrozenLocalMajorFamily.lean

GitHub source file

51 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.Erdos3.LocalMajorSliceTest line 15
  2. def OAI.Erdos3.LocalMajorSliceTest.weight line 27
  3. theorem OAI.Erdos3.LocalMajorSliceTest.weight_norm line 29
  4. def OAI.Erdos3.LocalMajorSliceTest.full line 35
  5. theorem OAI.Erdos3.exists_productive_localMajorSlice_coordinate_family line 50
  6. def OAI.Erdos3.OrdinaryPolynomialPhase.zeroLocalMajorSlice line 101
  7. def OAI.Erdos3.frozenLongExtension line 129
  8. theorem OAI.Erdos3.frozenLongExtension_long line 132
  9. theorem OAI.Erdos3.frozenLongExtension_injective line 137
  10. def OAI.Erdos3.ResidueBoxSlice.freezeShort line 147
  11. theorem OAI.Erdos3.ResidueBoxSlice.freezeShort_integerPoints line 161
  12. theorem OAI.Erdos3.ResidueBoxSlice.expect_freezeShort line 194
  13. theorem OAI.Erdos3.ResidueBoxSlice.freezeShort_commonStrideIndex line 204
  14. theorem OAI.Erdos3.ResidueBoxSlice.freezeShort_dense line 213
  15. def OAI.Erdos3.longCoordinateProjection line 251
  16. def OAI.Erdos3.RationalFilteredNilmanifold.Niltest.liftLong line 263
  17. theorem OAI.Erdos3.RationalFilteredNilmanifold.Niltest.liftLong_normBound line 268
  18. theorem OAI.Erdos3.RationalFilteredNilmanifold.Niltest.liftLong_complexityLE line 272
  19. theorem OAI.Erdos3.RationalFilteredNilmanifold.Niltest.eval_liftLong line 276
  20. def OAI.Erdos3.LocalMajorSliceTest.freezeShort line 289
  21. theorem OAI.Erdos3.LocalMajorSliceTest.freezeShort_weight line 302
  22. theorem OAI.Erdos3.LocalMajorSliceTest.expect_freezeShort line 313
  23. def OAI.Erdos3.LocalMajorSliceTest.default line 350
  24. theorem OAI.Erdos3.LocalMajorSliceTest.nonempty line 365
  25. def OAI.Erdos3.LocalMajorSliceTest.mono line 390
  26. theorem OAI.Erdos3.LocalMajorSliceTest.mono_weight line 401
  27. structure OAI.Erdos3.UniversalLocalMajorSliceTest line 416
  28. def OAI.Erdos3.UniversalLocalMajorSliceTest.nativeModel line 433
  29. theorem OAI.Erdos3.UniversalLocalMajorSliceTest.value_eq_native_eval line 437
  30. def OAI.Erdos3.UniversalLocalMajorSliceTest.weight line 441
  31. theorem OAI.Erdos3.UniversalLocalMajorSliceTest.weight_eq_native_eval line 446
  32. theorem OAI.Erdos3.UniversalLocalMajorSliceTest.weight_norm line 452
  33. def OAI.Erdos3.UniversalLocalMajorSliceTest.ofLocalMajorSliceTest line 457
  34. theorem OAI.Erdos3.UniversalLocalMajorSliceTest.ofLocalMajorSliceTest_weight line 478
  35. theorem OAI.Erdos3.UniversalLocalMajorSliceTest.ofLocalMajorSliceTest_slice line 486
  36. def OAI.Erdos3.UniversalLocalMajorSliceTest.default line 494
  37. theorem OAI.Erdos3.UniversalLocalMajorSliceTest.nonempty line 502
  38. def OAI.Erdos3.UniversalLocalMajorSliceTest.ofNative line 524
  39. def OAI.Erdos3.UniversalLocalMajorSliceTest.toLocalMajorSliceTest line 536
  40. theorem OAI.Erdos3.UniversalLocalMajorSliceTest.toLocalMajorSliceTest_slice line 547
  41. theorem OAI.Erdos3.UniversalLocalMajorSliceTest.toLocalMajorSliceTest_weight line 551
  42. def OAI.Erdos3.UniversalLocalMajorSliceTest.freezeShort line 558
  43. theorem OAI.Erdos3.UniversalLocalMajorSliceTest.freezeShort_stride line 566
  44. theorem OAI.Erdos3.UniversalLocalMajorSliceTest.freezeShort_slice line 573
  45. theorem OAI.Erdos3.UniversalLocalMajorSliceTest.freezeShort_weight line 581
  46. theorem OAI.Erdos3.UniversalLocalMajorSliceTest.expect_freezeShort line 591
  47. theorem OAI.Erdos3.UniversalLocalMajorSliceTest.expect_subtypeSites_freezeShort line 612
  48. def OAI.Erdos3.frozenShortStarts line 637
  49. theorem OAI.Erdos3.frozenShortStarts_inside line 640
  50. theorem OAI.Erdos3.frozenLongExtension_shortStarts line 649
  51. theorem OAI.Erdos3.exists_productive_frozen_localMajor_family line 661