OAI/Combinatorics/Progressions/Estimates/AllocatedCandidateCommonFastGeometry.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.basis_generator_matrix_range line 16
  2. theorem OAI.Erdos3.exists_submodule_quotient_presentation_exp_height line 23
  3. theorem OAI.Erdos3.exists_bounded_submodule_quotient_section_with_coordinates line 51
  4. theorem OAI.Erdos3.exists_bounded_submodule_quotient_section line 97
  5. def OAI.Erdos3.allocatedCandidateCommonFastSectionInput line 130
  6. def OAI.Erdos3.allocatedCandidateCommonFastGeometryLog line 132
  7. def OAI.Erdos3.allocatedCandidateCommonFastCoordinateHeight line 135
  8. theorem OAI.Erdos3.allocatedCandidateCommonFastSectionInput_bounds line 138
  9. theorem OAI.Erdos3.allocatedCandidateCommonFastGeometryLog_bounds line 147
  10. theorem OAI.Erdos3.allocatedCandidateCommonFastCoordinateHeight_bounds line 158
  11. def OAI.Erdos3.allocatedCandidateCommonFastBudget line 172
  12. theorem OAI.Erdos3.allocatedCandidateCommonFastBudget_bounds line 176
  13. theorem OAI.Erdos3.allocatedCandidateCommonFastGeneratorHeight_le line 192
  14. theorem OAI.Erdos3.exists_allocatedCandidateCommonFastBudget line 198
  15. theorem OAI.Erdos3.NilpotentLieFiltration.exists_allocatedCandidateCommonFastGeometry line 232