OAI/Geometry/ProjectionBodies/RankContinuity.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.PettyProjection.support_min_tendsto line 14

   Source documentation

   Actual lower-semicontinuity at a singular change of range, formulated with a bounded projected cylinder instead of extended real support functions.

   lemma support_min_tendsto {V : Submodule ℝ (Space n)}
       {Vj : ℕ → Submodule ℝ (Space n)} (gj : ∀ i,RelativeGauge (Vj i))
       (g : Seminorm ℝ (Space n)) {c : ℝ} (hc : 0<c)
       (hl : ∀ x,c*‖V.starProjection x‖≤g x)
       (hg : ∀ x,Tendsto (fun i => gj i x) atTop (𝓝 (g x)))
       {uj : ℕ → Space n} {u : Space n} (hu : u∈V) (huj : ∀ i,uj i∈Vj i)
       (ht : Tendsto uj atTop (𝓝 u)) :
       Tendsto (fun i => min (support (gj i).body (uj i))
         (support (RelativeGauge.project V g hc hl).body u)) atTop
         (𝓝 (support (RelativeGauge.project V g hc hl).body u)) := by
   …

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

2. lemma OAI.PettyProjection.projected_limit_normalization line 53
3. lemma OAI.PettyProjection.RelativeGauge.full_lower line 108
4. def OAI.PettyProjection.RelativeGauge.projectFull line 113
5. lemma OAI.PettyProjection.RelativeGauge.projectFull_le line 119
6. lemma OAI.PettyProjection.RelativeGauge.projectFull_body line 123
7. lemma OAI.PettyProjection.RelativeGauge.support_projectFull line 129
8. lemma OAI.PettyProjection.RelativeGauge.functional_projectFull line 147
9. lemma OAI.PettyProjection.RelativeGauge.minimizer_full_comparison line 156
10. def OAI.PettyProjection.RelativeGauge.thicken line 192

    Source documentation

    A genuine full-dimensional approximation of an arbitrary relative gauge. The sum regularization avoids any constant-rank assumption.

    def thicken (g : RelativeGauge V) (ε : ℝ) (hε : 0<ε) :
        RelativeGauge (⊤ : Submodule ℝ (Space n)) where
    …

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

11. lemma OAI.PettyProjection.RelativeGauge.thicken_apply line 206
12. lemma OAI.PettyProjection.RelativeGauge.thicken_ge line 209
13. lemma OAI.PettyProjection.RelativeGauge.support_thicken_le line 212
14. lemma OAI.PettyProjection.RelativeGauge.functional_thicken_le line 224
15. lemma OAI.PettyProjection.RelativeGauge.objective_thicken_tendsto line 236
16. lemma OAI.PettyProjection.RelativeGauge.cosine_map_tendsto line 269
17. lemma OAI.PettyProjection.RelativeGauge.normalized_limit_lower line 280
18. lemma OAI.PettyProjection.RelativeGauge.full_comparison_limit line 293
19. theorem OAI.PettyProjection.RelativeGauge.minimizer_limit_identify line 329

    Source documentation

    Every seminorm limit of actual minimizers is the actual minimizer in the limiting range, including arbitrary drops of rank.

    theorem minimizer_limit_identify (hμ : Integrable (fun x : Space n => ‖x‖) μ)
        (hq : ∀ x : Space n,x≠0 → 0< cosineSeminorm μ hμ x)
        {Aj : ℕ → Space n →L[ℝ] Space n} {A : Space n →L[ℝ] Space n}
        (hA : Tendsto Aj atTop (𝓝 A)) (hAn : LinearMap.range A.toLinearMap≠⊥)
        (hAj : ∀ i,LinearMap.range (Aj i).toLinearMap≠⊥) (b : Bool)
        (gj : ∀ i,RelativeGauge (LinearMap.range (Aj i).toLinearMap))
        (hn : ∀ i,supportFunctional (μ.map (Aj i)) (gj i).body=1)
        (hm : ∀ i (q : RelativeGauge (LinearMap.range (Aj i).toLinearMap)),supportFunctional (μ.map (Aj i)) q.body=1 → objective b (gj i).toSeminorm≤ objective b q.toSeminorm)
        (gA : RelativeGauge (LinearMap.range A.toLinearMap)) (hgn : supportFunctional (μ.map A) gA.body=1)
        (hgm : ∀ q : RelativeGauge (LinearMap.range A.toLinearMap),supportFunctional (μ.map A) q.body=1 → objective b gA.toSeminorm≤ objective b q.toSeminorm)
        {g : Seminorm ℝ (Space n)} (hg : ∀ x,Tendsto (fun i => gj i x) atTop (𝓝 (g x)))
        (hobj : Tendsto (fun i => objective b (gj i).toSeminorm) atTop (𝓝 (objective b g))) :
    …

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

20. lemma OAI.PettyProjection.RelativeGauge.full_functional_pos line 400
21. lemma OAI.PettyProjection.RelativeGauge.minimizers_uniform_bound line 408
22. lemma OAI.PettyProjection.RelativeGauge.objective_tendsto_of_pointwise line 437
23. lemma OAI.PettyProjection.RelativeGauge.limit_ne_zero line 462
24. theorem OAI.PettyProjection.RelativeGauge.minimizers_subsequence line 478

    Source documentation

    Sequential uniform compactness, and identification, for the actual optimizer family across all nonzero linear maps, without a rank restriction.

    theorem minimizers_subsequence (hμ : Integrable (fun x : Space n => ‖x‖) μ)
        (hq : ∀ x : Space n,x≠0 → 0< cosineSeminorm μ hμ x)
        {Aj : ℕ → Space n →L[ℝ] Space n} {A : Space n →L[ℝ] Space n}
        (hA : Tendsto Aj atTop (𝓝 A)) (hAn : LinearMap.range A.toLinearMap≠⊥)
        (hAj : ∀ i,LinearMap.range (Aj i).toLinearMap≠⊥) (b : Bool)
        (gj : ∀ i,RelativeGauge (LinearMap.range (Aj i).toLinearMap))
        (hn : ∀ i,supportFunctional (μ.map (Aj i)) (gj i).body=1)
        (hm : ∀ i (q : RelativeGauge (LinearMap.range (Aj i).toLinearMap)),supportFunctional (μ.map (Aj i)) q.body=1 →
          objective b (gj i).toSeminorm≤ objective b q.toSeminorm)
        (gA : RelativeGauge (LinearMap.range A.toLinearMap)) (hgn : supportFunctional (μ.map A) gA.body=1)
        (hgm : ∀ q : RelativeGauge (LinearMap.range A.toLinearMap),supportFunctional (μ.map A) q.body=1 →
          objective b gA.toSeminorm≤ objective b q.toSeminorm) :
    …

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