OAI/Combinatorics/BalancedRyser/Profiles/ProfileCoefficients.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Balanced.ProfileCoefficients.summable_abs_shift_sub line 13
  2. theorem OAI.Balanced.ProfileCoefficients.tsum_abs_shift_sub_le_two line 18
  3. theorem OAI.Balanced.ProfileCoefficients.summable_mul_weight line 39
  4. theorem OAI.Balanced.ProfileCoefficients.shifted_transform_sub line 46
  5. theorem OAI.Balanced.ProfileCoefficients.shift_fst_injective line 58
  6. theorem OAI.Balanced.ProfileCoefficients.shift_snd_injective line 65
  7. theorem OAI.Balanced.ProfileCoefficients.d_invisibility_iff line 72
  8. theorem OAI.Balanced.ProfileCoefficients.c_invisibility_iff line 89
  9. theorem OAI.Balanced.ProfileCoefficients.rpow_weight_abs_le_one line 106
  10. theorem OAI.Balanced.ProfileCoefficients.d_transform_sub line 111
  11. theorem OAI.Balanced.ProfileCoefficients.c_transform_sub line 118
  12. theorem OAI.Balanced.ProfileCoefficients.tsum_shift_fst line 125
  13. theorem OAI.Balanced.ProfileCoefficients.tsum_shift_snd line 133
  14. theorem OAI.Balanced.ProfileCoefficients.d_transform_reindex line 141
  15. theorem OAI.Balanced.ProfileCoefficients.c_transform_reindex line 152
  16. theorem OAI.Balanced.ProfileCoefficients.original_d_transform_sub line 163
  17. theorem OAI.Balanced.ProfileCoefficients.original_c_transform_sub line 172