OAI/Combinatorics/Progressions/Linear/NativeRankRelationExistence.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.rank_pair_density_loss line 11
  2. structure OAI.Erdos3.NativeWeightedRankIntervals line 42
  3. structure OAI.Erdos3.NativeAnchoredRankFibers line 82
  4. theorem OAI.Erdos3.NativeWeightedRankIntervals.exists_anchored_fibers line 99
  5. def OAI.Erdos3.NativeAnchoredRankFibers.fiber line 130
  6. theorem OAI.Erdos3.NativeAnchoredRankFibers.fiber_nonempty line 133
  7. theorem OAI.Erdos3.NativeAnchoredRankFibers.fiber_parameter line 139
  8. theorem OAI.Erdos3.NativeAnchoredRankFibers.fiber_anchor line 142
  9. theorem OAI.Erdos3.NativeAnchoredRankFibers.fiber_branch line 145
  10. theorem OAI.Erdos3.NativeAnchoredRankFibers.fiber_shift_injective line 148
  11. structure OAI.Erdos3.NativeRankInterval line 167
  12. def OAI.Erdos3.NativeRankInterval.mono line 192
  13. theorem OAI.Erdos3.exists_native_weighted_rank_intervals line 212
  14. theorem OAI.Erdos3.NativeAnchoredRankFibers.exists_interval_pairs line 282
  15. theorem OAI.Erdos3.NativeRankInterval.select_lower_term line 363
  16. theorem OAI.Erdos3.exists_rank_interval_raised_lower_term line 377
  17. structure OAI.Erdos3.NativeRankRelation line 411
  18. def OAI.Erdos3.NativeRankRelation.mono line 422
  19. theorem OAI.Erdos3.NativeRankInterval.monomialScale_modulus_bound line 446
  20. theorem OAI.Erdos3.NativeRankInterval.norm_bound_on_modulus line 462
  21. theorem OAI.Erdos3.NativeRankInterval.length_lower_bound line 488
  22. theorem OAI.Erdos3.NativeRankInterval.length_exp_lower_bound line 492
  23. theorem OAI.Erdos3.NativeWeightedRankIntervals.remove_weight line 512
  24. theorem OAI.Erdos3.exists_native_rank_relation line 562