OAI/Combinatorics/Progressions/Lattices/UniformExternalMarkedAffineSliceFreezingDictionary.lean

GitHub source file

34 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.ResidueBoxSlice.affineIntegerPoint line 13
  2. theorem OAI.Erdos3.ResidueBoxSlice.affineIntegerPoint_residue line 17
  3. theorem OAI.Erdos3.ResidueBoxSlice.exists_constant_freezing_pair line 26
  4. def OAI.Erdos3.affineParentIntegerPoint line 64
  5. theorem OAI.Erdos3.exists_long_affine_residue_cell_frozen_score line 68
  6. theorem OAI.Erdos3.exists_long_affine_residue_cell_frozen_score_with_cell line 161
  7. theorem OAI.Erdos3.ResidueBoxSlice.composeSlice_integerPoint line 261
  8. theorem OAI.Erdos3.ResidueBoxSlice.composeSlice_integerPoint_affine line 267
  9. theorem OAI.Erdos3.ResidueBoxSlice.composeSlice_integerPoints_eq_affine_image line 277
  10. theorem OAI.Erdos3.ResidueBoxSlice.composeSlice_integerPoints_eq_image line 286
  11. theorem OAI.Erdos3.ResidueBoxSlice.composeSlice_integerPoints_subset line 295
  12. theorem OAI.Erdos3.ResidueBoxSlice.expect_composeSlice_integerPoints line 303
  13. theorem OAI.Erdos3.ResidueBoxSlice.composeSlice_isDenseCommonStrideBox line 314
  14. theorem OAI.Erdos3.ResidueBoxSlice.composeSlice_isDenseCommonStrideBox_of_fraction line 330
  15. theorem OAI.Erdos3.ResidueBoxSlice.refined_stride_le_twice_exp_cost line 342
  16. theorem OAI.Erdos3.ResidueBoxSlice.refined_stride_le_exp_cost line 353
  17. def OAI.Erdos3.RationalFilteredNilmanifold.Niltest.markedFrozenValue line 375
  18. def OAI.Erdos3.RationalFilteredNilmanifold.MarkedAffineSliceFreezing line 389
  19. theorem OAI.Erdos3.RationalFilteredNilmanifold.BoundedCellMarkedPolynomialFreezing.affine_slice line 457
  20. theorem OAI.Erdos3.RationalFilteredNilmanifold.exists_uniform_marked_affine_slice_freezing line 504
  21. def OAI.Erdos3.RationalFilteredNilmanifold.ExternalMarkedAffineSliceFreezing line 549
  22. theorem OAI.Erdos3.RationalFilteredNilmanifold.BoundedCellMarkedPolynomialFreezing.external_affine_slice line 633
  23. theorem OAI.Erdos3.RationalFilteredNilmanifold.exists_uniform_external_marked_affine_slice_freezing line 700
  24. structure OAI.Erdos3.RationalFilteredNilmanifold.ExternalMarkedAffineSliceFreezing.Dictionary line 747
  25. theorem OAI.Erdos3.RationalFilteredNilmanifold.ExternalMarkedAffineSliceFreezing.exists_dictionary line 844
  26. def OAI.Erdos3.RationalFilteredNilmanifold.ExternalMarkedAffineSliceFreezing.Dictionary.mono_slow line 891
  27. theorem OAI.Erdos3.RationalFilteredNilmanifold.ExternalMarkedAffineSliceFreezing.Dictionary.mono_slow_grid line 922
  28. theorem OAI.Erdos3.RationalFilteredNilmanifold.ExternalMarkedAffineSliceFreezing.Dictionary.mono_slow_Q line 925
  29. theorem OAI.Erdos3.RationalFilteredNilmanifold.ExternalMarkedAffineSliceFreezing.Dictionary.mono_slow_modulus line 928
  30. theorem OAI.Erdos3.RationalFilteredNilmanifold.ExternalMarkedAffineSliceFreezing.Dictionary.mono_slow_denominator line 931
  31. theorem OAI.Erdos3.RationalFilteredNilmanifold.ExternalMarkedAffineSliceFreezing.Dictionary.mono_slow_rightCount line 934
  32. theorem OAI.Erdos3.RationalFilteredNilmanifold.ExternalMarkedAffineSliceFreezing.Dictionary.mono_slow_left line 937
  33. theorem OAI.Erdos3.RationalFilteredNilmanifold.ExternalMarkedAffineSliceFreezing.Dictionary.mono_slow_right line 940
  34. theorem OAI.Erdos3.RationalFilteredNilmanifold.exists_uniform_external_marked_affine_slice_freezing_dictionary line 954