OAI/Probability/FreeIsing/Conditioning/CenteredCopyDifference.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Problem367.CopyDifference.inner_const_one_self line 16
2. lemma OAI.Problem367.CopyDifference.centered_source_cover line 24
3. lemma OAI.Problem367.CopyDifference.rangeClosure_centered_eq line 32
4. lemma OAI.Problem367.CopyDifference.norm_restrict_le_of_centered_source line 39
5. lemma OAI.Problem367.CopyDifference.average_intertwines_apply line 56
6. def OAI.Problem367.CopyDifference.averageOnDifferences line 71
7. lemma OAI.Problem367.CopyDifference.averageOnDifferences_isSelfAdjoint line 82
8. lemma OAI.Problem367.CopyDifference.norm_averageOnDifferences_le line 94