OAI/Combinatorics/SumProduct/Alignment/HarmonicTranslation01.lean

GitHub source file

35 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.HarmonicTranslation.mass line 21
  2. def OAI.HarmonicTranslation.eval line 22
  3. def OAI.HarmonicTranslation.l1 line 23
  4. lemma OAI.HarmonicTranslation.mass_sub line 26
  5. lemma OAI.HarmonicTranslation.eval_sub line 30
  6. lemma OAI.HarmonicTranslation.mass_nonneg line 34
  7. lemma OAI.HarmonicTranslation.eval_bound line 38
  8. theorem OAI.HarmonicTranslation.l1_le_twice_edge line 51
  9. def OAI.HarmonicTranslation.shift line 92
  10. lemma OAI.HarmonicTranslation.shift_apply line 94
  11. lemma OAI.HarmonicTranslation.mass_shift line 99
  12. lemma OAI.HarmonicTranslation.eval_shift line 102
  13. lemma OAI.HarmonicTranslation.shift_zero line 106
  14. lemma OAI.HarmonicTranslation.shift_shift line 107
  15. lemma OAI.HarmonicTranslation.shift_sub line 113
  16. lemma OAI.HarmonicTranslation.l1_shift line 117
  17. def OAI.HarmonicTranslation.raw line 122
  18. lemma OAI.HarmonicTranslation.raw_apply line 132
  19. lemma OAI.HarmonicTranslation.raw_nonneg line 137
  20. lemma OAI.HarmonicTranslation.raw_le_inv line 144
  21. lemma OAI.HarmonicTranslation.raw_outside_lower line 151
  22. lemma OAI.HarmonicTranslation.outside_edge line 157
  23. theorem OAI.HarmonicTranslation.raw_translation_nonneg line 177
  24. lemma OAI.HarmonicTranslation.l1_neg line 192
  25. lemma OAI.HarmonicTranslation.l1_sub_comm line 197
  26. lemma OAI.HarmonicTranslation.l1_translation_neg line 200
  27. theorem OAI.HarmonicTranslation.raw_translation line 204
  28. lemma OAI.HarmonicTranslation.sum_le_mass line 213
  29. theorem OAI.HarmonicTranslation.raw_mass_lower line 221
  30. def OAI.HarmonicTranslation.law line 270
  31. lemma OAI.HarmonicTranslation.mass_smul line 272
  32. lemma OAI.HarmonicTranslation.l1_smul line 277
  33. lemma OAI.HarmonicTranslation.shift_smul line 283
  34. lemma OAI.HarmonicTranslation.mass_law line 287
  35. theorem OAI.HarmonicTranslation.law_translation line 294