OAI/Analysis/KadisonKastler/ScalarWeakLimit.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Bounded scalar weak limits

Uniformly bounded scalar functions have simultaneous weak L2 cluster points on a probability space. Closed convex disk constraints retain the essential bound, so the limits are actual L-infinity classes.

  1. def OAI.KadisonKastler.scalarInfinityToL2 line 22
  2. theorem OAI.KadisonKastler.scalarInfinityToL2_ae line 25
  3. theorem OAI.KadisonKastler.norm_scalarInfinityToL2_le line 28
  4. theorem OAI.KadisonKastler.scalarInfinityToL2_injective line 35
  5. theorem OAI.KadisonKastler.scalarInfinityToL2_add line 43
  6. theorem OAI.KadisonKastler.scalarInfinityToL2_smul line 52
  7. def OAI.KadisonKastler.scalarInfinityToL2L line 60
  8. theorem OAI.KadisonKastler.scalarInfinityToL2L_apply line 68
  9. theorem OAI.KadisonKastler.exists_scalar_weak_ultralimit line 71
  10. theorem OAI.KadisonKastler.exists_scalar_linear_weak_ultralimit line 97

    Source documentation

    One ultrafilter gives a simultaneous linear, contractive scalar limit.

    theorem exists_scalar_linear_weak_ultralimit
    {E : Type*} [NormedAddCommGroup E] [NormedSpace ℂ E]
    {ι : Type*} (ω : Ultrafilter ι) (A : ι → E →L[ℂ] ScalarLInfinity μ)
    (hA : ∀ i x, ‖A i x‖ ≤ ‖x‖) :
    ∃ B : E →L[ℂ] ScalarLInfinity μ, (∀ x, ‖B x‖ ≤ ‖x‖) ∧
      ∀ x y, Tendsto (fun i => inner ℂ y (scalarInfinityToL2 (A i x))) (ω : Filter ι)
        (𝓝 (inner ℂ y (scalarInfinityToL2 (B x)))) := by
…

    Mentions: OAI.KadisonKastler.ScalarLInfinity, OAI.KadisonKastler.scalarInfinityToL2