OAI/Probability/FreeIsing/Trees/NoisyCutLevelIndependence.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem367.RootedBroadcast.map_cutSpins_cutLabels_noises line 21
2. theorem OAI.Problem367.RootedBroadcast.iCondIndepFun_noisy_factor_cutLevel line 66
3. theorem OAI.Problem367.freeIsingMeasure_iCondIndepFun_noisy_cutLevel line 130
4. theorem OAI.Problem367.HasFreeIsingLaw.iCondIndepFun_noisy_cutLevel line 167
5. theorem OAI.Problem367.HasFreeIsingLaw.iCondIndepFun_cutLevel_observables line 187
6. theorem OAI.Problem367.HasFreeIsingLaw.iIndepFun_cutLevel_observables_cond line 208