OAI/Geometry/TamingCompatibility/Hodge/HodgeGlobalParametrix.lean
13 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.assembleline 22 - def
OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.globalLeadingline 26 - def
OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.globalResidualline 27 - lemma
OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.physicalCompact_targetline 30 - lemma
OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.assemble_continuousOnline 36 - lemma
OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.globalLeading_continuousOnline 59 - lemma
OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.globalResidual_continuousOnline 67 - lemma
OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.assemble_measurableline 77 - lemma
OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.globalLeading_measurableline 96 - lemma
OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.globalResidual_measurableline 104 - lemma
OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.frameEncode_manifoldTestline 130 - lemma
OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.leadingSlice_domain_allline 162 - lemma
OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.residualSlice_domain_allline 176