OAI/Combinatorics/Progressions/Lattices/PrincipalResidueMixture.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.integerMappedCubeTuple line 9
  2. theorem OAI.Erdos3.integerMappedCubeTuple_residue line 14
  3. def OAI.Erdos3.integerMappedJetMatrix line 33
  4. theorem OAI.Erdos3.integerMappedJetMatrix_residue line 38
  5. theorem OAI.Erdos3.integerMappedCubeTuple_normalized line 46
  6. theorem OAI.Erdos3.integerMappedCubeTuple_residue_both line 64
  7. theorem OAI.Erdos3.integerMappedJetMatrix_residue_both line 84
  8. abbrev OAI.Erdos3.PrincipalIntegerTuples line 102
  9. def OAI.Erdos3.principalTupleIntegers line 105
  10. def OAI.Erdos3.principalTupleNormalized line 110
  11. def OAI.Erdos3.principalTupleResidues line 115
  12. def OAI.Erdos3.principalResidueWeights line 119
  13. theorem OAI.Erdos3.principalResidueWeights_support line 127
  14. theorem OAI.Erdos3.principalResidueWeights_matrix line 139
  15. def OAI.Erdos3.principalTupleWeights line 164
  16. def OAI.Erdos3.principalResidueLabel line 170
  17. theorem OAI.Erdos3.principalResidueCell_eq line 174
  18. theorem OAI.Erdos3.principalResidueCell_mass_pos line 187
  19. theorem OAI.Erdos3.principalResidueWeights_eq_condition line 199
  20. theorem OAI.Erdos3.principalResidue_fiberMean line 213