OAI/Combinatorics/Progressions/Estimates/RationalPowerHeight.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.rationalLogHeight_le_iff line 13
  2. theorem OAI.Erdos3.rationalLogHeight_nonneg line 19
  3. theorem OAI.Erdos3.rationalHeightLE_ceil_exp line 24
  4. theorem OAI.Erdos3.rationalLogHeight_le_of_height line 29
  5. theorem OAI.Erdos3.one_le_ceil_exp line 35
  6. theorem OAI.Erdos3.ceil_exp_le_exp_add_one line 38
  7. theorem OAI.Erdos3.NilpotentLieFiltration.exists_bounded_sorted_adapted_basis_logHeight line 61
  8. def OAI.Erdos3.boundedRationalCandidates line 106
  9. theorem OAI.Erdos3.mem_boundedRationalCandidates line 111
  10. theorem OAI.Erdos3.boundedRationalCandidates_card line 122
  11. theorem OAI.Erdos3.finite_card_bounded_height_arrays line 130
  12. theorem OAI.Erdos3.exists_bounded_normalized_square line 161
  13. theorem OAI.Erdos3.rational_functional_value_logHeight line 201
  14. theorem OAI.Erdos3.linearMap_coordinate_logHeight line 236
  15. theorem OAI.Erdos3.RationalFilteredNilmanifold.MultidegreeStructure.exists_layer_basis line 274
  16. theorem OAI.Erdos3.RationalFilteredNilmanifold.MultidegreeStructure.exists_ordinary_layer_basis line 281
  17. theorem OAI.Erdos3.RationalFilteredNilmanifold.exists_positive_layer_basis line 302
  18. theorem OAI.Erdos3.RationalFilteredNilmanifold.exists_native_complex_reconstruction line 332
  19. theorem OAI.Erdos3.RationalHeightLE.pow line 389
  20. theorem OAI.Erdos3.ceil_exp_power_le_exp line 395