OAI/Probability/FreeIsing/Ising/CopyResponseRowSummability.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem367.IsingCopyResponseRowPaths.row_identDistrib_gaussian line 17
2. theorem OAI.Problem367.IsingCopyResponseRowPaths.integrable_row_sq_and_integral_le line 33
3. theorem OAI.Problem367.IsingCopyResponseRowPaths.observation_row_energy line 43
4. theorem OAI.Problem367.IsingCopyResponseRowPaths.copies_rows_summable_ae line 65
5. theorem OAI.Problem367.IsingCopyResponseRowPaths.integrable_copies_row_energies line 78
6. theorem OAI.Problem367.IsingCopyResponseRowPaths.integral_density_le_shell_energies_of_positive line 88