OAI/Geometry/TamingCompatibility/Concentration/HodgeResidualFamily.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.TamingCompatibility.GeometricHilbert.NormalHeatResidual.residual_family_smooth line 19
2. lemma OAI.TamingCompatibility.GeometricHilbert.NormalHeatResidual.cutoff_residual_eq_zero line 58
3. lemma OAI.TamingCompatibility.GeometricHilbert.NormalHeatResidual.compact_cutoff_matrix line 74
4. def OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.residualCoordinate line 121
5. def OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.residualPatch line 129
6. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.residualCoordinate_support line 135
7. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.residualCoordinate_smooth line 149
8. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.residualMatrix_gaussian line 164
9. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.norm_smul_comp_le line 192
10. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.residualCoordinate_gaussian line 201