OAI/Geometry/TamingCompatibility/Hodge/HodgeKernelGammaBounds.lean

GitHub source file

35 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.TamingCompatibility.GeometricHilbert.HodgeKernelBounds.rapidConstant line 13
2. lemma OAI.TamingCompatibility.GeometricHilbert.HodgeKernelBounds.rapidConstant_pos line 16
3. lemma OAI.TamingCompatibility.GeometricHilbert.HodgeKernelBounds.exp_neg_le_rapid line 21
4. def OAI.TamingCompatibility.GeometricHilbert.HodgeKernelBounds.moment line 40
5. lemma OAI.TamingCompatibility.GeometricHilbert.HodgeKernelBounds.moment_integrable line 42
6. lemma OAI.TamingCompatibility.GeometricHilbert.HodgeKernelBounds.moment_integral line 48
7. lemma OAI.TamingCompatibility.GeometricHilbert.HodgeKernelBounds.moment_pos line 57
8. def OAI.TamingCompatibility.GeometricHilbert.HodgeKernelBounds.profile line 61
9. lemma OAI.TamingCompatibility.GeometricHilbert.HodgeKernelBounds.profile_nonneg line 64
10. lemma OAI.TamingCompatibility.GeometricHilbert.HodgeKernelBounds.gaussian_exponent_split line 69
11. lemma OAI.TamingCompatibility.GeometricHilbert.HodgeKernelBounds.profile_le_exp line 86
12. lemma OAI.TamingCompatibility.GeometricHilbert.HodgeKernelBounds.profile_integrable line 100
13. lemma OAI.TamingCompatibility.GeometricHilbert.HodgeKernelBounds.profile_integral_le_exp line 110
14. lemma OAI.TamingCompatibility.GeometricHilbert.HodgeKernelBounds.profile_integral_le_rapid line 122
15. def OAI.TamingCompatibility.GeometricHilbert.HodgeKernelBounds.truncatedProfile line 133
16. lemma OAI.TamingCompatibility.GeometricHilbert.HodgeKernelBounds.truncatedProfile_nonneg line 136
17. lemma OAI.TamingCompatibility.GeometricHilbert.HodgeKernelBounds.truncatedProfile_le line 142
18. lemma OAI.TamingCompatibility.GeometricHilbert.HodgeKernelBounds.leading_profile_lower line 149
19. lemma OAI.TamingCompatibility.GeometricHilbert.HodgeKernelBounds.truncatedProfile_lower line 168
20. def OAI.TamingCompatibility.GeometricHilbert.HodgeKernelBounds.leading line 191
21. def OAI.TamingCompatibility.GeometricHilbert.HodgeKernelBounds.leadingConstant line 195
22. lemma OAI.TamingCompatibility.GeometricHilbert.HodgeKernelBounds.leadingConstant_pos line 198
23. lemma OAI.TamingCompatibility.GeometricHilbert.HodgeKernelBounds.leading_nonneg line 204
24. lemma OAI.TamingCompatibility.GeometricHilbert.HodgeKernelBounds.leading_upper line 208
25. lemma OAI.TamingCompatibility.GeometricHilbert.HodgeKernelBounds.leading_lower line 220
26. def OAI.TamingCompatibility.GeometricHilbert.HodgeKernelBounds.gaussianError line 231
27. lemma OAI.TamingCompatibility.GeometricHilbert.HodgeKernelBounds.gaussianError_upper line 234
28. def OAI.TamingCompatibility.GeometricHilbert.HodgeKernelBounds.gammaTail line 245
29. lemma OAI.TamingCompatibility.GeometricHilbert.HodgeKernelBounds.gammaTail_nonneg line 247
30. lemma OAI.TamingCompatibility.GeometricHilbert.HodgeKernelBounds.gammaTail_le line 252
31. lemma OAI.TamingCompatibility.GeometricHilbert.HodgeKernelBounds.exp_neg_le_power line 277
32. lemma OAI.TamingCompatibility.GeometricHilbert.HodgeKernelBounds.gammaTail_small_scale line 287
33. lemma OAI.TamingCompatibility.GeometricHilbert.HodgeKernelBounds.power_absorb line 300
34. lemma OAI.TamingCompatibility.GeometricHilbert.HodgeKernelBounds.gaussianError_nonneg line 325
35. lemma OAI.TamingCompatibility.GeometricHilbert.HodgeKernelBounds.gammaTail_spatial line 332