OAI/Dynamics/TriangleBilliards/WeakCompactness.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.TriangularBilliards.Analytic.WeaklyTendsto line 51

   Source documentation

   Scalar-test characterization of weak convergence over the real field.

   def WeaklyTendsto (u : α → E) (l : Filter α) (v : E) : Prop :=
   …

2. lemma OAI.TriangularBilliards.Analytic.weaklyTendsto_of_tendsto line 54
3. lemma OAI.TriangularBilliards.Analytic.WeaklyTendsto.comp line 58
4. lemma OAI.TriangularBilliards.Analytic.WeaklyTendsto.prod line 63
5. lemma OAI.TriangularBilliards.Analytic.WeaklyTendsto.sub_const line 72
6. lemma OAI.TriangularBilliards.Analytic.WeaklyTendsto.mem_of_closed_convex line 80

   Source documentation

   Norm-closed convex sets remain closed under weak limits. In particular this applies to a uniform L∞ bound inside L² and to a closed derivative graph.

   lemma WeaklyTendsto.mem_of_closed_convex [l.NeBot] {u : α → E} {v : E}
       (h : WeaklyTendsto u l v) {C : Set E} (hc : IsClosed C) (hcv : Convex ℝ C)
       (hu : ∀ᶠ n in l, u n ∈ C) : v ∈ C := by
   …

   Mentions: OAI.TriangularBilliards.Analytic.WeaklyTendsto

7. lemma OAI.TriangularBilliards.Analytic.WeaklyTendsto.norm_le line 88
8. lemma OAI.TriangularBilliards.Analytic.WeaklyTendsto.norm_le_of_bounds line 94
9. lemma OAI.TriangularBilliards.Analytic.exists_weak_subsequence line 113

   Source documentation

   Weak sequential compactness of a bounded set in a separable real Hilbert space, obtained from Banach–Alaoglu and Riesz.

   lemma exists_weak_subsequence (u : ℕ → E) {R : ℝ} (hu : ∀ n, ‖u n‖ ≤ R) :
       ∃ v : E, ‖v‖ ≤ R ∧ ∃ φ : ℕ → ℕ, StrictMono φ ∧ WeaklyTendsto (u ∘ φ) atTop v := by
   …

   Mentions: OAI.TriangularBilliards.Analytic.WeaklyTendsto

10. def OAI.TriangularBilliards.Analytic.TestGraph line 150

    Source documentation

    A distributional graph described by test identities. Instantiating it with weak differentiation requires constructing its actual test functionals.

    def TestGraph {ι : Type uIota} (A : ι → E →L[ℝ] ℝ) (B : ι → F →L[ℝ] ℝ) : Set (E × F) :=
    …

11. lemma OAI.TriangularBilliards.Analytic.testGraph_closed line 153
12. lemma OAI.TriangularBilliards.Analytic.testGraph_convex line 162
13. lemma OAI.TriangularBilliards.Analytic.testGraph_weak_limit line 170

    Source documentation

    Identifying the weak derivative limit uses only test identities, not an unjustified claim that the entire horizontal derivative lies in L².

    lemma testGraph_weak_limit {ι : Type uIota} {α : Type uAlpha} (A : ι → E →L[ℝ] ℝ) (B : ι → F →L[ℝ] ℝ)
        {l : Filter α} [l.NeBot] {u : α → E} {d : α → F} {v : E} {e : F}
        (hu : WeaklyTendsto u l v) (hd : WeaklyTendsto d l e)
        (hgraph : ∀ᶠ n in l, (u n, d n) ∈ TestGraph A B) : (v, e) ∈ TestGraph A B :=
    …

    Mentions: OAI.TriangularBilliards.Analytic.WeaklyTendsto, OAI.TriangularBilliards.Analytic.TestGraph

14. lemma OAI.TriangularBilliards.Analytic.testGraph_unique line 185
15. lemma OAI.TriangularBilliards.Analytic.testGraph_pairing_of_strong_limit line 197

    Source documentation

    The second-limit step: strong convergence of the functions and a uniform bound for only the relevant derivatives suffice to pass a fixed pairing to the limit. There is no bound for the sum of all mode derivatives.

    lemma testGraph_pairing_of_strong_limit {ι : Type uIota}
        (A : ι → E →L[ℝ] ℝ) (B : ι → F →L[ℝ] ℝ)
        (hsep : ∀ v : F, (∀ i, B i v = 0) → v = 0)
        (u : ℕ → E) (d : ℕ → F) {f : E} {e : F} {R : ℝ}
        (hgraph : ∀ n, (u n, d n) ∈ TestGraph A B)
        (hf : (f, e) ∈ TestGraph A B)
        (hu : Tendsto u atTop (𝓝 f)) (hd : ∀ n, ‖d n‖ ≤ R)
        (L : F →L[ℝ] ℝ) (hL : Tendsto (fun n => L (d n)) atTop (𝓝 0)) : L e = 0 := by
    …

    Mentions: OAI.TriangularBilliards.Analytic.TestGraph

16. lemma OAI.TriangularBilliards.Analytic.testGraph_first_limit line 226

    Source documentation

    The fixed-clearance-budget weak limit. The derivative bound M is allowed to depend on that fixed budget. An application must supply all smoothing, support, transport and distributional-graph properties; this lemma supplies the two subsequence extractions and all limit passages.

    lemma testGraph_first_limit {ι : Type uIota} {κ : Type uKappa}
        (A : ι → E →L[ℝ] ℝ) (B : ι → F →L[ℝ] ℝ) (X : κ → E →L[ℝ] ℝ)
        (C : Set E) (hCclosed : IsClosed C) (hCconvex : Convex ℝ C)
        (u : ℕ → E) (d : ℕ → F) {f : E} {H M δ : ℝ} (δn : ℕ → ℝ)
        (hu : ∀ n, ‖u n‖ ≤ H) (hd : ∀ n, ‖d n‖ ≤ M)
        (hC : ∀ n, u n ∈ C) (hgraph : ∀ n, (u n, d n) ∈ TestGraph A B)
        (hX : ∀ k, Tendsto (fun n => X k (u n)) atTop (𝓝 0))
        (hδn : Tendsto δn atTop (𝓝 δ)) (hclose : ∀ n, ‖u n - f‖ ≤ δn n)
        (L : F →L[ℝ] ℝ) (hL : Tendsto (fun n => L (d n)) atTop (𝓝 0)) :
        ∃ g : E, ∃ e : F,
          g ∈ C ∧ (∀ k, X k g = 0) ∧ ‖g - f‖ ≤ δ ∧ (g, e) ∈ TestGraph A B ∧ L e = 0 := by
    …

    Mentions: OAI.TriangularBilliards.Analytic.TestGraph

17. lemma OAI.TriangularBilliards.Analytic.exists_weak_subsequence_unrestricted line 258