PoissonVectorAverage.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

Vector integration for Poisson smoothing

The averages are taken on each Hilbert-space vector. No norm measurability of an operator-valued field is required. The fixed standard Cauchy measure allows dominated convergence at every point of strong continuity.

theorem OAI.KadisonKastler.integrable_vectorField line 26

def OAI.KadisonKastler.probabilityOperatorIntegral line 35

Source documentation

An actual bounded operator obtained by integrating its values on vectors.

def probabilityOperatorIntegral (μ : Measure S) [IsProbabilityMeasure μ]
    (F : S → H →L[ℂ] H) (hm : ∀ x, AEStronglyMeasurable (fun s => F s x) μ)
    (C : ℝ) (hb : ∀ᵐ s ∂μ, ‖F s‖ ≤ C) : H →L[ℂ] H :=
…

theorem OAI.KadisonKastler.probabilityOperatorIntegral_apply line 56
theorem OAI.KadisonKastler.norm_probabilityOperatorIntegral_le line 62
theorem OAI.KadisonKastler.probabilityOperatorIntegral_star line 75
theorem OAI.KadisonKastler.norm_probabilityOperatorIntegral_sub_le line 102

def OAI.KadisonKastler.poissonVectorAverage line 123

Source documentation

Poisson averaging, written with the standard Cauchy random variable.

def poissonVectorAverage (F : ℝ → H →L[ℂ] H)
    (hF : ∀ x, Continuous (fun s => F s x)) (C : ℝ) (hC : ∀ s, ‖F s‖ ≤ C)
    (t r : ℝ) : H →L[ℂ] H :=
…

theorem OAI.KadisonKastler.poissonVectorAverage_tendsto line 131

theorem OAI.KadisonKastler.poissonVectorAverage_star_tendsto line 155

Source documentation

The adjoints also converge at every time of strong-* continuity.

theorem poissonVectorAverage_star_tendsto (F : ℝ → H →L[ℂ] H)
    (hF : ∀ x, Continuous (fun s => F s x))
    (hFs : ∀ x, Continuous (fun s => star (F s) x))
    (C : ℝ) (hC : ∀ s, ‖F s‖ ≤ C) (t : ℝ) (x : H) :
    Tendsto (fun r => star (poissonVectorAverage F hF C hC t r) x)
      (𝓝 0) (𝓝 (star (F t) x)) := by
…

Mentions: OAI.KadisonKastler.poissonVectorAverage