OAI/Geometry/ProjectionBodies/CosineCalculus.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PettyProjection.Spherical.posPower line 10

    Source documentation

    Positive part to a natural power; the endpoint is fixed to zero.

    def posPower (r : ℕ) (x : ℝ) : ℝ := if 0 < x then x^r else 0
  2. lemma OAI.PettyProjection.Spherical.posPower_hasDerivAt line 12
  3. lemma OAI.PettyProjection.Spherical.posPower_contDiff_one line 24
  4. lemma OAI.PettyProjection.Spherical.posPower_contDiff_two line 36
  5. lemma OAI.PettyProjection.Spherical.abs_pow_posPower line 46
  6. lemma OAI.PettyProjection.Spherical.abs_pow_contDiff_two line 53
  7. lemma OAI.PettyProjection.Spherical.abs_pow_hasDerivAt line 59
  8. lemma OAI.PettyProjection.Spherical.abs_pow_second_deriv line 76
  9. lemma OAI.PettyProjection.Spherical.inner_generator line 105
  10. lemma OAI.PettyProjection.Spherical.sum_inner_generator_sq line 110
  11. lemma OAI.PettyProjection.Spherical.rotDeriv_scalar_linear line 126
  12. lemma OAI.PettyProjection.Spherical.rotDeriv_scalar_linear_twice line 133
  13. lemma OAI.PettyProjection.Spherical.casimir_scalar_inner line 149
  14. lemma OAI.PettyProjection.Spherical.posPower_mul line 163
  15. lemma OAI.PettyProjection.Spherical.posPower_mul_sq line 167
  16. lemma OAI.PettyProjection.Spherical.casimir_posPower_inner line 171
  17. lemma OAI.PettyProjection.Spherical.mean_casimir_comm line 194
  18. lemma OAI.PettyProjection.Spherical.sum_inner_generator_mul line 209
  19. def OAI.PettyProjection.Spherical.sphereGradient line 225

    Source documentation

    Genuine tangential gradient on the unit sphere, expressed ambiently.

    def sphereGradient {n : ℕ} (f : Space n → ℝ) (x : Space n) : Space n :=
…

    Mentions: OAI.PettyProjection.Spherical.Space

  20. lemma OAI.PettyProjection.Spherical.continuous_gradient_of_contDiff line 228
  21. lemma OAI.PettyProjection.Spherical.sphereGradient_continuous line 232
  22. lemma OAI.PettyProjection.Spherical.sphereGradient_inner line 237
  23. lemma OAI.PettyProjection.Spherical.sphereGradient_tangent line 241
  24. lemma OAI.PettyProjection.Spherical.sum_rotDeriv_inner line 246
  25. lemma OAI.PettyProjection.Spherical.mean_gradient_casimir line 254