OAI/Geometry/ProjectionBodies/SeminormBounds.lean

GitHub source file

43 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.PettyProjection.Spherical.seminorm_le_max_norm line 12
2. lemma OAI.PettyProjection.Spherical.seminorm_coordinate_minorant line 28

   Source documentation

   Exact coordinate minorant used for logarithmic coercivity and continuous extension to singular matrix ranks.

   lemma seminorm_coordinate_minorant {n : ℕ} [NeZero n] (g : Seminorm ℝ (Space n))
       (hg : g ≠ 0) : ∃ (R : ℝ) (e : Sphere n), 0 < R ∧
         (∀ u : Sphere n, g u ≤ R) ∧
         (∀ x : Space n, R*|⟪x,(e:Space n)⟫| ≤ g x) := by
   …

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

3. lemma OAI.PettyProjection.Spherical.intervalIntegrable_abs_rpow line 87
4. lemma OAI.PettyProjection.Spherical.inner_rpow_integrable_ball line 97
5. lemma OAI.PettyProjection.Spherical.sphere_integrable_of_homogeneous line 131
6. lemma OAI.PettyProjection.Spherical.inner_rpow_integrable_sphere line 168
7. lemma OAI.PettyProjection.Spherical.log_sq_le_negative_rpow line 174
8. lemma OAI.PettyProjection.Spherical.log_inner_sq_integrable line 188
9. lemma OAI.PettyProjection.Spherical.log_inner_integrable line 200
10. lemma OAI.PettyProjection.Spherical.inner_ne_zero_ae_sphere line 218
11. lemma OAI.PettyProjection.Spherical.mean_inner_independent line 240
12. lemma OAI.PettyProjection.Spherical.seminorm_pos_ae_sphere line 250
13. lemma OAI.PettyProjection.Spherical.log_sq_coercive_bound line 256
14. lemma OAI.PettyProjection.Spherical.seminorm_log_sq_integrable line 273
15. lemma OAI.PettyProjection.Spherical.seminorm_log_integrable line 284
16. lemma OAI.PettyProjection.Spherical.seminorm_log_coercivity line 293
17. lemma OAI.PettyProjection.Spherical.unifIntegrable_of_sq_bound line 319
18. lemma OAI.PettyProjection.Spherical.tendsto_integral_of_sq_bound line 359
19. lemma OAI.PettyProjection.Spherical.seminorm_log_sq_bound line 370
20. lemma OAI.PettyProjection.Spherical.seminorm_log_integral_tendsto line 409
21. lemma OAI.PettyProjection.Spherical.seminorm_lipschitz_of_sphere_bound line 441
22. def OAI.PettyProjection.Spherical.radialExtension line 449
23. lemma OAI.PettyProjection.Spherical.radialExtension_sphere line 455
24. lemma OAI.PettyProjection.Spherical.radialExtension_seminorm line 460
25. lemma OAI.PettyProjection.Spherical.radialExtension_tendsto line 468
26. theorem OAI.PettyProjection.Spherical.bounded_seminorm_subsequence line 481

    Source documentation

    Uniform sphere compactness of bounded seminorms, including all singular limits. The limiting algebraic object is proved to be a seminorm.

    theorem bounded_seminorm_subsequence {n : ℕ} (g : ℕ → Seminorm ℝ (Space n))
        {R : ℝ≥0} (hR : ∀ i (u : Sphere n),g i u≤R) :
        ∃ f : Seminorm ℝ (Space n), ∃ φ : ℕ → ℕ, StrictMono φ ∧
          TendstoUniformly (fun i (u : Sphere n) => g (φ i) u) (fun u => f u) atTop ∧
          (∀ x,Tendsto (fun i => g (φ i) x) atTop (𝓝 (f x))) := by
    …

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

27. def OAI.PettyProjection.seminormUnit line 529

    Source documentation

    Closed unit set of the actual seminorm. It is allowed to be a cylinder.

    def seminormUnit {n : ℕ} (g : Seminorm ℝ (Space n)) : Set (Space n) := {x | g x≤1}

    Mentions: OAI.PettyProjection.Space

28. lemma OAI.PettyProjection.seminormUnit_zero line 531
29. lemma OAI.PettyProjection.seminormUnit_closed line 534
30. lemma OAI.PettyProjection.seminormUnit_convex line 537
31. lemma OAI.PettyProjection.seminormUnit_balanced line 540
32. lemma OAI.PettyProjection.seminormUnit_nhds line 543
33. lemma OAI.PettyProjection.gauge_seminormUnit line 547
34. lemma OAI.PettyProjection.seminormUnit_compact line 564
35. lemma OAI.PettyProjection.seminorm_pos_uniform line 572
36. lemma OAI.PettyProjection.integrable_abs_inner line 598
37. def OAI.PettyProjection.cosineSeminorm line 605

    Source documentation

    The actual cosine-transform norm furnished by a spanning measure.

    def cosineSeminorm {n : ℕ} (μ : Measure (Space n))
        (hμ : Integrable (fun x : Space n => ‖x‖) μ) : Seminorm ℝ (Space n) :=
    …

    Mentions: OAI.PettyProjection.Space

38. lemma OAI.PettyProjection.support_integrable line 619
39. lemma OAI.PettyProjection.abs_inner_le_support line 630
40. lemma OAI.PettyProjection.cosine_le_functional line 640
41. lemma OAI.PettyProjection.functional_smul line 647
42. lemma OAI.PettyProjection.functional_add line 654
43. lemma OAI.PettyProjection.functional_nonneg line 663