OAI/Probability/FreeIsing/Ising/StemRerootAverage.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Problem367.IsingOrientedPath.orderedEdgeFactor line 16
2. theorem OAI.Problem367.IsingOrientedPath.orderedEdgeFactor_mem_Icc line 21
3. theorem OAI.Problem367.IsingOrientedPath.rootEdgeProduct_orderedEdgeFactor line 29
4. theorem OAI.Problem367.IsingOrientedPath.orderedEdgeFactor_relabel_ae line 37
5. theorem OAI.Problem367.IsingOrientedPath.extensionAverage_le_restricted_average_relabel line 48
6. theorem OAI.Problem367.IsingOrientedPath.measure_extensionAverage_gt_le_restricted_average_ge line 74