PoissonNormContinuity.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Norm continuity of vectorwise Poisson averages

Although the boundary field is only strongly continuous, translating the integrable scalar kernel gives norm continuity of each positive-height operator average.

theorem OAI.KadisonKastler.continuous_realPoissonKernel line 20
theorem OAI.KadisonKastler.integrable_poisson_vector line 30

theorem OAI.KadisonKastler.norm_poissonVectorAverage_sub_le line 45

Source documentation

A quantitative translation bound independent of the boundary field's modulus of strong continuity.

theorem norm_poissonVectorAverage_sub_le
    (F : ℝ → H →L[ℂ] H) (hF : ∀ x, Continuous (fun s => F s x))
    {C : ℝ} (hC0 : 0 ≤ C) (hC : ∀ s, ‖F s‖ ≤ C)
    (t u : ℝ) {r : ℝ} (hr : 0 < r) :
    ‖poissonVectorAverage F hF C hC t r - poissonVectorAverage F hF C hC u r‖ ≤
      (2 * C / r) * |t - u| := by
…

Mentions: OAI.KadisonKastler.poissonVectorAverage

theorem OAI.KadisonKastler.continuous_poissonVectorAverage line 82

Source documentation

Positive-height Poisson smoothing is continuous in operator norm.

theorem continuous_poissonVectorAverage
    (F : ℝ → H →L[ℂ] H) (hF : ∀ x, Continuous (fun s => F s x))
    {C : ℝ} (hC0 : 0 ≤ C) (hC : ∀ s, ‖F s‖ ≤ C)
    {r : ℝ} (hr : 0 < r) :
    Continuous (fun t => poissonVectorAverage F hF C hC t r) := by
…

Mentions: OAI.KadisonKastler.poissonVectorAverage