integrable_indicatorConstLp — Mathlib

English

Under the same hypotheses as IndicatorConstLp, the integrability holds for the corresponding constant function in the Lp framework.

Русский

При тех же предпосылках, что и IndicatorConstLp, интегрируемость сохраняется для соответствующей константной функции в рамках Lp.

LaTeX

$$Integrable (indicatorConstLp p hs hμs c).val.cast μ$$

Lean4

theorem integrable_indicatorConstLp {E} [NormedAddCommGroup E] {p : ℝ≥0∞} {s : Set α} (hs : MeasurableSet s)
    (hμs : μ s ≠ ∞) (c : E) : Integrable (indicatorConstLp p hs hμs c) μ :=
  by
  rw [integrable_congr indicatorConstLp_coeFn, integrable_indicator_iff hs, IntegrableOn, integrable_const_iff,
    isFiniteMeasure_restrict]
  exact .inr hμs

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