OAI/Combinatorics/Progressions/Linear/RankPreparationProjectedAxisBudget.lean

GitHub source file

46 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.preparationHeight line 13
  2. theorem OAI.Erdos3.preparationExponent_pos line 16
  3. theorem OAI.Erdos3.preparationExponent_mono line 21
  4. theorem OAI.Erdos3.preparationHeight_pos line 27
  5. theorem OAI.Erdos3.preparationHeight_le_exp line 33
  6. theorem OAI.Erdos3.preparationHeight_mono line 37
  7. theorem OAI.Erdos3.rankCutDirectionHeight_le_preparationHeight line 43
  8. def OAI.Erdos3.RankPreparationFamily.PreparedHeights line 62
  9. theorem OAI.Erdos3.RankPreparationFamily.PreparedHeights.descend line 65
  10. def OAI.Erdos3.RankPreparationFamily.initial line 99
  11. theorem OAI.Erdos3.RankPreparationFamily.initial_potential line 102
  12. theorem OAI.Erdos3.RankPreparationFamily.initial_value line 112
  13. theorem OAI.Erdos3.RankPreparationFamily.initial_sized line 119
  14. theorem OAI.Erdos3.RankPreparationFamily.initial_heights line 130
  15. theorem OAI.Erdos3.RankPreparationLayer.empty_samplingRank line 155
  16. def OAI.Erdos3.RankPreparationFamily.pad line 168
  17. theorem OAI.Erdos3.RankPreparationFamily.pad_apply_lt line 172
  18. theorem OAI.Erdos3.RankPreparationFamily.pad_apply_ge line 176
  19. theorem OAI.Erdos3.RankPreparationFamily.pad_apply_castLE line 180
  20. theorem OAI.Erdos3.RankPreparationFamily.pad_valid line 184
  21. theorem OAI.Erdos3.RankPreparationFamily.PreparedHeights.pad line 193
  22. theorem OAI.Erdos3.RankPreparationFamily.pad_samplingRank line 204
  23. theorem OAI.Erdos3.RankPreparationFamily.pad_degreeLE line 215
  24. theorem OAI.Erdos3.RankPreparationFamily.pad_coefficients_mem line 225
  25. theorem OAI.Erdos3.RankPreparationFamily.pad_coordinate_card_le line 235
  26. theorem OAI.Erdos3.RankPreparationFamily.Sized.pad line 245
  27. theorem OAI.Erdos3.RankPreparationFamily.pad_sum line 257
  28. theorem OAI.Erdos3.RankPreparationFamily.pad_value line 273
  29. theorem OAI.Erdos3.RankPreparationFamily.pad_coordinate_card line 277
  30. def OAI.Erdos3.RankPreparationLayer.euclideanEquiv line 299
  31. theorem OAI.Erdos3.RankPreparationLayer.euclidean_finrank line 303
  32. theorem OAI.Erdos3.RankPreparationLayer.rank_add_orthogonal_finrank line 306
  33. theorem OAI.Erdos3.RankPreparationLayer.lattice_full line 310
  34. theorem OAI.Erdos3.RankPreparationLayer.exists_uniform_chart line 314
  35. theorem OAI.Erdos3.RankPreparationFamily.PreparedHeights.lattice_full line 333
  36. theorem OAI.Erdos3.RankPreparationFamily.PreparedHeights.coefficientTorus_compact line 339
  37. theorem OAI.Erdos3.RankPreparationFamily.PreparedHeights.exists_uniform_charts line 345
  38. def OAI.Erdos3.RankPreparationLayer.integralCoordinateBasis line 376
  39. theorem OAI.Erdos3.RankPreparationLayer.integralCoordinateBasis_card line 382
  40. theorem OAI.Erdos3.RankPreparationLayer.integralCoordinateBasis_integer line 389
  41. def OAI.Erdos3.RankPreparationLayer.integralCoordinateMatrix line 401
  42. theorem OAI.Erdos3.RankPreparationLayer.integralCoordinateMatrix_cast line 408
  43. def OAI.Erdos3.RankPreparationLayer.shortIntegralBasisNormBound line 427
  44. theorem OAI.Erdos3.RankPreparationLayer.exists_short_integral_basis line 433
  45. theorem OAI.Erdos3.basisAxisScale_jointRationalSpace_le_exp line 464
  46. theorem OAI.Erdos3.RankPreparationLayer.basisAxisScale_le_exp line 507