OAI/Probability/FreeIsing/Gaussian/FiniteSignalFieldRecursion.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem367.tanh_add_eq_binaryFusion line 12

   Distinct definitions of this name: OAI/Probability/FreeIsing/Cavity/ArtanhFusion.lean:10 (different declaration text). Qualify references as OAI.Problem367.tanh_add_eq_binaryFusion@path.

2. theorem OAI.Problem367.artanh_binaryFusion line 20

   Distinct definitions of this name: OAI/Probability/FreeIsing/Cavity/ArtanhFusion.lean:22 (different declaration text). Qualify references as OAI.Problem367.artanh_binaryFusion@path.

3. theorem OAI.Problem367.artanh_condExp_spin_sup line 26
4. theorem OAI.Problem367.artanh_condExp_spin_finiteSignalField line 41
5. theorem OAI.Problem367.artanh_condExp_finite_observation line 70
6. theorem OAI.Problem367.artanh_condExp_own_and_finite_observation line 90