OAI/Geometry/TamingCompatibility/Hodge/HodgePairingIntegral.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.TamingCompatibility.GeometricHilbert.hodgeRegularization_symmetric line 24
2. def OAI.TamingCompatibility.GeometricHilbert.HodgeSmoothingCover.pairingEvaluationVector line 38
3. lemma OAI.TamingCompatibility.GeometricHilbert.HodgeSmoothingCover.pairingEvaluationVector_continuous line 41
4. lemma OAI.TamingCompatibility.GeometricHilbert.HodgeSmoothingCover.pairingEvaluationVector_integrable line 46
5. lemma OAI.TamingCompatibility.GeometricHilbert.HodgeSmoothingCover.pairingEvaluationVector_pair line 52
6. lemma OAI.TamingCompatibility.GeometricHilbert.HodgeSmoothingCover.pairingEvaluationVector_integral line 59
7. lemma OAI.TamingCompatibility.GeometricHilbert.HodgeSmoothingCover.pairingEvaluationVector_gram line 73
8. lemma OAI.TamingCompatibility.GeometricHilbert.hodgeGammaShift_integrable line 109
9. def OAI.TamingCompatibility.GeometricHilbert.hodgeGammaShiftLinear line 124
10. lemma OAI.TamingCompatibility.GeometricHilbert.hodgeGammaShiftLinear_bound line 136
11. def OAI.TamingCompatibility.GeometricHilbert.hodgeGammaShift line 161
12. lemma OAI.TamingCompatibility.GeometricHilbert.hodgeGammaTailAction_factor line 167
13. def OAI.TamingCompatibility.GeometricHilbert.HodgeSmoothingCover.gammaTailKernel line 202
14. lemma OAI.TamingCompatibility.GeometricHilbert.HodgeSmoothingCover.gammaTailKernel_continuous line 206
15. lemma OAI.TamingCompatibility.GeometricHilbert.HodgeSmoothingCover.gammaTailKernel_bound line 212
16. lemma OAI.TamingCompatibility.GeometricHilbert.HodgeSmoothingCover.gammaTailKernel_uniform line 222