OAI/Geometry/TamingCompatibility/DifferentialForms/HermitianUnitMetric.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.TamingCompatibility.ManifoldVolume.chartMetric_compact_bounds line 22
2. lemma OAI.TamingCompatibility.ManifoldVolume.chartMetric_unit_norm_bounds line 30
3. lemma OAI.TamingCompatibility.ManifoldVolume.chartMetric_hermitian line 43
4. lemma OAI.TamingCompatibility.ManifoldVolume.form_unit_line_bound line 51
5. lemma OAI.TamingCompatibility.ManifoldVolume.inverse_coordinates_eval line 69
6. lemma OAI.TamingCompatibility.ManifoldVolume.unitEvaluation_lower_of_chart line 84
7. theorem OAI.TamingCompatibility.GeometricHilbert.Hermitian.logForm_far_uniform line 145
8. theorem OAI.TamingCompatibility.GeometricHilbert.Hermitian.sqrtForm_far_uniform line 192