OAI/Probability/FreeIsing/Estimates/NormalizedPositiveWindowRow.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Problem367.NormalizedInfiniteTimeEnergy.finiteRow_abs_le_one line 24
2. lemma OAI.Problem367.NormalizedInfiniteTimeEnergy.integrable_finiteRow_sq line 31
3. theorem OAI.Problem367.NormalizedInfiniteTimeEnergy.finiteRow_tendsto_ae_timeMeasure line 48
4. theorem OAI.Problem367.NormalizedInfiniteTimeEnergy.finiteRow_timeMeasure_meanSquare line 67
5. theorem OAI.Problem367.NormalizedInfiniteTimeEnergy.integral_finiteRow_sq_timeMeasure_le line 90
6. theorem OAI.Problem367.NormalizedInfiniteTimeEnergy.finiteRow_timeMeasure_error_bound line 128
7. theorem OAI.Problem367.NormalizedInfiniteTimeEnergy.finiteRow_timeMeasure_row_meanSquare line 180
8. theorem OAI.Problem367.NormalizedInfiniteTimeEnergy.finiteRow_timeMeasure_row_lintegral_tendsto line 208
9. theorem OAI.Problem367.NormalizedInfiniteTimeEnergy.finiteRow_timeMeasure_row_integral_tendsto line 244
10. theorem OAI.Problem367.NormalizedInfiniteTimeEnergy.finiteRow_positiveWindow_row_lintegral_tendsto line 277