aestronglyMeasurable_condExpInd — Mathlib

English

The family (μ, condExpInd) defines a Dominated FinMeasAdditive object with bound 1, i.e., for every measurable S, condExpInd acts as a finite-additive set-function dominated by 1.

Русский

Семейство (μ, condExpInd) образуют Dominated FinMeasAdditive с верхней гранью 1, то есть для каждого измеримого S condExpInd ограничено сверху единицей.

LaTeX

$$$ \text{DominatedFinMeasAdditive}\; μ\; (condExpInd\; G\; hm\; μ) \; 1$$

Lean4

theorem aestronglyMeasurable_condExpInd (hs : MeasurableSet s) (hμs : μ s ≠ ∞) (x : G) :
    AEStronglyMeasurable[m] (condExpInd G hm μ s x) μ :=
  (aestronglyMeasurable_condExpIndSMul hm hs hμs x).congr (condExpInd_ae_eq_condExpIndSMul hm hs hμs x).symm

Похожие утверждения