OAI/Probability/FreeIsing/Gaussian/GlobalFreeLawNoise.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Problem367.RootedBroadcast.noiseFromSpins_restrict line 15
2. lemma OAI.Problem367.HasFreeIsingLaw.map_noiseFromSpins line 32
3. lemma OAI.Problem367.HasFreeIsingLaw.map_noiseFromSpins_coord line 61
4. lemma OAI.Problem367.HasFreeIsingLaw.iIndepFun_noiseFromSpins line 72
5. lemma OAI.Problem367.HasFreeIsingLaw.eq_map_ofNoise line 87