OAI/Combinatorics/Progressions/Linear/RealDualRationalBounds.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.realDualBasis line 15
  2. theorem OAI.Erdos3.realDualBasis_inl line 18
  3. theorem OAI.Erdos3.realDualBasis_inr line 22
  4. theorem OAI.Erdos3.realDualBasis_repr_inl line 26
  5. theorem OAI.Erdos3.realDualBasis_repr_inr line 30
  6. def OAI.Erdos3.dualStructureConstants line 34
  7. theorem OAI.Erdos3.realDualBasis_structure line 40
  8. theorem OAI.Erdos3.dualStructureConstants_height line 48
  9. theorem OAI.Erdos3.dual_basis_bound line 64
  10. theorem OAI.Erdos3.exists_dual_coordinate_operation_bound line 75
  11. def OAI.Erdos3.rationalDualBasis line 184
  12. theorem OAI.Erdos3.rationalDualBasis_inl line 187
  13. theorem OAI.Erdos3.rationalDualBasis_inr line 191
  14. theorem OAI.Erdos3.rationalDualBasis_repr_inl line 195
  15. theorem OAI.Erdos3.rationalDualBasis_repr_inr line 199
  16. theorem OAI.Erdos3.rationalDualBasis_structure line 203
  17. theorem OAI.Erdos3.rationalDualBasis_structure_height line 209
  18. theorem OAI.Erdos3.rationalDualBasis_grid_iff line 215
  19. theorem OAI.Erdos3.exists_rational_dual_operation_grid line 243
  20. theorem OAI.Erdos3.real_dual_log_grid_of_rational line 338
  21. theorem OAI.Erdos3.real_dual_adjoint_grid_of_rational line 371
  22. theorem OAI.Erdos3.exists_real_dual_operation_grid line 393