OAI/Geometry/ProjectionBodies/CosineSpectrum.lean

GitHub source file

37 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.PettyProjection.Spherical.posPower_eq_max_pow line 10
2. def OAI.PettyProjection.Spherical.higherKernel line 17

   Source documentation

   Positive-hemisphere power kernel, including the constant zeroth power.

   def higherKernel {n : ℕ} (r : ℕ) (u : Sphere n) (f : Sphere n → ℝ) : ℝ :=
   …

   Mentions: OAI.PettyProjection.Spherical.Sphere

3. lemma OAI.PettyProjection.Spherical.higherKernel_const_pos line 20
4. lemma OAI.PettyProjection.Spherical.higherKernel_recurrence line 29
5. lemma OAI.PettyProjection.Spherical.higherKernel_const_recurrence line 58
6. lemma OAI.PettyProjection.Spherical.higherKernel_peak line 67
7. def OAI.PettyProjection.Spherical.higherFactor line 94

   Source documentation

   Normalized multiplier of the positive-power kernel on degree 2*j.

   def higherFactor (n j : ℕ) (s : ℝ) : ℝ :=
   …

8. lemma OAI.PettyProjection.Spherical.higherFactor_zero line 97
9. lemma OAI.PettyProjection.Spherical.higherFactor_succ line 100
10. lemma OAI.PettyProjection.Spherical.higherFactor_odd_ne_zero line 104
11. lemma OAI.PettyProjection.Spherical.higherFactor_step line 117
12. lemma OAI.PettyProjection.Spherical.higherFactor_tendsto line 132
13. lemma OAI.PettyProjection.Spherical.eigenvalue_sub_even line 153
14. lemma OAI.PettyProjection.Spherical.eigenvalue_odd_sub_even_ne_zero line 159
15. lemma OAI.PettyProjection.Spherical.higherKernel_normalized_recurrence line 172
16. lemma OAI.PettyProjection.Spherical.higherKernel_eigenfunction line 185
17. lemma OAI.PettyProjection.Spherical.higherKernel_harmonic line 232
18. def OAI.PettyProjection.Spherical.pole line 248
19. lemma OAI.PettyProjection.Spherical.higherKernel_const_rotation line 251
20. lemma OAI.PettyProjection.Spherical.higherKernel_const_independent line 261
21. def OAI.PettyProjection.Spherical.cosineConstant line 270

    Source documentation

    The true normalized cosine kernel's constant, not an assumed multiplier.

    def cosineConstant (n : ℕ) [NeZero n] : ℝ :=
    …

22. lemma OAI.PettyProjection.Spherical.cosineConstant_pos line 273
23. lemma OAI.PettyProjection.Spherical.mean_pos_inner_even line 276
24. lemma OAI.PettyProjection.Spherical.mean_abs_inner line 301
25. def OAI.PettyProjection.Spherical.cosine line 307

    Source documentation

    The actual cosine integral, with its constant fixed geometrically.

    def cosine {n : ℕ} [NeZero n] (f : Sphere n → ℝ) (u : Sphere n) : ℝ :=
    …

    Mentions: OAI.PettyProjection.Spherical.Sphere

26. lemma OAI.PettyProjection.Spherical.cosine_continuous line 310
27. lemma OAI.PettyProjection.Spherical.cosine_const line 318
28. lemma OAI.PettyProjection.Spherical.polynomialFunction_even line 325
29. lemma OAI.PettyProjection.Spherical.cosine_harmonic line 331
30. def OAI.PettyProjection.Spherical.cosineMap line 348
31. lemma OAI.PettyProjection.Spherical.cosine_selfadj line 351
32. lemma OAI.PettyProjection.Spherical.mean_cosine line 369
33. lemma OAI.PettyProjection.Spherical.cosine_neg line 374
34. lemma OAI.PettyProjection.Spherical.mean_sphere_even_mul_odd line 383
35. lemma OAI.PettyProjection.Spherical.cosine_harmonic_odd line 400
36. lemma OAI.PettyProjection.Spherical.cosine_projection_even line 407
37. lemma OAI.PettyProjection.Spherical.cosine_projection_odd line 429