OAI/Geometry/TamingCompatibility/Concentration/HodgeCompactResidual.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.TamingCompatibility.GeometricHilbert.UniformJets.compact_normal_bounds line 24
2. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.gaugedFirst_center line 67
3. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.normalGauge_unitary line 78
4. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.compact_actual_coefficients line 95
5. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.pulledA_scalar_at line 165
6. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.actual_normal_residual_bound line 194
7. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.compact_actual_residual line 283