OAI/Probability/FreeIsing/Estimates/NormalizedCriticalRowConvergence.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem367.NormalizedInfiniteTimeEnergy.lintegral_finiteRow_le line 16
2. theorem OAI.Problem367.NormalizedInfiniteTimeEnergy.lintegral_rowError_ne_top line 45
3. theorem OAI.Problem367.NormalizedInfiniteTimeEnergy.rowError_integrable line 66
4. theorem OAI.Problem367.NormalizedInfiniteTimeEnergy.lintegral_finiteRow_le_criticalEnvelope line 94
5. theorem OAI.Problem367.NormalizedInfiniteTimeEnergy.lintegral_rowError_le_criticalEnvelope line 127
6. theorem OAI.Problem367.NormalizedInfiniteTimeEnergy.finiteRow_critical_row_lintegral_tendsto line 155
7. theorem OAI.Problem367.NormalizedInfiniteTimeEnergy.finiteRow_critical_row_integral_tendsto line 198