OAI/Geometry/Riemannian/HarmonicCore/RadialDistance.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.HarmonicCounterexample.Main.SmoothMetric3.inner_symm line 18
  2. lemma OAI.HarmonicCounterexample.Main.SmoothMetric3.inner_sub_left line 30
  3. lemma OAI.HarmonicCounterexample.Main.SmoothMetric3.inner_smul_left line 36
  4. lemma OAI.HarmonicCounterexample.Main.SmoothMetric3.inner_sub_right line 47
  5. lemma OAI.HarmonicCounterexample.Main.SmoothMetric3.inner_smul_right line 54
  6. lemma OAI.HarmonicCounterexample.Main.SmoothMetric3.inner_radial line 60
  7. lemma OAI.HarmonicCounterexample.Main.SmoothMetric3.radial_cauchy_sq line 67
  8. lemma OAI.HarmonicCounterexample.Main.SmoothMetric3.regularized_radius_deriv_bound line 84
  9. lemma OAI.HarmonicCounterexample.Main.SmoothMetric3.radius_change_le_pathLength line 112
  10. lemma OAI.HarmonicCounterexample.Main.SmoothMetric3.radius_change_le_distance line 144
  11. lemma OAI.HarmonicCounterexample.Main.SmoothMetric3.radial_straight_length line 153
  12. lemma OAI.HarmonicCounterexample.Main.SmoothMetric3.distance_origin_eq_norm line 171