OAI/Geometry/Riemannian/HarmonicCore/PolarDensity.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.HarmonicCounterexample.Main.det_radial_update line 18
  2. lemma OAI.HarmonicCounterexample.Main.det_polar_algebra line 56
  3. lemma OAI.HarmonicCounterexample.Main.polarMetric_distance_origin line 73
  4. lemma OAI.HarmonicCounterexample.Main.polarMetric_density line 84
  5. lemma OAI.HarmonicCounterexample.Main.polarMetric_density_bounds line 101
  6. lemma OAI.HarmonicCounterexample.Main.SmoothMetric3.density_continuous line 122
  7. lemma OAI.HarmonicCounterexample.Main.SmoothMetric3.volumeMeasure_apply line 130