OAI/Geometry/TamingCompatibility/Hodge/HodgeErrorInitial.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.kernelWeakAction_bound_of_col line 24
2. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.globalError_weak_initial line 44
3. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.globalError_weak_initial_of_bounds line 90
4. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.globalCandidate_L2_realization line 118