Documentation

TauCeti.MeasureTheory.Integral.AddContent

Integration of simple functions against a real content #

Let ν be a real-valued content on a ring of sets C that contains the measurable sets of α. A real simple function f is integrated against ν by the finite sum ∑ c ∈ f.range, ν (f ⁻¹' {c}) * c (MeasureTheory.AddContent.integralSimple). Neither the sum nor its properties involve countable additivity.

The sum is Mathlib's MeasureTheory.SimpleFunc.setToSimpleFunc for the set function s ↦ ν s • id, taken with the zero measure: for it, FinMeasAdditive is finite additivity on disjoint measurable sets, and every simple function is integrable. This gives linearity, the value c * ν s at c times the indicator of a measurable set s, and, for nonnegative ν, the bound |∫ f dν| ≤ c * ν univ whenever |f| ≤ c. If ν vanishes on the null sets of a measure μ, the integral depends only on the μ-almost everywhere class of f.

These finite sums underlie the correspondences between positive linear functionals and nonnegative contents in TauCeti/Topology/ContinuousMap/Bounded/AddContent.lean (bounded functions on a discrete space, contents on all subsets) and TauCeti/MeasureTheory/Function/Lp/AddContent.lean (L∞, contents on the measurable sets).

Main definitions #

Main results #

source
noncomputable def MeasureTheory.AddContent.integralSimple {α : Type u_1} [MeasurableSpace α] {C : Set (Set α)} (ν : AddContent ℝ C) (hC : IsSetRing C) (hCm : ∀ (s : Set α), MeasurableSet s → s ∈ C) :
SimpleFunc α ℝ →ₗ[ℝ] ℝ

The integral ∑ c ∈ f.range, ν (f ⁻¹' {c}) * c of real simple functions f against a real content ν on a ring of sets containing the measurable sets.

Instances For
    source
    theorem MeasureTheory.AddContent.integralSimple_apply {α : Type u_1} [MeasurableSpace α] {C : Set (Set α)} (ν : AddContent ℝ C) (hC : IsSetRing C) (hCm : ∀ (s : Set α), MeasurableSet s → s ∈ C) (f : SimpleFunc α ℝ) :
    (ν.integralSimple hC hCm) f = ∑ c ∈ f.range, ν (⇑f ⁻¹' {c}) * c

    The integral of a simple function against a content is the sum, over its values c, of c times the content of the fiber over c.

    source
    theorem MeasureTheory.AddContent.integralSimple_piecewise {α : Type u_1} [MeasurableSpace α] {C : Set (Set α)} (ν : AddContent ℝ C) (hC : IsSetRing C) (hCm : ∀ (s : Set α), MeasurableSet s → s ∈ C) {s : Set α} (hs : MeasurableSet s) (c : ℝ) :
    (ν.integralSimple hC hCm) (SimpleFunc.piecewise s hs (SimpleFunc.const α c) (SimpleFunc.const α 0)) = c * ν s

    The integral of c times the indicator of a measurable set s is c * ν s.

    source
    theorem MeasureTheory.AddContent.integralSimple_le {α : Type u_1} [MeasurableSpace α] {C : Set (Set α)} {ν : AddContent ℝ C} (hC : IsSetRing C) (hCm : ∀ (s : Set α), MeasurableSet s → s ∈ C) (hν : ∀ (s : Set α), MeasurableSet s → 0 ≤ ν s) {f : SimpleFunc α ℝ} {c : ℝ} (h : ∀ (x : α), f x ≤ c) :
    (ν.integralSimple hC hCm) f ≤ c * ν Set.univ

    Against a nonnegative content, a simple function bounded above by c has integral at most c * ν univ.

    source
    theorem MeasureTheory.AddContent.abs_integralSimple_le {α : Type u_1} [MeasurableSpace α] {C : Set (Set α)} {ν : AddContent ℝ C} (hC : IsSetRing C) (hCm : ∀ (s : Set α), MeasurableSet s → s ∈ C) (hν : ∀ (s : Set α), MeasurableSet s → 0 ≤ ν s) {f : SimpleFunc α ℝ} {c : ℝ} (h : ∀ (x : α), |f x| ≤ c) :
    |(ν.integralSimple hC hCm) f| ≤ c * ν Set.univ

    Against a nonnegative content, a simple function bounded in absolute value by c has integral of absolute value at most c * ν univ.

    source
    theorem MeasureTheory.AddContent.integralSimple_congr_ae {α : Type u_1} [MeasurableSpace α] {C : Set (Set α)} {ν : AddContent ℝ C} (hC : IsSetRing C) (hCm : ∀ (s : Set α), MeasurableSet s → s ∈ C) {μ : Measure α} (hνμ : ∀ (s : Set α), MeasurableSet s → μ s = 0 → ν s = 0) {f g : SimpleFunc α ℝ} (h : ⇑f =ᵐ[μ] ⇑g) :
    (ν.integralSimple hC hCm) f = (ν.integralSimple hC hCm) g

    If a content vanishes on the measurable μ-null sets, the integral of a simple function against it depends only on its μ-almost everywhere class.