OAI/Probability/Subsphere/Mixture/Haar.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. instance OAI.SubsphereCurrent.Mixture.orthogonal_probability line 13
  2. instance OAI.SubsphereCurrent.Mixture.orthogonal_haar line 16
  3. instance OAI.SubsphereCurrent.Mixture.orthogonal_right line 20
  4. def OAI.SubsphereCurrent.Mixture.act line 25
  5. lemma OAI.SubsphereCurrent.Mixture.continuous_act line 27
  6. lemma OAI.SubsphereCurrent.Mixture.act_mul line 31
  7. lemma OAI.SubsphereCurrent.Mixture.act_one line 33
  8. lemma OAI.SubsphereCurrent.Mixture.act_norm line 35
  9. lemma OAI.SubsphereCurrent.Mixture.exists_act line 37
  10. lemma OAI.SubsphereCurrent.Mixture.haar_integral_independent line 46
  11. lemma OAI.SubsphereCurrent.Mixture.haar_eval_integral line 55
  12. lemma OAI.SubsphereCurrent.Mixture.haar_eval_preserving line 73
  13. lemma OAI.SubsphereCurrent.Mixture.blockIso_apply line 100
  14. lemma OAI.SubsphereCurrent.Mixture.continuous_blockIso line 107
  15. lemma OAI.SubsphereCurrent.Mixture.blockIso_one line 115
  16. lemma OAI.SubsphereCurrent.Mixture.blockIso_on_left line 119
  17. lemma OAI.SubsphereCurrent.Mixture.blockIso_on_right line 124
  18. lemma OAI.SubsphereCurrent.Mixture.blockIso_mul line 129
  19. lemma OAI.SubsphereCurrent.Mixture.blockIso_comp line 134