OAI/Geometry/Riemannian/HarmonicCore/Warping.lean

GitHub source file

37 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.HarmonicCounterexample.tailDensity_zero line 17
  2. lemma OAI.HarmonicCounterexample.tailDensity_nonneg line 25
  3. lemma OAI.HarmonicCounterexample.tailDensity_le line 31
  4. lemma OAI.HarmonicCounterexample.tailDensity_exact line 35
  5. lemma OAI.HarmonicCounterexample.tailDensity_smooth line 42
  6. lemma OAI.HarmonicCounterexample.tailDensity_integrable line 53
  7. lemma OAI.HarmonicCounterexample.tailMass_nonneg line 62
  8. lemma OAI.HarmonicCounterexample.tailMass_bound line 65
  9. lemma OAI.HarmonicCounterexample.tailPrimitive_hasDerivAt line 75
  10. lemma OAI.HarmonicCounterexample.tailPrimitive_deriv line 82
  11. lemma OAI.HarmonicCounterexample.tailPrimitive_smooth line 87
  12. lemma OAI.HarmonicCounterexample.tailPrimitive_zero line 93
  13. lemma OAI.HarmonicCounterexample.tailPrimitive_nonneg line 103
  14. lemma OAI.HarmonicCounterexample.tail_decomposition line 109
  15. lemma OAI.HarmonicCounterexample.tailPrimitive_le_mass line 120
  16. lemma OAI.HarmonicCounterexample.tailPrimitive_exact line 129
  17. lemma OAI.HarmonicCounterexample.radialPrimitive_zero line 143
  18. lemma OAI.HarmonicCounterexample.radialPrimitive_smooth line 151
  19. lemma OAI.HarmonicCounterexample.radialPrimitive_nonneg line 167
  20. lemma OAI.HarmonicCounterexample.radialPrimitive_le_mass line 174
  21. lemma OAI.HarmonicCounterexample.slope_smooth line 181
  22. lemma OAI.HarmonicCounterexample.slope_le_one line 186
  23. lemma OAI.HarmonicCounterexample.a_le_slope line 193
  24. lemma OAI.HarmonicCounterexample.slope_one_near_zero line 200
  25. lemma OAI.HarmonicCounterexample.warping_hasDerivAt line 204
  26. lemma OAI.HarmonicCounterexample.warping_deriv line 211
  27. lemma OAI.HarmonicCounterexample.warping_smooth line 216
  28. lemma OAI.HarmonicCounterexample.warping_eq_id_near_zero line 221
  29. def OAI.HarmonicCounterexample.radialDensity line 230
  30. lemma OAI.HarmonicCounterexample.radialPrimitive_hasDerivAt_gt_one line 233
  31. lemma OAI.HarmonicCounterexample.radialPrimitive_hasDerivAt line 242
  32. lemma OAI.HarmonicCounterexample.radialDensity_nonneg line 263
  33. lemma OAI.HarmonicCounterexample.slope_hasDerivAt line 270
  34. lemma OAI.HarmonicCounterexample.warping_second_deriv line 279
  35. lemma OAI.HarmonicCounterexample.slope_antitone line 285
  36. lemma OAI.HarmonicCounterexample.warping_bounds line 294
  37. lemma OAI.HarmonicCounterexample.warping_pos line 306