setToFun_indicator_const — Mathlib

English

For a measurable set s, the indicator of s times x maps through setToFun to the action of T on s and x: setToFun μ T hT (s.indicator (fun _ => x)) = T s x.

Русский

На измеримом множестве s индикатор функции, умноженный на x, переносится через setToFun в действие T на s применительно к x.

LaTeX

$$$\mathrm{setToFun}(\mu, T)\,h_T (\mathbf{1}_s \cdot x) = T(s) x$$$

Lean4

theorem setToFun_indicator_const (hT : DominatedFinMeasAdditive μ T C) {s : Set α} (hs : MeasurableSet s)
    (hμs : μ s ≠ ∞) (x : E) : setToFun μ T hT (s.indicator fun _ => x) = T s x :=
  by
  rw [setToFun_congr_ae hT (@indicatorConstLp_coeFn _ _ _ 1 _ _ _ hs hμs x).symm]
  rw [L1.setToFun_eq_setToL1 hT]
  exact L1.setToL1_indicatorConstLp hT hs hμs x

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