OAI/Geometry/TamingCompatibility/Concentration/ConcentrationDifferential.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.concentrationPatch_differential_chart line 22
2. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.concentrationPatch_differential_zero_off line 41
3. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.concentrationPatch_wedge_zero_off line 55
4. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.concentrationPatch_wedge_chart line 65
5. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.concentration_theta_bound line 82
6. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.concentration_partition_derivative_bound line 90
7. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.concentrationPatch_tangential_bound line 117
8. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.concentrationPatch_coefficient_bound line 188