OAI/Geometry/ProjectionBodies/RelativeGauges.lean

GitHub source file

52 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.PettyProjection.RelativeGauge line 13

    Source documentation

    A genuine extended gauge of a relative symmetric convex body. The lower bound is only on its supporting subspace, so cylinders are retained.

    structure RelativeGauge {n : ℕ} (V : Submodule ℝ (Space n)) where
…

    Mentions: OAI.PettyProjection.Space

  2. instance OAI.PettyProjection.(instance at line 18) line 18
  3. def OAI.PettyProjection.RelativeGauge.body line 24
  4. lemma OAI.PettyProjection.RelativeGauge.zero_mem line 26
  5. lemma OAI.PettyProjection.RelativeGauge.nonempty line 27
  6. lemma OAI.PettyProjection.RelativeGauge.convex line 28
  7. lemma OAI.PettyProjection.RelativeGauge.closed line 29
  8. lemma OAI.PettyProjection.RelativeGauge.neg_mem line 30
  9. lemma OAI.PettyProjection.RelativeGauge.compact line 36
  10. lemma OAI.PettyProjection.RelativeGauge.ne_zero line 46
  11. lemma OAI.PettyProjection.RelativeGauge.pos line 55
  12. lemma OAI.PettyProjection.RelativeGauge.radial_mem line 61
  13. lemma OAI.PettyProjection.RelativeGauge.inner_le_gauge_support line 68
  14. lemma OAI.PettyProjection.RelativeGauge.cosine_le_gauge_functional line 78
  15. def OAI.PettyProjection.RelativeGauge.scale line 92

    Source documentation

    Every positive dilation is again the exact relative gauge.

    def scale (g : RelativeGauge V) (a : ℝ) (ha : 0<a) : RelativeGauge V where
…

    Mentions: OAI.PettyProjection.RelativeGauge

  16. lemma OAI.PettyProjection.RelativeGauge.scale_apply line 103
  17. lemma OAI.PettyProjection.RelativeGauge.body_scale line 106
  18. lemma OAI.PettyProjection.RelativeGauge.functional_scale line 122
  19. def OAI.PettyProjection.Spherical.objectiveIntegrand line 137

    Source documentation

    Variational objective: the logarithmic endpoint (k=1), or the linear (k=2).

    def objectiveIntegrand (logarithmic : Bool) (t : ℝ) : ℝ :=
…
  20. def OAI.PettyProjection.Spherical.objective line 140
  21. lemma OAI.PettyProjection.Spherical.seminorm_integrable line 143
  22. lemma OAI.PettyProjection.Spherical.objective_integrable line 147
  23. lemma OAI.PettyProjection.Spherical.objectiveIntegrand_strictMono line 153
  24. lemma OAI.PettyProjection.Spherical.objective_mono line 158
  25. lemma OAI.PettyProjection.Spherical.objective_mono_eq line 164
  26. lemma OAI.PettyProjection.Spherical.objective_scale line 182
  27. lemma OAI.PettyProjection.Spherical.coordinate_mean_pos line 196
  28. lemma OAI.PettyProjection.Spherical.objective_coercive line 205

    Source documentation

    Objective sublevels impose a common Lipschitz bound, including cylinders.

    lemma objective_coercive {n : ℕ} [NeZero n] (b : Bool) (M : ℝ) :
    ∃ R : ℝ,0<R ∧ ∀ g : Seminorm ℝ (Space n),g≠0 → objective b g≤M → ∀ u : Sphere n,g u≤R := by
…

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

  29. lemma OAI.PettyProjection.Spherical.objective_tendsto line 230
  30. lemma OAI.PettyProjection.seminorm_positive_subspace_bound line 256
  31. def OAI.PettyProjection.RelativeGauge.ball line 282

    Source documentation

    Extended gauge of the unit ball in V.

    def ball (V : Submodule ℝ (Space n)) : RelativeGauge V where
…

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

  32. lemma OAI.PettyProjection.RelativeGauge.ball_apply line 289
  33. lemma OAI.PettyProjection.RelativeGauge.support_ball line 291
  34. lemma OAI.PettyProjection.RelativeGauge.cylinder_nhds line 320
  35. def OAI.PettyProjection.RelativeGauge.ofBody line 332

    Source documentation

    Recover the relative extended gauge from an actual relative convex body.

    def ofBody {K : Set (Space n)} (hK : IsCompact K) (hc : Convex ℝ K) (hb : Balanced ℝ K)
    (hinner : ∃ r : ℝ,0<r ∧ ∀ x∈V,‖x‖≤r → x∈K) : RelativeGauge V := by
…

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

  36. lemma OAI.PettyProjection.RelativeGauge.ofBody_apply line 361
  37. lemma OAI.PettyProjection.RelativeGauge.body_ofBody line 365
  38. lemma OAI.PettyProjection.support_mono_compact line 391
  39. lemma OAI.PettyProjection.functional_mono_compact line 398
  40. lemma OAI.PettyProjection.RelativeGauge.balanced line 408
  41. lemma OAI.PettyProjection.RelativeGauge.inner_ball line 414
  42. lemma OAI.PettyProjection.RelativeGauge.body_subset_smul line 420
  43. lemma OAI.PettyProjection.RelativeGauge.functional_le_scale line 428
  44. lemma OAI.PettyProjection.RelativeGauge.functional_pos line 435
  45. lemma OAI.PettyProjection.RelativeGauge.normalized_lower line 443
  46. lemma OAI.PettyProjection.RelativeGauge.support_bound line 449
  47. lemma OAI.PettyProjection.RelativeGauge.functional_bound line 461
  48. lemma OAI.PettyProjection.RelativeGauge.seminorm_close_ambient line 468
  49. lemma OAI.PettyProjection.RelativeGauge.close_le_scale line 480
  50. lemma OAI.PettyProjection.RelativeGauge.functional_close line 491
  51. lemma OAI.PettyProjection.RelativeGauge.functional_tendsto line 517
  52. theorem OAI.PettyProjection.RelativeGauge.normalized_subsequence line 546

    Source documentation

    Compactness of fixed-subspace normalized gauges. All constants arise from the actual cosine norm and objective, not regularity assumptions.

    theorem normalized_subsequence {μ : Measure (Space n)}
    (hμ : Integrable (fun x : Space n => ‖x‖) μ) (hV : V≠⊥)
    (hq : ∀ x∈V,x≠0 → 0<cosineSeminorm μ hμ x)
    (b : Bool) (g : ℕ → RelativeGauge V) (hn : ∀ i,supportFunctional μ (g i).body=1)
    {M : ℝ} (hM : ∀ i,Spherical.objective b (g i).toSeminorm≤M) :
    ∃ f : RelativeGauge V, ∃ φ : ℕ → ℕ, StrictMono φ ∧ supportFunctional μ f.body=1 ∧
      TendstoUniformly (fun i (u : Sphere n) => g (φ i) u) (fun u => f u) atTop ∧
      Tendsto (fun i => Spherical.objective b (g (φ i)).toSeminorm) atTop
        (𝓝 (Spherical.objective b f.toSeminorm)) := by
…

    Mentions: OAI.PettyProjection.Space, OAI.PettyProjection.cosineSeminorm, OAI.PettyProjection.RelativeGauge, OAI.PettyProjection.supportFunctional, OAI.PettyProjection.RelativeGauge.body, OAI.PettyProjection.Spherical.objective