OAI/Geometry/TamingCompatibility/Concentration/HodgeResidualSlices.lean
8 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.ParametrixData.cutoffResidualline 31 - lemma
OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.ParametrixData.cutoffResidual_zero_offline 44 - def
OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.residualSliceline 50 - lemma
OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.residualSlice_smoothline 54 - lemma
OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.residualSlice_normalline 62 - lemma
OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.residualSlice_tsupportline 74 - lemma
OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.residualSlice_compactline 110 - lemma
OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.residualSlice_domainline 117