OAI/Geometry/TamingCompatibility/Hodge/HodgeGaussianSchur.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.TamingCompatibility.GeometricHilbert.FlatHeat.polynomial_bound line 15
2. lemma OAI.TamingCompatibility.GeometricHilbert.FlatHeat.weighted_heat_bound line 28
3. lemma OAI.TamingCompatibility.GeometricHilbert.FlatHeat.gaussian_weighted_schur line 51
4. def OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.coordinateMatrix line 120
5. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.coordinateMatrix_support line 125
6. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.coordinateMatrix_joint_smooth line 132
7. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.coordinateMatrix_uniform_bound line 155
8. def OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.leadingMatrix line 184
9. def OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.residualMatrix line 187
10. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.leadingMatrix_smooth line 191
11. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.residualMatrix_smooth line 198
12. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.leadingMatrix_gaussian line 205
13. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.residualFrameMatrix_gaussian line 215