OAI/Probability/FreeIsing/Ising/CanonicalArtanhIdentification.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem367.IsingObservationFactor.canonical_artanh_uniformSum_memLp line 13
2. theorem OAI.Problem367.IsingObservationFactor.canonical_artanh_eq_of_meanSquare_limit line 43
3. theorem OAI.Problem367.IsingObservationFactor.canonical_artanh_eq_all_of_meanSquare_limits line 63