mathlib documentation

measure_theory.set_integral

Set integral

In this file we prove some properties of ∫ x in s, f x ∂μ. Recall that this notation is defined as ∫ x, f x ∂(μ.restrict s). In integral_indicator we prove that for a measurable function f and a measurable set s this definition coincides with another natural definition: ∫ x, indicator s f x ∂μ = ∫ x in s, f x ∂μ, where indicator s f x is equal to f x for x ∈ s and is zero otherwise.

Since ∫ x in s, f x ∂μ is a notation, one can rewrite or apply any theorem about ∫ x, f x ∂μ directly. In this file we prove some theorems about dependence of ∫ x in s, f x ∂μ on s, e.g. integral_union, integral_empty, integral_univ.

We also define integrable_on f s μ := integrable f (μ.restrict s) and prove theorems like integrable_on_union : integrable_on f (s ∪ t) μ ↔ integrable_on f s μ ∧ integrable_on f t μ.

Next we define a predicate integrable_at_filter (f : α → E) (l : filter α) (μ : measure α) saying that f is integrable at some set s ∈ l and prove that a measurable function is integrable at l with respect to μ provided that f is bounded above at l ⊓ μ.ae and μ is finite at l.

Finally, we prove a version of the Fundamental theorem of calculus for set integral, see filter.tendsto.integral_sub_linear_is_o_ae and its corollaries. Namely, consider a measurably generated filter l, a measure μ finite at this filter, and a function f that has a finite limit c at l ⊓ μ.ae. Then ∫ x in s, f x ∂μ = μ s • c + o(μ s) as s tends to l.lift' powerset, i.e. for any ε>0 there exists t ∈ l such that ∥∫ x in s, f x ∂μ - μ s • c∥ ≤ ε * μ s whenever s ⊆ t. We also formulate a version of this theorem for a locally finite measure μ and a function f continuous at a point a.

Notation

∫ a in s, f a is measure_theory.integral (s.indicator f)

TODO

The file ends with over a hundred lines of commented out code. This is the old contents of this file using the indicator approach to the definition of ∫ x in s, f x ∂μ. This code should be migrated to the new definition.

theorem piecewise_ae_eq_restrict {α : Type u_1} {β : Type u_2} [measurable_space α] {μ : measure_theory.measure α} {s : set α} {f g : α → β} :

theorem piecewise_ae_eq_restrict_compl {α : Type u_1} {β : Type u_2} [measurable_space α] {μ : measure_theory.measure α} {s : set α} {f g : α → β} :

theorem indicator_ae_eq_restrict {α : Type u_1} {β : Type u_2} [measurable_space α] [has_zero β] {μ : measure_theory.measure α} {s : set α} {f : α → β} :

theorem indicator_ae_eq_restrict_compl {α : Type u_1} {β : Type u_2} [measurable_space α] [has_zero β] {μ : measure_theory.measure α} {s : set α} {f : α → β} :

theorem measure_theory.has_finite_integral_restrict_of_bounded {α : Type u_1} {E : Type u_3} [measurable_space α] [normed_group E] {f : α → E} {s : set α} {μ : measure_theory.measure α} {C : } :
μ s < (∀ᵐ (x : α) ∂μ.restrict s, f x C)measure_theory.has_finite_integral f (μ.restrict s)

def measure_theory.integrable_on {α : Type u_1} {E : Type u_3} [measurable_space α] [normed_group E] [measurable_space E] :
(α → E)set α(measure_theory.measure α . "volume_tac") → Prop

A function is integrable_on a set s if it is a measurable function and if the integral of its pointwise norm over s is less than infinity.

Equations
theorem measure_theory.integrable_on.integrable {α : Type u_1} {E : Type u_3} [measurable_space α] [normed_group E] [measurable_space E] {f : α → E} {s : set α} {μ : measure_theory.measure α} :

@[simp]
theorem measure_theory.integrable_on_empty {α : Type u_1} {E : Type u_3} [measurable_space α] [normed_group E] [measurable_space E] {f : α → E} {μ : measure_theory.measure α} :

theorem measure_theory.integrable_on_zero {α : Type u_1} {E : Type u_3} [measurable_space α] [normed_group E] [measurable_space E] {s : set α} {μ : measure_theory.measure α} :
measure_theory.integrable_on (λ (_x : α), 0) s μ

theorem measure_theory.integrable_on_const {α : Type u_1} {E : Type u_3} [measurable_space α] [normed_group E] [measurable_space E] {s : set α} {μ : measure_theory.measure α} {C : E} :
measure_theory.integrable_on (λ (_x : α), C) s μ C = 0 μ s <

theorem measure_theory.integrable_on.mono {α : Type u_1} {E : Type u_3} [measurable_space α] [normed_group E] [measurable_space E] {f : α → E} {s t : set α} {μ ν : measure_theory.measure α} :

theorem measure_theory.integrable_on.mono_set {α : Type u_1} {E : Type u_3} [measurable_space α] [normed_group E] [measurable_space E] {f : α → E} {s t : set α} {μ : measure_theory.measure α} :

theorem measure_theory.integrable_on.mono_measure {α : Type u_1} {E : Type u_3} [measurable_space α] [normed_group E] [measurable_space E] {f : α → E} {s : set α} {μ ν : measure_theory.measure α} :

theorem measure_theory.integrable_on.mono_set_ae {α : Type u_1} {E : Type u_3} [measurable_space α] [normed_group E] [measurable_space E] {f : α → E} {s t : set α} {μ : measure_theory.measure α} :

theorem measure_theory.integrable.integrable_on {α : Type u_1} {E : Type u_3} [measurable_space α] [normed_group E] [measurable_space E] {f : α → E} {s : set α} {μ : measure_theory.measure α} :

theorem measure_theory.integrable.integrable_on' {α : Type u_1} {E : Type u_3} [measurable_space α] [normed_group E] [measurable_space E] {f : α → E} {s : set α} {μ : measure_theory.measure α} :

theorem measure_theory.integrable_on.left_of_union {α : Type u_1} {E : Type u_3} [measurable_space α] [normed_group E] [measurable_space E] {f : α → E} {s t : set α} {μ : measure_theory.measure α} :

theorem measure_theory.integrable_on.right_of_union {α : Type u_1} {E : Type u_3} [measurable_space α] [normed_group E] [measurable_space E] {f : α → E} {s t : set α} {μ : measure_theory.measure α} :

theorem measure_theory.integrable_on.union {α : Type u_1} {E : Type u_3} [measurable_space α] [normed_group E] [measurable_space E] {f : α → E} {s t : set α} {μ : measure_theory.measure α} :

@[simp]

@[simp]
theorem measure_theory.integrable_on_finite_union {α : Type u_1} {β : Type u_2} {E : Type u_3} [measurable_space α] [normed_group E] [measurable_space E] {f : α → E} {μ : measure_theory.measure α} (hf : measurable f) {s : set β} (hs : s.finite) {t : β → set α} :
measure_theory.integrable_on f (⋃ (i : β) (H : i s), t i) μ ∀ (i : β), i smeasure_theory.integrable_on f (t i) μ

@[simp]
theorem measure_theory.integrable_on_finset_union {α : Type u_1} {β : Type u_2} {E : Type u_3} [measurable_space α] [normed_group E] [measurable_space E] {f : α → E} {μ : measure_theory.measure α} (hf : measurable f) {s : finset β} {t : β → set α} :
measure_theory.integrable_on f (⋃ (i : β) (H : i s), t i) μ ∀ (i : β), i smeasure_theory.integrable_on f (t i) μ

theorem measure_theory.integrable_on.add_measure {α : Type u_1} {E : Type u_3} [measurable_space α] [normed_group E] [measurable_space E] {f : α → E} {s : set α} {μ ν : measure_theory.measure α} :

@[simp]

theorem measure_theory.integrable_on.indicator {α : Type u_1} {E : Type u_3} [measurable_space α] [normed_group E] [measurable_space E] {f : α → E} {s : set α} {μ : measure_theory.measure α} :

def measure_theory.integrable_at_filter {α : Type u_1} {E : Type u_3} [measurable_space α] [normed_group E] [measurable_space E] :
(α → E)filter α(measure_theory.measure α . "volume_tac") → Prop

We say that a function f is integrable at filter l if it is integrable on some set s ∈ l. Equivalently, it is eventually integrable on s in l.lift' powerset.

Equations
theorem measure_theory.integrable_at_filter.eventually {α : Type u_1} {E : Type u_3} [measurable_space α] [normed_group E] [measurable_space E] {f : α → E} {μ : measure_theory.measure α} {l : filter α} :

If μ is a measure finite at filter l and f is a function such that its norm is bounded above at l, then f is integrable at l.

theorem measure_theory.integrable.induction {α : Type u_1} {E : Type u_3} [measurable_space α] [normed_group E] [measurable_space E] {μ : measure_theory.measure α} [borel_space E] [topological_space.second_countable_topology E] (P : (α → E) → Prop) (h_ind : ∀ (c : E) ⦃s : set α⦄, is_measurable sμ s < P (s.indicator (λ (_x : α), c))) (h_sum : ∀ ⦃f g : α → E⦄, set.univ f ⁻¹' {0} g ⁻¹' {0}measure_theory.integrable f μmeasure_theory.integrable g μP fP gP (f + g)) (h_closed : is_closed {f : α →₁[μ] E | P f}) (h_ae : ∀ ⦃f g : α → E⦄, f =ᵐ[μ] gmeasure_theory.integrable f μmeasurable gP fP g) ⦃f : α → E⦄ :

To prove something for an arbitrary measurable + integrable function in a second countable Borel normed group, it suffices to show that

  • the property holds for (multiples of) characteristic functions;
  • is closed under addition;
  • the set of functions in the space for which the property holds is closed.
  • the property is closed under the almost-everywhere equal relation.

It is possible to make the hypotheses in the induction steps a bit stronger, and such conditions can be added once we need them (for example in h_sum it is only necessary to consider the sum of a simple function with a multiple of a characteristic function and that the intersection of their images is a subset of {0}).

theorem measure_theory.integral_union {α : Type u_1} {E : Type u_3} [measurable_space α] [normed_group E] [measurable_space E] {f : α → E} {s t : set α} {μ : measure_theory.measure α} [borel_space E] [topological_space.second_countable_topology E] [complete_space E] [normed_space E] :
disjoint s tis_measurable sis_measurable tmeasure_theory.integrable_on f s μmeasure_theory.integrable_on f t μ (x : α) in s t, f x μ = (x : α) in s, f x μ + (x : α) in t, f x μ

theorem measure_theory.integral_univ {α : Type u_1} {E : Type u_3} [measurable_space α] [normed_group E] [measurable_space E] {f : α → E} {μ : measure_theory.measure α} [borel_space E] [topological_space.second_countable_topology E] [complete_space E] [normed_space E] :
(x : α) in set.univ, f x μ = (x : α), f x μ

theorem measure_theory.integral_add_compl {α : Type u_1} {E : Type u_3} [measurable_space α] [normed_group E] [measurable_space E] {f : α → E} {s : set α} {μ : measure_theory.measure α} [borel_space E] [topological_space.second_countable_topology E] [complete_space E] [normed_space E] :
is_measurable smeasure_theory.integrable f μ (x : α) in s, f x μ + (x : α) in s, f x μ = (x : α), f x μ

theorem measure_theory.integral_indicator {α : Type u_1} {E : Type u_3} [measurable_space α] [normed_group E] [measurable_space E] {f : α → E} {s : set α} {μ : measure_theory.measure α} [borel_space E] [topological_space.second_countable_topology E] [complete_space E] [normed_space E] :
measurable fis_measurable s (x : α), s.indicator f x μ = (x : α) in s, f x μ

For a measurable function f and a measurable set s, the integral of indicator s f over the whole space is equal to ∫ x in s, f x ∂μ defined as ∫ x, f x ∂(μ.restrict s).

@[simp]
theorem measure_theory.integral_indicator_const {α : Type u_1} {E : Type u_3} [measurable_space α] [normed_group E] [measurable_space E] {μ : measure_theory.measure α} [borel_space E] [topological_space.second_countable_topology E] [complete_space E] [normed_space E] (e : E) ⦃s : set α⦄ :
is_measurable s (a : α), s.indicator (λ (x : α), e) a μ = (μ s).to_real e

theorem measure_theory.set_integral_map {α : Type u_1} {E : Type u_3} [measurable_space α] [normed_group E] [measurable_space E] {μ : measure_theory.measure α} [borel_space E] [topological_space.second_countable_topology E] [complete_space E] [normed_space E] {β : Type u_2} [measurable_space β] {g : α → β} {f : β → E} {s : set β} :
is_measurable smeasurable fmeasurable g (y : β) in s, f y (measure_theory.measure.map g) μ = (x : α) in g ⁻¹' s, f (g x) μ

theorem measure_theory.norm_set_integral_le_of_norm_le_const_ae {α : Type u_1} {E : Type u_3} [measurable_space α] [normed_group E] [measurable_space E] {f : α → E} {s : set α} {μ : measure_theory.measure α} [borel_space E] [topological_space.second_countable_topology E] [complete_space E] [normed_space E] {C : } :
μ s < (∀ᵐ (x : α) ∂μ.restrict s, f x C) (x : α) in s, f x μ C * (μ s).to_real

theorem measure_theory.norm_set_integral_le_of_norm_le_const_ae' {α : Type u_1} {E : Type u_3} [measurable_space α] [normed_group E] [measurable_space E] {f : α → E} {s : set α} {μ : measure_theory.measure α} [borel_space E] [topological_space.second_countable_topology E] [complete_space E] [normed_space E] {C : } :
μ s < (∀ᵐ (x : α) ∂μ, x sf x C)measurable f (x : α) in s, f x μ C * (μ s).to_real

theorem measure_theory.norm_set_integral_le_of_norm_le_const_ae'' {α : Type u_1} {E : Type u_3} [measurable_space α] [normed_group E] [measurable_space E] {f : α → E} {s : set α} {μ : measure_theory.measure α} [borel_space E] [topological_space.second_countable_topology E] [complete_space E] [normed_space E] {C : } :
μ s < is_measurable s(∀ᵐ (x : α) ∂μ, x sf x C) (x : α) in s, f x μ C * (μ s).to_real

theorem measure_theory.norm_set_integral_le_of_norm_le_const {α : Type u_1} {E : Type u_3} [measurable_space α] [normed_group E] [measurable_space E] {f : α → E} {s : set α} {μ : measure_theory.measure α} [borel_space E] [topological_space.second_countable_topology E] [complete_space E] [normed_space E] {C : } :
μ s < (∀ (x : α), x sf x C)measurable f (x : α) in s, f x μ C * (μ s).to_real

theorem measure_theory.norm_set_integral_le_of_norm_le_const' {α : Type u_1} {E : Type u_3} [measurable_space α] [normed_group E] [measurable_space E] {f : α → E} {s : set α} {μ : measure_theory.measure α} [borel_space E] [topological_space.second_countable_topology E] [complete_space E] [normed_space E] {C : } :
μ s < is_measurable s(∀ (x : α), x sf x C) (x : α) in s, f x μ C * (μ s).to_real

theorem measure_theory.set_integral_eq_zero_iff_of_nonneg_ae {α : Type u_1} [measurable_space α] {s : set α} {μ : measure_theory.measure α} {f : α → } :
0 ≤ᵐ[μ.restrict s] fmeasure_theory.integrable_on f s μ( (x : α) in s, f x μ = 0 f =ᵐ[μ.restrict s] 0)

theorem measure_theory.set_integral_pos_iff_support_of_nonneg_ae {α : Type u_1} [measurable_space α] {s : set α} {μ : measure_theory.measure α} {f : α → } :
0 ≤ᵐ[μ.restrict s] fmeasure_theory.integrable_on f s μ(0 < (x : α) in s, f x μ 0 < μ (function.support f s))

theorem filter.tendsto.integral_sub_linear_is_o_ae {α : Type u_1} {E : Type u_3} [measurable_space α] [measurable_space E] [normed_group E] [normed_space E] [topological_space.second_countable_topology E] [complete_space E] [borel_space E] {μ : measure_theory.measure α} {l : filter α} [l.is_measurably_generated] {f : α → E} {b : E} :
filter.tendsto f (l μ.ae) (𝓝 b)measurable fμ.finite_at_filter lasymptotics.is_o (λ (s : set α), (x : α) in s, f x μ - (μ s).to_real b) (λ (s : set α), (μ s).to_real) (l.lift' set.powerset)

Fundamental theorem of calculus for set integrals: if μ is a measure that is finite at a filter l and f is a measurable function that has a finite limit b at l ⊓ μ.ae, then ∫ x in s, f x ∂μ = μ s • b + o(μ s) as s tends to l.lift' powerset. Since μ s is an ennreal number, we use (μ s).to_real in the actual statement.

theorem is_compact.integrable_on_of_nhds_within {α : Type u_1} {E : Type u_3} [measurable_space α] [measurable_space E] [normed_group E] [topological_space α] {μ : measure_theory.measure α} {s : set α} (hs : is_compact s) {f : α → E} :
measurable f(∀ (x : α), x smeasure_theory.integrable_at_filter f (𝓝[s] x) μ)measure_theory.integrable_on f s μ

If a function is integrable at 𝓝[s] x for each point x of a compact set s, then it is integrable on s.

A function f continuous on a compact set s is integrable on this set with respect to any locally finite measure.

A continuous function f is integrable on any compact set with respect to any locally finite measure.

A continuous function with compact closure of the support is integrable on the whole space.

Fundamental theorem of calculus for set integrals, nhds version: if μ is a locally finite measure that and f is a measurable function that is continuous at a point a, then ∫ x in s, f x ∂μ = μ s • f a + o(μ s) as s tends to (𝓝 a).lift' powerset. Since μ s is an ennreal number, we use (μ s).to_real in the actual statement.

### Continuous linear maps composed with integration

The goal of this section is to prove that integration commutes with continuous linear maps. The first step is to prove that, given a function φ : α → E which is measurable and integrable, and a continuous linear map L : E →L[ℝ] F, the function λ a, L(φ a) is also measurable and integrable. Note we cannot write this as L ∘ φ since the type of L is not an actual function type.

The next step is translate this to l1, replacing the function φ by a term with type α →₁[μ] E (an equivalence class of integrable functions). The corresponding "composition" is L.comp_l1 φ : α →₁[μ] F. This is then upgraded to a linear map L.comp_l1ₗ : (α →₁[μ] E) →ₗ[ℝ] (α →₁[μ] F) and a continuous linear map L.comp_l1L : (α →₁[μ] E) →L[ℝ] (α →₁[μ] F).

Then we can prove the commutation result using continuity of all relevant operations and the result on simple functions.

theorem continuous_linear_map.norm_comp_l1_apply_le {α : Type u_1} {E : Type u_3} {F : Type u_4} [measurable_space α] [measurable_space E] [normed_group E] {μ : measure_theory.measure α} [normed_space E] [normed_group F] [normed_space F] [opens_measurable_space E] [topological_space.second_countable_topology E] (φ : α →₁[μ] E) (L : E →L[] F) :
∀ᵐ (a : α) ∂μ, L (φ a) L * φ a

theorem continuous_linear_map.integrable_comp {α : Type u_1} {E : Type u_3} {F : Type u_4} [measurable_space α] [measurable_space E] [normed_group E] {μ : measure_theory.measure α} [normed_space E] [normed_group F] [normed_space F] [measurable_space F] [borel_space F] [opens_measurable_space E] {φ : α → E} (L : E →L[] F) :
measure_theory.integrable φ μmeasure_theory.integrable (λ (a : α), L (φ a)) μ

Composing φ : α →₁[μ] E with L : E →L[ℝ] F.

Equations

Composing φ : α →₁[μ] E with L : E →L[ℝ] F, seen as a -linear map on α →₁[μ] E.

Equations

Composing φ : α →₁[μ] E with L : E →L[ℝ] F, seen as a continuous -linear map on α →₁[μ] E.

Equations
theorem integral_pair {α : Type u_1} {E : Type u_3} {F : Type u_4} [measurable_space α] [measurable_space E] [normed_group E] {μ : measure_theory.measure α} [normed_space E] [normed_group F] [normed_space F] [borel_space E] [topological_space.second_countable_topology E] [complete_space E] [measurable_space F] [borel_space F] [topological_space.second_countable_topology F] [complete_space F] {f : α → E} {g : α → F} :
measure_theory.integrable f μmeasure_theory.integrable g μ (x : α), (f x, g x) μ = ( (x : α), f x μ, (x : α), g x μ)

theorem integral_smul_const {α : Type u_1} {E : Type u_3} [measurable_space α] [measurable_space E] [normed_group E] {μ : measure_theory.measure α} [normed_space E] [borel_space E] [topological_space.second_countable_topology E] [complete_space E] (f : α → ) (c : E) :
(x : α), f x c μ = ( (x : α), f x μ) c