OAI/Geometry/Riemannian/HarmonicCore/WarpingLimit.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.HarmonicCounterexample.tailPrimitive_tendsto line 17
  2. lemma OAI.HarmonicCounterexample.radialPrimitive_tendsto line 27
  3. lemma OAI.HarmonicCounterexample.sigma_tendsto line 33
  4. lemma OAI.HarmonicCounterexample.slope_tendsto line 38
  5. lemma OAI.HarmonicCounterexample.compactLoss_eventually_pos line 48
  6. lemma OAI.HarmonicCounterexample.warping_upper_tangent line 59
  7. lemma OAI.HarmonicCounterexample.warping_ratio_tendsto line 75
  8. lemma OAI.HarmonicCounterexample.b_eq_div line 101
  9. lemma OAI.HarmonicCounterexample.b_bounds line 104
  10. lemma OAI.HarmonicCounterexample.b_tendsto line 113
  11. lemma OAI.HarmonicCounterexample.b_smooth line 118
  12. lemma OAI.HarmonicCounterexample.b_hasDerivAt line 122
  13. lemma OAI.HarmonicCounterexample.b_deriv line 132
  14. lemma OAI.HarmonicCounterexample.b_first_equation line 137
  15. lemma OAI.HarmonicCounterexample.b_deriv_hasDerivAt line 142
  16. lemma OAI.HarmonicCounterexample.b_second_deriv line 150
  17. lemma OAI.HarmonicCounterexample.slope_exp_exact line 156
  18. lemma OAI.HarmonicCounterexample.b_first_equation_tail line 167
  19. lemma OAI.HarmonicCounterexample.b_second_equation line 171
  20. lemma OAI.HarmonicCounterexample.b_deriv_bounded line 182
  21. lemma OAI.HarmonicCounterexample.slope_le_b line 190
  22. lemma OAI.HarmonicCounterexample.b_deriv_nonpos line 199