OAI/Probability/FreeIsing/Conditioning/CutLevelConditionalMean.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem367.RootedBroadcast.cutSpins_coordinate_fair line 20
2. theorem OAI.Problem367.RootedBroadcast.condExp_noisy_factor_cone_le_two_integral line 32
3. theorem OAI.Problem367.freeIsingMeasure_condExp_cutLevel_observable_le_two_integral line 91
4. theorem OAI.Problem367.HasFreeIsingLaw.condExp_cutLevel_observable_le_two_integral line 157