average_mem_openSegment_compl_self

English

The average with respect to μ|s equals the integral over s divided by μ(s).

Русский

Среднее по μ|s равно интегралу по s, делённому на μ(s).

LaTeX

$$$\operatorname{average}(\mu|_s) f = (\mu.s)^{-1} \int_{s} f \, d\mu$$$

Lean4

theorem average_mem_openSegment_compl_self [IsFiniteMeasure μ] {f : α → E} {s : Set α} (hs : NullMeasurableSet s μ)
    (hs₀ : μ s ≠ 0) (hsc₀ : μ sᶜ ≠ 0) (hfi : Integrable f μ) :
    ⨍ x, f x ∂μ ∈ openSegment ℝ (⨍ x in s, f x ∂μ) (⨍ x in sᶜ, f x ∂μ) := by
  simpa only [union_compl_self, restrict_univ] using
    average_union_mem_openSegment aedisjoint_compl_right hs.compl hs₀ hsc₀ (measure_ne_top _ _) (measure_ne_top _ _)
      hfi.integrableOn hfi.integrableOn

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