OAI/Analysis/KadisonKastler/StripAverageMembership.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Recovering algebra membership from all strip averages

Once the bounded modular equation identifies these averages with algebra elements, this lemma gives membership of every operator on the orbit.

  1. theorem OAI.KadisonKastler.mem_of_strip_averages line 21

    Source documentation

    Exponential strip averages determine membership in a von Neumann algebra.

    theorem mem_of_strip_averages (M : VonNeumannAlgebra H) {a : ℝ} (ha : 0 < a)
    (F : ℝ → H →L[ℂ] H) (hc : ∀ x, Continuous (fun t => F t x))
    (B : ℝ) (hb : ∀ t, ‖F t‖ ≤ B)
    (hm : ∀ s (hs : |s| < a),
      weightedOperatorIntegral volume (stripAverageKernel a (s : ℂ))
        (stripAverageKernel_integrable (by simpa using hs)) F
        (fun x => (hc x).aestronglyMeasurable) B (Filter.Eventually.of_forall hb) ∈ M) :
    ∀ t, F t ∈ M := by
…

    Mentions: OAI.KadisonKastler.weightedOperatorIntegral, OAI.KadisonKastler.stripAverageKernel, OAI.KadisonKastler.stripAverageKernel_integrable