OAI/Geometry/Riemannian/HarmonicCore/WarpProfiles.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.HarmonicCounterexample.a line 18
  2. def OAI.HarmonicCounterexample.theta line 20
  3. def OAI.HarmonicCounterexample.sigma line 22
  4. def OAI.HarmonicCounterexample.beta line 24
  5. lemma OAI.HarmonicCounterexample.theta_smooth line 26
  6. lemma OAI.HarmonicCounterexample.theta_nonneg line 29
  7. lemma OAI.HarmonicCounterexample.theta_le_one line 30
  8. lemma OAI.HarmonicCounterexample.theta_zero line 32
  9. lemma OAI.HarmonicCounterexample.theta_one line 36
  10. lemma OAI.HarmonicCounterexample.sigma_smooth line 40
  11. lemma OAI.HarmonicCounterexample.sigma_nonneg line 43
  12. lemma OAI.HarmonicCounterexample.sigma_le_one line 44
  13. lemma OAI.HarmonicCounterexample.sigma_zero line 46
  14. lemma OAI.HarmonicCounterexample.sigma_one line 50
  15. lemma OAI.HarmonicCounterexample.sigma_monotone line 54
  16. lemma OAI.HarmonicCounterexample.beta_smooth line 58
  17. lemma OAI.HarmonicCounterexample.beta_nonneg line 61
  18. lemma OAI.HarmonicCounterexample.beta_zero_left line 64
  19. lemma OAI.HarmonicCounterexample.beta_zero_right line 71
  20. lemma OAI.HarmonicCounterexample.beta_support line 78
  21. lemma OAI.HarmonicCounterexample.beta_compactSupport line 86
  22. lemma OAI.HarmonicCounterexample.beta_normalization line 89
  23. def OAI.HarmonicCounterexample.tailDensity line 102
  24. def OAI.HarmonicCounterexample.tailMass line 104
  25. def OAI.HarmonicCounterexample.compactLoss line 106
  26. def OAI.HarmonicCounterexample.tailPrimitive line 108
  27. def OAI.HarmonicCounterexample.radialPrimitive line 110
  28. def OAI.HarmonicCounterexample.slope line 113
  29. def OAI.HarmonicCounterexample.warping line 116
  30. def OAI.HarmonicCounterexample.b line 118