OAI/Geometry/ProjectionBodies/SphericalGap.lean

GitHub source file

42 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PettyProjection.Spherical.restrictContinuous line 12
2. lemma OAI.PettyProjection.Spherical.polynomialFunction_odd line 15
3. lemma OAI.PettyProjection.Spherical.mean_even_mul_odd line 21
4. lemma OAI.PettyProjection.Spherical.projection_odd_zero line 37
5. def OAI.PettyProjection.Spherical.harmonicRepresentative line 48

   Source documentation

   A chosen true polynomial representative of a harmonic L² vector.

   def harmonicRepresentative {n d : ℕ} [NeZero n] (v : harmonicSpace n d) : MvPolynomial (Fin n) ℝ :=
   …

   Mentions: OAI.PettyProjection.Spherical.harmonicSpace

6. lemma OAI.PettyProjection.Spherical.harmonicRepresentative_homogeneous line 51
7. lemma OAI.PettyProjection.Spherical.harmonicRepresentative_laplace line 55
8. lemma OAI.PettyProjection.Spherical.harmonicRepresentative_toH line 59
9. lemma OAI.PettyProjection.Spherical.inner_projection_self line 63
10. lemma OAI.PettyProjection.Spherical.energy_harmonicRepresentative_right line 69
11. lemma OAI.PettyProjection.Spherical.sum_inner_projection line 81
12. lemma OAI.PettyProjection.Spherical.energy_bessel_finset line 99

    Source documentation

    The finite Bessel bound, established by subtracting a finite harmonic polynomial sum. No infinite series is differentiated.

    lemma energy_bessel_finset {n : ℕ} (hn : 2 ≤ n) [NeZero n]
        {f : Space n → ℝ} (hf : ContDiff ℝ 1 f) (s : Finset ℕ) :
        ∑ d ∈ s, eigenvalue n d * ‖(harmonicSpace n d).starProjection
          (toH n (restrictContinuous f hf.continuous))‖ ^ 2 ≤ energy f f := by
    …

    Mentions: OAI.PettyProjection.Spherical.Space, OAI.PettyProjection.Spherical.eigenvalue, OAI.PettyProjection.Spherical.harmonicSpace, OAI.PettyProjection.Spherical.toH, OAI.PettyProjection.Spherical.restrictContinuous, OAI.PettyProjection.Spherical.energy

13. lemma OAI.PettyProjection.Spherical.eigenvalue_nonneg line 138
14. lemma OAI.PettyProjection.Spherical.eigenvalue_four_le line 144
15. lemma OAI.PettyProjection.Spherical.Q_zero_of_mem_lowSpace line 152
16. lemma OAI.PettyProjection.Spherical.projection_zero_mem_lowSpace line 156
17. lemma OAI.PettyProjection.Spherical.projection_inner_ne line 162
18. lemma OAI.PettyProjection.Spherical.norm_Q_sq_le_remainder line 171
19. lemma OAI.PettyProjection.Spherical.energy_spectral_lower line 190
20. def OAI.PettyProjection.Spherical.variance line 230

    Source documentation

    The mean-subtracted variance in the probability normalization.

    def variance {n : ℕ} (f : Sphere n → ℝ) : ℝ := mean (fun u => f u ^ 2) - (mean f) ^ 2

    Mentions: OAI.PettyProjection.Spherical.Sphere, OAI.PettyProjection.Spherical.mean

21. lemma OAI.PettyProjection.Spherical.even_spectral_gap line 235

    Source documentation

    The genuine degree-two-removed even spherical spectral gap, under the canonical probability measure. energy is the integrated squared tangential derivative represented by the coordinate rotation generators.

    lemma even_spectral_gap {n : ℕ} (hn : 2 ≤ n) [NeZero n]
        {f : Space n → ℝ} (hf : ContDiff ℝ 1 f) (heven : Function.Even f) :
        (2 * n : ℝ) * variance (fun u : Sphere n => f u) + (2 * n + 8 : ℝ) *
          ‖Q n (toH n (restrictContinuous f hf.continuous))‖ ^ 2 ≤ energy f f := by
    …

    Mentions: OAI.PettyProjection.Spherical.Space, OAI.PettyProjection.Spherical.variance, OAI.PettyProjection.Spherical.Sphere, OAI.PettyProjection.Spherical.Q, OAI.PettyProjection.Spherical.toH, OAI.PettyProjection.Spherical.restrictContinuous, OAI.PettyProjection.Spherical.energy

22. lemma OAI.PettyProjection.Spherical.line_convex line 265
23. lemma OAI.PettyProjection.Spherical.line_hasDerivAt line 277
24. lemma OAI.PettyProjection.Spherical.line_second_hasDerivAt line 283
25. lemma OAI.PettyProjection.Spherical.hessian_nonneg_of_convex line 301
26. lemma OAI.PettyProjection.Spherical.rotDeriv_rotDeriv line 316
27. lemma OAI.PettyProjection.Spherical.generator_square_coord line 327
28. lemma OAI.PettyProjection.Spherical.sum_generator_square line 334
29. lemma OAI.PettyProjection.Spherical.convex_casimir_lower line 344
30. lemma OAI.PettyProjection.Spherical.seminorm_continuous line 366
31. lemma OAI.PettyProjection.Spherical.seminorm_lipschitz line 369
32. def OAI.PettyProjection.Spherical.normSmooth line 376
33. lemma OAI.PettyProjection.Spherical.normSmooth_contDiff line 379
34. lemma OAI.PettyProjection.Spherical.normSmooth_even line 384
35. lemma OAI.PettyProjection.Spherical.normSmooth_integrable line 390
36. lemma OAI.PettyProjection.Spherical.normSmooth_convex line 395
37. lemma OAI.PettyProjection.Spherical.normSmooth_dist_le line 417
38. lemma OAI.PettyProjection.Spherical.convex_radial_bounds line 424
39. lemma OAI.PettyProjection.Spherical.normSmooth_radial_dist_le line 438
40. lemma OAI.PettyProjection.Spherical.sphere_ae_of_radial line 458
41. lemma OAI.PettyProjection.Spherical.seminorm_ae_differentiable_sphere line 488
42. lemma OAI.PettyProjection.Spherical.normSmooth_lipschitz line 503