OAI/Probability/FreeIsing/Conditioning/Characteristic.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Problem367.ConditionalCharacteristic.character line 14
2. theorem OAI.Problem367.ConditionalCharacteristic.measurable_character line 17
3. theorem OAI.Problem367.ConditionalCharacteristic.integrable_character line 22
4. theorem OAI.Problem367.ConditionalCharacteristic.map_restrict_eq_smul_of_condExp_character line 31
5. theorem OAI.Problem367.ConditionalCharacteristic.map_eq_of_condExp_character line 52
6. theorem OAI.Problem367.ConditionalCharacteristic.indepFun_of_condExp_character line 62
7. theorem OAI.Problem367.ConditionalCharacteristic.hasLaw_of_condExp_character line 79
8. theorem OAI.Problem367.ConditionalCharacteristic.gaussian_law_and_indep_of_condExp_character line 88