OAI/Geometry/TamingCompatibility/Concentration/ConcentrationKernel.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.TamingCompatibility.Concentration.rationalKernel line 13
2. lemma OAI.TamingCompatibility.Concentration.rationalKernel_nonneg line 16
3. lemma OAI.TamingCompatibility.Concentration.rationalKernel_pos line 21
4. lemma OAI.TamingCompatibility.Concentration.rationalKernel_smooth line 25
5. lemma OAI.TamingCompatibility.Concentration.rationalKernel_deriv line 30
6. lemma OAI.TamingCompatibility.Concentration.rationalKernel_neg line 44
7. lemma OAI.TamingCompatibility.Concentration.compact_continuous_bound line 48
8. lemma OAI.TamingCompatibility.Concentration.hasFDerivAt_finite_convolution line 61
9. lemma OAI.TamingCompatibility.Concentration.finite_convolution_deriv line 80
10. lemma OAI.TamingCompatibility.Concentration.finite_convolution_smooth line 92
11. def OAI.TamingCompatibility.Concentration.cutKernel line 106
12. lemma OAI.TamingCompatibility.Concentration.cutKernel_smooth line 108
13. lemma OAI.TamingCompatibility.Concentration.cutKernel_compact line 112
14. lemma OAI.TamingCompatibility.Concentration.cutKernel_deriv line 115
15. def OAI.TamingCompatibility.Concentration.radialCoefficient line 138
16. lemma OAI.TamingCompatibility.Concentration.radialCoefficient_nonneg line 140
17. lemma OAI.TamingCompatibility.Concentration.rational_cutoff_bound line 144
18. lemma OAI.TamingCompatibility.Concentration.radialCoefficient_mul_defect_bound line 153
19. lemma OAI.TamingCompatibility.Concentration.rational_defect_tendsto_zero line 164
20. lemma OAI.TamingCompatibility.Concentration.rational_geometric_error_tendsto_zero line 192