OAI/Probability/FreeIsing/Estimates/BalancedLatentMean.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem367.integrable_of_unit_bounds line 14
2. theorem OAI.Problem367.integral_binary_channel_le_two_integral line 22
3. theorem OAI.Problem367.condExp_binary_channel_le_two_integral line 61
4. theorem OAI.Problem367.condExp_binary_channel_comp_le_two_integral line 78