OAI/Geometry/TamingCompatibility/Hodge/HodgeKernelChartGaussian.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.weight_of_dist_bound line 15
2. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.push_weighted_gaussian line 31
3. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.push_continuous line 78
4. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.push_gaussian_row line 95
5. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.push_gaussian_col line 131