OAI/Probability/SignedSweeps/KernelTransition.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SignedSweeps.unitary_representation_adjoint line 13
2. lemma OAI.SignedSweeps.adjoint_finiteMean line 22
3. lemma OAI.SignedSweeps.unitary_finiteMean_adjoint line 26
4. lemma OAI.SignedSweeps.finiteProb_kernel_apply line 44
5. lemma OAI.SignedSweeps.tupleRepresentation_norm line 57
6. theorem OAI.SignedSweeps.tupleSweep_adjoint_eq_endpointKernel line 61
7. lemma OAI.SignedSweeps.tupleRealization_intertwines_adjoint_sweep line 88
8. theorem OAI.SignedSweeps.sweep_norm_le_of_adjoint_tuple_bound line 100