laverage_mem_openSegment_compl_self

English

For finite μ and finite-measurable s, the laverage over s has to lie in the open segment between laverage over s and laverage over sᶜ.

Русский

Для конечной меры μ и конечного множества s laverage над s лежит внутри открытого отрезка между лаverage над s и над комплементом s.

LaTeX

$$$\\laverage_{μ}(f) ∈ openSegment \\mathbb{R}_{\\ge 0}^{\\infty} (\\laverage_{μ|s} f) (\\laverage_{μ|s^c} f)$$$

Lean4

theorem laverage_mem_openSegment_compl_self [IsFiniteMeasure μ] (hs : NullMeasurableSet s μ) (hs₀ : μ s ≠ 0)
    (hsc₀ : μ sᶜ ≠ 0) : ⨍⁻ x, f x ∂μ ∈ openSegment ℝ≥0∞ (⨍⁻ x in s, f x ∂μ) (⨍⁻ x in sᶜ, f x ∂μ) := by
  simpa only [union_compl_self, restrict_univ] using
    laverage_union_mem_openSegment aedisjoint_compl_right hs.compl hs₀ hsc₀ (measure_ne_top _ _) (measure_ne_top _ _)

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