OAI/Analysis/AncientFlat/Regularity/SchauderLag.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ParabolicSchauder.lagMajorant line 8
2. lemma OAI.ParabolicSchauder.integral_short_power line 10
3. lemma OAI.ParabolicSchauder.integrable_short_power line 14
4. lemma OAI.ParabolicSchauder.integrable_lagMajorant line 18
5. lemma OAI.ParabolicSchauder.integral_lagMajorant line 39
6. lemma OAI.ParabolicSchauder.lagMajorant_nonneg line 63
7. lemma OAI.ParabolicSchauder.norm_integral_lag_split line 70
8. lemma OAI.ParabolicSchauder.integrable_reverse_power line 100
9. lemma OAI.ParabolicSchauder.integral_reverse_power line 107
10. lemma OAI.ParabolicSchauder.norm_integral_reverse_power line 113
11. lemma OAI.ParabolicSchauder.integral_Ioo_split line 122