OAI/Geometry/Riemannian/HarmonicCore/PolarMetric.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.HarmonicCounterexample.Main.AngularTensor line 18
2. def OAI.HarmonicCounterexample.Main.radialProjection line 30
3. lemma OAI.HarmonicCounterexample.Main.radialProjection_posSemidef line 35
4. def OAI.HarmonicCounterexample.Main.polarCoeff line 41
5. lemma OAI.HarmonicCounterexample.Main.polarCoeff_core line 48
6. lemma OAI.HarmonicCounterexample.Main.polarCoeff_positive line 60
7. lemma OAI.HarmonicCounterexample.Main.radialProjection_smooth line 76
8. lemma OAI.HarmonicCounterexample.Main.polarCoeff_smooth line 86
9. def OAI.HarmonicCounterexample.Main.polarMetric line 111
10. lemma OAI.HarmonicCounterexample.Main.polarMetric_euclidean line 120