OAI/Probability/ClassicalON/FerromagneticMean.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ClassicalON.edgeHamiltonian line 17
2. def OAI.ClassicalON.edgeMean line 19
3. theorem OAI.ClassicalON.continuous_edgeHamiltonian line 22
4. def OAI.ClassicalON.EdgeCovarianceNonneg line 26
5. theorem OAI.ClassicalON.edgeMean_zero line 30
6. theorem OAI.ClassicalON.edgeMean_direction_derivative line 35
7. theorem OAI.ClassicalON.edgeMean_mono_couplings line 60
8. theorem OAI.ClassicalON.edgeMean_nonneg line 83