OAI/Probability/FreeIsing/Energy/RowEnergyL1.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Problem367.RowEnergyL1.abs_sq_sub_sq_le_young line 12
2. theorem OAI.Problem367.RowEnergyL1.abs_tsum_sq_sub_le line 28
3. theorem OAI.Problem367.RowEnergyL1.tendsto_integral_abs_tsum_sq_sub line 50
4. theorem OAI.Problem367.RowEnergyL1.tendsto_integral_abs_mul_sub line 107
5. theorem OAI.Problem367.RowEnergyL1.tendsto_integral_abs_multiplier_tsum_sq_sub line 161
6. theorem OAI.Problem367.RowEnergyL1.integral_abs_timePrimitive_le line 185
7. theorem OAI.Problem367.RowEnergyL1.integral_abs_timePrimitive_sub_le line 207
8. theorem OAI.Problem367.RowEnergyL1.timePrimitive_sub_tendsto_uniform_L1 line 229
9. theorem OAI.Problem367.RowEnergyL1.tendsto_integral_abs_mul_sub_of_tendstoInMeasure line 244
10. theorem OAI.Problem367.RowEnergyL1.tendstoInMeasure_of_integral_sq_sub line 262
11. theorem OAI.Problem367.RowEnergyL1.tendsto_integral_abs_mul_sub_of_meanSquare line 278