MeasurablePoisson.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

Poisson integration of bounded vector-measurable operator fields

The analytic multiplier fields need only be measurable on each vector. These averages therefore use vector integrals, without asserting norm measurability of a field valued in the bounded operators.

theorem OAI.KadisonKastler.cauchyMeasure_absolutelyContinuous line 20
def OAI.KadisonKastler.measurablePoissonAverage line 27
theorem OAI.KadisonKastler.measurablePoissonAverage_apply line 35
theorem OAI.KadisonKastler.norm_measurablePoissonAverage_le line 54

theorem OAI.KadisonKastler.norm_measurablePoissonAverage_sub_le line 62

Source documentation

Averaging preserves an essential uniform approximation bound.

theorem norm_measurablePoissonAverage_sub_le (F G : ℝ → H →L[ℂ] H)
    (hF : ∀ x, AEStronglyMeasurable (fun s => F s x) volume)
    (hG : ∀ x, AEStronglyMeasurable (fun s => G s x) volume)
    (C D : ℝ) (hC : ∀ᵐ s, ‖F s‖ ≤ C) (hD : ∀ᵐ s, ‖G s‖ ≤ D)
    {e : ℝ} (he : 0 ≤ e) (hFG : ∀ᵐ s, ‖F s - G s‖ ≤ e)
    (t r : ℝ) (hr : 0 < r) :
    ‖measurablePoissonAverage F hF C hC t r hr -
      measurablePoissonAverage G hG D hD t r hr‖ ≤ e :=
…

Mentions: OAI.KadisonKastler.measurablePoissonAverage

theorem OAI.KadisonKastler.measurablePoissonAverage_eq_poissonVectorAverage line 73
theorem OAI.KadisonKastler.integrable_measurablePoisson_vector line 82

theorem OAI.KadisonKastler.norm_measurablePoissonAverage_translate_sub_le line 99

Source documentation

An essentially bounded vector-measurable boundary field yields an operator-norm Lipschitz function on every horizontal line of positive height.

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

Mentions: OAI.KadisonKastler.measurablePoissonAverage

theorem OAI.KadisonKastler.continuous_measurablePoissonAverage line 135