OAI/MathematicalPhysics/PEPSMove/ConditionalCollision.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PolynomialPEPS.PhysicalMove.ConditionalCollision.coefficient line 18
2. def OAI.PolynomialPEPS.PhysicalMove.ConditionalCollision.inputSlice line 21
3. theorem OAI.PolynomialPEPS.PhysicalMove.ConditionalCollision.inputSlice_norm_sq line 26
4. theorem OAI.PolynomialPEPS.PhysicalMove.ConditionalCollision.rows_apply_slice line 32
5. theorem OAI.PolynomialPEPS.PhysicalMove.ConditionalCollision.collision_le line 49
6. abbrev OAI.PolynomialPEPS.PhysicalMove.ConditionalCollision.density line 108
7. theorem OAI.PolynomialPEPS.PhysicalMove.ConditionalCollision.density_pos line 112
8. theorem OAI.PolynomialPEPS.PhysicalMove.ConditionalCollision.density_marginal line 116
9. theorem OAI.PolynomialPEPS.PhysicalMove.ConditionalCollision.conditional_spectral_mgf line 127