OAI/Geometry/ProjectionBodies/SignCalculus.lean

GitHub source file

41 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PettyProjection.Spherical.softAbs line 9
  2. def OAI.PettyProjection.Spherical.softSign line 10
  3. def OAI.PettyProjection.Spherical.softSlope line 11
  4. lemma OAI.PettyProjection.Spherical.softAbs_pos line 13
  5. lemma OAI.PettyProjection.Spherical.softAbs_sq line 16
  6. lemma OAI.PettyProjection.Spherical.softAbs_contDiff line 19
  7. lemma OAI.PettyProjection.Spherical.softSign_contDiff line 22
  8. lemma OAI.PettyProjection.Spherical.softAbs_hasDerivAt line 25
  9. lemma OAI.PettyProjection.Spherical.softSign_hasDerivAt line 32
  10. lemma OAI.PettyProjection.Spherical.abs_le_softAbs line 40
  11. lemma OAI.PettyProjection.Spherical.softAbs_le line 45
  12. lemma OAI.PettyProjection.Spherical.abs_softSign_le line 52
  13. lemma OAI.PettyProjection.Spherical.abs_softCorrection_le line 56
  14. lemma OAI.PettyProjection.Spherical.real_sign_eq line 64
  15. lemma OAI.PettyProjection.Spherical.softAbs_tendsto line 71
  16. lemma OAI.PettyProjection.Spherical.softSign_tendsto line 79
  17. lemma OAI.PettyProjection.Spherical.softCorrection_tendsto line 87
  18. lemma OAI.PettyProjection.Spherical.casimir_linear line 105
  19. lemma OAI.PettyProjection.Spherical.sphereGradient_linear_inner line 111
  20. lemma OAI.PettyProjection.Spherical.mean_sphereGradient_inner line 118
  21. lemma OAI.PettyProjection.Spherical.sphereGradient_product_scalar_inner line 138
  22. lemma OAI.PettyProjection.Spherical.mean_weighted_gradient line 152
  23. lemma OAI.PettyProjection.Spherical.sign_measurable line 185
  24. lemma OAI.PettyProjection.Spherical.abs_sign_le line 190
  25. lemma OAI.PettyProjection.Spherical.sign_mul_self line 196
  26. lemma OAI.PettyProjection.Spherical.sign_weight_integrable line 203
  27. lemma OAI.PettyProjection.Spherical.mean_softSign_tendsto line 210
  28. lemma OAI.PettyProjection.Spherical.mean_softCorrection_tendsto line 226
  29. lemma OAI.PettyProjection.Spherical.mean_softAbs_tendsto line 248
  30. lemma OAI.PettyProjection.Spherical.mean_sign_gradient_tangent line 275
  31. lemma OAI.PettyProjection.Spherical.sphereGradient_scalar_inner line 311
  32. lemma OAI.PettyProjection.Spherical.mean_sign_gradient_radial line 321
  33. def OAI.PettyProjection.Spherical.signedPair line 362
  34. lemma OAI.PettyProjection.Spherical.signedPair_integrable line 366
  35. lemma OAI.PettyProjection.Spherical.signedPair_eq line 378
  36. lemma OAI.PettyProjection.Spherical.signedPair_eq_swap line 384
  37. lemma OAI.PettyProjection.Spherical.signedPair_symm line 391
  38. lemma OAI.PettyProjection.Spherical.signedPair_add_left line 400
  39. lemma OAI.PettyProjection.Spherical.signedPair_add_right line 407
  40. lemma OAI.PettyProjection.Spherical.signedPair_smul_left line 414
  41. lemma OAI.PettyProjection.Spherical.signedPair_smul_right line 420