OAI/Geometry/ProjectionBodies/PositionMatrices.lean

GitHub source file

47 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.PettyProjection.RelativeGauge.NonzeroMap line 13
2. def OAI.PettyProjection.RelativeGauge.optimizer line 15
3. lemma OAI.PettyProjection.RelativeGauge.optimizer_normalized line 20
4. lemma OAI.PettyProjection.RelativeGauge.optimizer_minimal line 25
5. def OAI.PettyProjection.RelativeGauge.optimizerSphere line 31
6. theorem OAI.PettyProjection.RelativeGauge.optimizerSphere_continuous line 39

   Source documentation

   Rank-continuity of the actual canonical variational optimizer. The codomain carries the uniform norm on the entire ambient sphere.

   theorem optimizerSphere_continuous (hμ : Integrable (fun x : Space n => ‖x‖) μ)
       (hq : ∀ x : Space n,x≠0 → 0< cosineSeminorm μ hμ x) (b : Bool) :
       Continuous (optimizerSphere hμ hq b) := by
   …

   Mentions: OAI.PettyProjection.Space, OAI.PettyProjection.cosineSeminorm, OAI.PettyProjection.RelativeGauge.optimizerSphere

7. lemma OAI.PettyProjection.gaussian_real_second_moment line 65
8. lemma OAI.PettyProjection.seminorm_add_kernel line 78
9. lemma OAI.PettyProjection.gaussian_shadow_norm line 87
10. lemma OAI.PettyProjection.gaussian_kernel_moment line 95

    Source documentation

    Genuine Gaussian independence in a seminorm kernel, proved by the measure-preserving orthogonal coordinate map and Fubini product integrals.

    lemma gaussian_kernel_moment {n : ℕ} (g : Seminorm ℝ (Space n)) (k : ℕ)
        (e : Sphere n) (he : g e=0) :
        (∫ x : Space n,g x^k*⟪(e:Space n),x⟫^2*Real.exp (-(‖x‖^2)))=
          (1/2:ℝ)*(∫ x : Space n,g x^k*Real.exp (-(‖x‖^2))) := by
    …

    Mentions: OAI.PettyProjection.Space

11. theorem OAI.PettyProjection.sphere_kernel_moment line 130

    Source documentation

    The boundary moment ratio, for every seminorm and every natural homogeneity degree, including all singular and nonsmooth cases.

    theorem sphere_kernel_moment {n : ℕ} [NeZero n] (g : Seminorm ℝ (Space n)) (k : ℕ)
        (e : Sphere n) (he : g e=0) :
        ((n:ℝ)+k)*mean (fun u : Sphere n => g u^k*⟪(e:Space n),(u:Space n)⟫^2)=
          mean (fun u : Sphere n => g u^k) := by
    …

    Mentions: OAI.PettyProjection.Space

12. abbrev OAI.PettyProjection.Position.Mat line 161
13. def OAI.PettyProjection.Position.matrix line 163
14. def OAI.PettyProjection.Position.op line 164
15. def OAI.PettyProjection.Position.tr line 165
16. def OAI.PettyProjection.Position.quad line 166
17. def OAI.PettyProjection.Position.Symmetric line 167
18. def OAI.PettyProjection.Position.PSD line 168
19. def OAI.PettyProjection.Position.domain line 169
20. lemma OAI.PettyProjection.Position.op_apply line 171
21. lemma OAI.PettyProjection.Position.quad_eq line 172
22. lemma OAI.PettyProjection.Position.op_continuous line 177
23. lemma OAI.PettyProjection.Position.quad_continuous line 183
24. lemma OAI.PettyProjection.Position.tr_continuous line 185
25. lemma OAI.PettyProjection.Position.quad_add line 188
26. lemma OAI.PettyProjection.Position.quad_smul line 190
27. lemma OAI.PettyProjection.Position.quad_sub line 192
28. lemma OAI.PettyProjection.Position.symmetric_op line 194
29. lemma OAI.PettyProjection.Position.op_kernel_of_quad_zero line 198
30. lemma OAI.PettyProjection.Position.symmetric_closed line 225
31. lemma OAI.PettyProjection.Position.quad_nonneg_closed line 234
32. lemma OAI.PettyProjection.Position.psd_closed line 238
33. lemma OAI.PettyProjection.Position.domain_closed line 245
34. lemma OAI.PettyProjection.Position.domain_convex line 247
35. lemma OAI.PettyProjection.Position.quad_basis line 261
36. lemma OAI.PettyProjection.Position.quad_basis_add line 263
37. lemma OAI.PettyProjection.Position.domain_entry_bound line 268
38. lemma OAI.PettyProjection.Position.domain_compact line 277
39. lemma OAI.PettyProjection.Position.domain_nonempty line 291
40. lemma OAI.PettyProjection.Position.domain_range_ne_bot line 305
41. def OAI.PettyProjection.Position.identity line 324
42. def OAI.PettyProjection.Position.momentField line 325
43. lemma OAI.PettyProjection.Position.mean_power_pos line 329
44. lemma OAI.PettyProjection.Position.field_symmetric line 340
45. lemma OAI.PettyProjection.Position.field_trace line 347
46. lemma OAI.PettyProjection.Position.field_quad line 366
47. lemma OAI.PettyProjection.Position.field_kernel line 406