OAI/Probability/FreeIsing/Conditioning/NoisyCopyDifference.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Problem367.CopyDifference.noisyAverageOnDifferences line 21
2. theorem OAI.Problem367.CopyDifference.diagonalReflection_involutive line 29
3. theorem OAI.Problem367.CopyDifference.noisyAverageOnDifferences_isSelfAdjoint line 37
4. theorem OAI.Problem367.CopyDifference.noisyAverageOnDifferences_norm_le line 42