OAI/Probability/FreeIsing/Gaussian/RerootedFreeLawNoise.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Problem367.RootedBroadcast.rerootedNoise line 16
2. lemma OAI.Problem367.RootedBroadcast.measurable_rerootedNoise line 20
3. lemma OAI.Problem367.RootedBroadcast.rerootedNoise_root line 24
4. lemma OAI.Problem367.RootedBroadcast.rerootedNoise_root_of_map line 30
5. lemma OAI.Problem367.RootedBroadcast.rerootedNoise_nonroot line 36
6. lemma OAI.Problem367.HasFreeIsingLaw.map_rerootedNoise line 44
7. lemma OAI.Problem367.HasFreeIsingLaw.iIndepFun_rerootedNoise line 55
8. lemma OAI.Problem367.HasFreeIsingLaw.indepFun_rerootedNoise_blocks line 76
9. lemma OAI.Problem367.HasFreeIsingLaw.iIndepFun_rerootedNoise_blocks line 86
10. lemma OAI.Problem367.HasFreeIsingLaw.map_rerootedNoise_blocks line 96