OAI/Combinatorics/SumProduct/Alignment/RationalLattice24.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.WeightedBoxes.boxLaw line 25
  2. lemma OAI.WeightedBoxes.boxLaw_eq line 32
  3. lemma OAI.WeightedBoxes.pointMap_continuous line 37
  4. theorem OAI.WeightedBoxes.boxLaw_shear_invariance line 45
  5. def OAI.RationalLattice.expQuotient line 83
  6. def OAI.RationalLattice.weightedCoverLaw line 87
  7. lemma OAI.RationalLattice.weightedCover_translation_invariance line 93
  8. theorem OAI.RationalLattice.weightedCover_weak_haar line 122
  9. lemma OAI.AsymptoticProbability.map_event_bound line 155
  10. def OAI.RationalLattice.weightedShearLaw line 175
  11. lemma OAI.RationalLattice.weightedShearLaw_event_bound line 180
  12. theorem OAI.RationalLattice.weightedShear_weak_haar line 192
  13. theorem OAI.RationalLattice.weightedShear_pointImage_limit line 214
  14. instance OAI.PolynomialShearPoint.shearPointAction line 240
  15. lemma OAI.PolynomialShearPoint.shear_smul line 249
  16. abbrev OAI.PolynomialShearPoint.CoverGroup line 252
  17. abbrev OAI.PolynomialShearPoint.CoverState line 253
  18. instance OAI.PolynomialShearPoint.coverAction line 255
  19. lemma OAI.PolynomialShearPoint.cover_smul_fst line 265
  20. lemma OAI.PolynomialShearPoint.cover_smul_snd line 267
  21. lemma OAI.PolynomialShearPoint.cover_lowerCentralSeries line 270