OAI/Dynamics/ConditionalShuffle/InjectionKernel.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.Thorp.Conditional.Reset.Injection line 10
  2. def OAI.Thorp.Conditional.Reset.act line 12
  3. lemma OAI.Thorp.Conditional.Reset.act_apply line 14
  4. lemma OAI.Thorp.Conditional.Reset.act_mul line 17
  5. lemma OAI.Thorp.Conditional.Reset.act_one line 20
  6. lemma OAI.Thorp.Conditional.Reset.act_eq_iff line 22
  7. def OAI.Thorp.Conditional.Reset.actEquiv line 28
  8. lemma OAI.Thorp.Conditional.Reset.uniform_injection line 34
  9. def OAI.Thorp.Conditional.Reset.kernel line 43
  10. lemma OAI.Thorp.Conditional.Reset.kernel_nonneg line 46
  11. lemma OAI.Thorp.Conditional.Reset.kernel_row_sum line 49
  12. lemma OAI.Thorp.Conditional.Reset.kernel_column_sum line 52
  13. def OAI.Thorp.Conditional.Reset.toInjection line 60
  14. lemma OAI.Thorp.Conditional.Reset.toInjection_coe line 63
  15. lemma OAI.Thorp.Conditional.Reset.injection_tv_le line 66
  16. lemma OAI.Thorp.Conditional.Reset.kernel_row_bound line 75
  17. lemma OAI.Thorp.Conditional.Reset.reflection_column line 87
  18. lemma OAI.Thorp.Conditional.Reset.kernel_column_bound line 111