OAI/Geometry/TamingCompatibility/Hodge/HodgeKernelSeriesCore.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.TamingCompatibility.GeometricHilbert.KernelSeries.integrable_tsum_bound line 18
2. lemma OAI.TamingCompatibility.GeometricHilbert.KernelSeries.tsum_stronglyMeasurable line 42
3. def OAI.TamingCompatibility.GeometricHilbert.KernelSeries.clip line 52
4. lemma OAI.TamingCompatibility.GeometricHilbert.KernelSeries.clip_measurable line 56
5. lemma OAI.TamingCompatibility.GeometricHilbert.KernelSeries.clip_of_mem line 61
6. lemma OAI.TamingCompatibility.GeometricHilbert.KernelSeries.clip_of_not_mem line 65
7. lemma OAI.TamingCompatibility.GeometricHilbert.KernelSeries.heatBound_clip line 69
8. lemma OAI.TamingCompatibility.GeometricHilbert.KernelSeries.heatBound_neg line 79
9. def OAI.TamingCompatibility.GeometricHilbert.KernelSeries.term line 85
10. lemma OAI.TamingCompatibility.GeometricHilbert.KernelSeries.term_heatBound line 90
11. lemma OAI.TamingCompatibility.GeometricHilbert.KernelSeries.term_outside line 104
12. lemma OAI.TamingCompatibility.GeometricHilbert.KernelSeries.term_norm_summable line 109
13. lemma OAI.TamingCompatibility.GeometricHilbert.KernelSeries.weighted_tsum_L1 line 127
14. lemma OAI.TamingCompatibility.GeometricHilbert.KernelSeries.heatBound_tsum line 153
15. def OAI.TamingCompatibility.GeometricHilbert.KernelSeries.correction line 192
16. lemma OAI.TamingCompatibility.GeometricHilbert.KernelSeries.correction_heatBound line 195
17. lemma OAI.TamingCompatibility.GeometricHilbert.KernelSeries.heatBound_norm line 212
18. lemma OAI.TamingCompatibility.GeometricHilbert.KernelSeries.spatial_product_norm_bound line 219
19. lemma OAI.TamingCompatibility.GeometricHilbert.KernelSeries.spatial_tsum_right line 250
20. lemma OAI.TamingCompatibility.GeometricHilbert.KernelSeries.convolution_tsum_right line 272
21. lemma OAI.TamingCompatibility.GeometricHilbert.KernelSeries.correction_equation line 304