OAI/Combinatorics/Progressions/Lattices/ResidueStrideRebase.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.residueTransitionNumerator_pos line 10
  2. theorem OAI.Erdos3.residueTransition_scale line 18
  3. theorem OAI.Erdos3.residueTransition_shift line 28
  4. theorem OAI.Erdos3.residueTransition_physical line 34
  5. theorem OAI.Erdos3.residueTransition_denominator_bound line 53
  6. def OAI.Erdos3.residueBoxStrideValue line 74
  7. theorem OAI.Erdos3.integerInterval_abs_sub_le line 78
  8. theorem OAI.Erdos3.residueBox_stride_bound line 87
  9. def OAI.Erdos3.residueStepMatrix line 113
  10. theorem OAI.Erdos3.integerAffineMap_residueStepMatrix line 116
  11. theorem OAI.Erdos3.commonStrideIndex_residue_affine line 121
  12. theorem OAI.Erdos3.residueBoxStride_expect line 138
  13. theorem OAI.Erdos3.RationalFilteredNilmanifold.Niltest.residueBoxStride_mean line 161
  14. theorem OAI.Erdos3.scalarAffinePolynomial_comp line 184
  15. theorem OAI.Erdos3.RationalFilteredNilmanifold.Niltest.scalarAffinePullback_comp_orbit line 201
  16. theorem OAI.Erdos3.RationalFilteredNilmanifold.Niltest.scalarAffinePullback_comp_orbit_of_eq line 214
  17. theorem OAI.Erdos3.RationalFilteredNilmanifold.Niltest.scalarAffinePullback_transition_orbit line 221
  18. theorem OAI.Erdos3.RationalFilteredNilmanifold.Niltest.scalarAffinePullback_transition_factorization line 231
  19. theorem OAI.Erdos3.residue_refinement_offset_identity line 263
  20. theorem OAI.Erdos3.commonStrideIndex_of_refinement line 270
  21. theorem OAI.Erdos3.residue_refinement_parameter_bounds line 279
  22. theorem OAI.Erdos3.RationalFilteredNilmanifold.Niltest.scalarAffinePullback_refinement_orbit line 316
  23. theorem OAI.Erdos3.integerAffinePolynomial_residue_scalar line 338
  24. theorem OAI.Erdos3.RationalFilteredNilmanifold.Niltest.residue_scalar_affine_orbit line 352
  25. theorem OAI.Erdos3.RationalFilteredNilmanifold.Niltest.residue_scalar_affine_symbol line 363
  26. theorem OAI.Erdos3.RationalFilteredNilmanifold.Niltest.scalarAffinePullback_residue_factorization line 391
  27. theorem OAI.Erdos3.physical_box_anchor_bounds line 430
  28. theorem OAI.Erdos3.anchored_residue_refinement_bounds line 454
  29. theorem OAI.Erdos3.RationalFilteredNilmanifold.Niltest.eval_commonStride_rebase line 506
  30. theorem OAI.Erdos3.RationalFilteredNilmanifold.Niltest.residueBoxStride_rebase line 523