OAI/Geometry/TamingCompatibility/Concentration/ConcentrationGlobalError.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.globalConcentration_wedge line 28
2. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.globalConcentration_current_control line 38
3. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.globalConcentration_Q_control line 82
4. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.concentrationPatch_integrable line 145
5. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.globalConcentration_integrable line 154
6. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.concentrationPatch_volume_growth line 163
7. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.globalConcentration_volume_growth line 187
8. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.globalConcentration_volume_limit line 199