OAI/Geometry/TamingCompatibility/Hodge/HodgeVolterraKernel.lean

GitHub source file

33 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.TamingCompatibility.GeometricHilbert.VolterraBounds.weight line 17
2. lemma OAI.TamingCompatibility.GeometricHilbert.VolterraBounds.weight_one_le line 19
3. lemma OAI.TamingCompatibility.GeometricHilbert.VolterraBounds.weight_pos line 25
4. lemma OAI.TamingCompatibility.GeometricHilbert.VolterraBounds.weight_symm line 28
5. lemma OAI.TamingCompatibility.GeometricHilbert.VolterraBounds.weight_submultiplicative line 31
6. lemma OAI.TamingCompatibility.GeometricHilbert.VolterraBounds.weight_continuous line 45
7. lemma OAI.TamingCompatibility.GeometricHilbert.VolterraBounds.spatial_convolution_bound line 51
8. lemma OAI.TamingCompatibility.GeometricHilbert.VolterraBounds.spatial_convolution_bound_right line 86
9. lemma OAI.TamingCompatibility.GeometricHilbert.VolterraBounds.time_integrand_bound line 122
10. lemma OAI.TamingCompatibility.GeometricHilbert.VolterraBounds.time_convolution_bound line 158
11. lemma OAI.TamingCompatibility.GeometricHilbert.SchurIntegration.product_integrable line 213
12. lemma OAI.TamingCompatibility.GeometricHilbert.SchurIntegration.product_integral_le line 233
13. lemma OAI.TamingCompatibility.GeometricHilbert.SchurIntegration.norm_integral_row line 246
14. lemma OAI.TamingCompatibility.GeometricHilbert.SchurIntegration.integral_row_bound line 266
15. lemma OAI.TamingCompatibility.GeometricHilbert.SchurIntegration.integral_row_bound_ae line 288
16. lemma OAI.TamingCompatibility.GeometricHilbert.SchurKernel.convolution_row line 322
17. abbrev OAI.TamingCompatibility.GeometricHilbert.VolterraKernel.Kernel line 367
18. def OAI.TamingCompatibility.GeometricHilbert.VolterraKernel.MeasurableKernel line 369
19. def OAI.TamingCompatibility.GeometricHilbert.VolterraKernel.spatial line 372
20. def OAI.TamingCompatibility.GeometricHilbert.VolterraKernel.convolution line 375
21. lemma OAI.TamingCompatibility.GeometricHilbert.VolterraKernel.spatial_measurable line 378
22. lemma OAI.TamingCompatibility.GeometricHilbert.VolterraKernel.convolution_measurable line 388
23. lemma OAI.TamingCompatibility.GeometricHilbert.VolterraKernel.kernel_section line 402
24. lemma OAI.TamingCompatibility.GeometricHilbert.VolterraKernel.spatial_section line 406
25. lemma OAI.TamingCompatibility.GeometricHilbert.VolterraKernel.product_section line 414
26. structure OAI.TamingCompatibility.GeometricHilbert.VolterraKernel.HeatBound line 423
27. lemma OAI.TamingCompatibility.GeometricHilbert.VolterraKernel.convolution_sup line 433
28. lemma OAI.TamingCompatibility.GeometricHilbert.VolterraKernel.weighted_section line 452
29. lemma OAI.TamingCompatibility.GeometricHilbert.VolterraKernel.spatial_row line 460
30. lemma OAI.TamingCompatibility.GeometricHilbert.VolterraKernel.convolution_row line 477
31. lemma OAI.TamingCompatibility.GeometricHilbert.VolterraKernel.spatial_col line 512
32. lemma OAI.TamingCompatibility.GeometricHilbert.VolterraKernel.convolution_col line 552
33. lemma OAI.TamingCompatibility.GeometricHilbert.VolterraKernel.convolution_heatBound line 586