OAI/Combinatorics/SumProduct/Alignment/WeightedLinear01.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.RationalLattice.logHomLinear_displacement_weighted line 31
  2. lemma OAI.RationalLattice.logHomLinear_weighted line 49
  3. theorem OAI.RationalLattice.affine_log_displacement_weighted line 58
  4. def OAI.WeightedLinear.level line 83
  5. def OAI.WeightedLinear.Preserves line 89
  6. lemma OAI.WeightedLinear.single_mem line 93
  7. lemma OAI.WeightedLinear.basis_expansion line 99
  8. lemma OAI.WeightedLinear.apply_eq_sum line 104
  9. lemma OAI.WeightedLinear.Preserves.coeff line 113
  10. lemma OAI.WeightedLinear.preserves_of_coeff line 119
  11. lemma OAI.WeightedLinear.Preserves.weighted line 131
  12. theorem OAI.WeightedLinear.exists_rightInverse line 139
  13. theorem OAI.WeightedLinear.lifted_displacement_weighted line 169
  14. def OAI.PolynomialShearPoint.pointMap line 200
  15. lemma OAI.PolynomialShearPoint.eval_pointMap line 203
  16. lemma OAI.PolynomialShearPoint.pointMap_comp line 211
  17. lemma OAI.PolynomialShearPoint.pointMap_id line 216
  18. def OAI.PolynomialShearPoint.pointEquiv line 220
  19. theorem OAI.PolynomialShearPoint.exists_shear line 228
  20. lemma OAI.AsymptoticProbability.levy_bound line 263
  21. lemma OAI.AsymptoticProbability.same_weak_limit line 279
  22. lemma OAI.AsymptoticProbability.pushed_event_bound line 296
  23. lemma OAI.AsymptoticProbability.cluster_invariant line 320
  24. lemma OAI.AsymptoticProbability.weak_haar_of_unique line 347