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 : α → β} (hs : is_measurable s) :

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

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

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

def measurable_at_filter {α : Type u_1} {β : Type u_2} [measurable_space α] [measurable_space β] (f : α → β) (l : filter α) (μ : measure_theory.measure α . "volume_tac") :
Prop

A function f is measurable at filter l w.r.t. a measure μ if it is ae-measurable w.r.t. μ.restrict s for some s ∈ l.

Equations
@[simp]
theorem measurable_at_bot {α : Type u_1} {β : Type u_2} [measurable_space α] [measurable_space β] {μ : measure_theory.measure α} {f : α → β} :

theorem measurable_at_filter.eventually {α : Type u_1} {β : Type u_2} [measurable_space α] [measurable_space β] {l : filter α} {f : α → β} {μ : measure_theory.measure α} (h : measurable_at_filter f l μ) :
∀ᶠ (s : set α) in l.lift' set.powerset, ae_measurable f (μ.restrict s)

theorem measurable_at_filter.filter_mono {α : Type u_1} {β : Type u_2} [measurable_space α] [measurable_space β] {l l' : filter α} {f : α → β} {μ : measure_theory.measure α} (h : measurable_at_filter f l μ) (h' : l' l) :

theorem ae_measurable.measurable_at_filter {α : Type u_1} {β : Type u_2} [measurable_space α] [measurable_space β] {l : filter α} {f : α → β} {μ : measure_theory.measure α} (h : ae_measurable f μ) :

theorem ae_measurable.measurable_at_filter_of_mem {α : Type u_1} {β : Type u_2} [measurable_space α] [measurable_space β] {l : filter α} {f : α → β} {μ : measure_theory.measure α} {s : set α} (h : ae_measurable f (μ.restrict s)) (hl : s l) :

theorem measurable.measurable_at_filter {α : Type u_1} {β : Type u_2} [measurable_space α] [measurable_space β] {l : filter α} {f : α → β} {μ : measure_theory.measure α} (h : measurable 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 : } (hs : μ s < ) (hf : ∀ᵐ (x : α) ∂μ.restrict s, f x C) :

def measure_theory.integrable_on {α : Type u_1} {E : Type u_3} [measurable_space α] [normed_group E] [measurable_space E] (f : α → E) (s : 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 α} (h : measure_theory.integrable_on f s μ) :

@[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 α} (h : measure_theory.integrable_on f t ν) (hs : s t) (hμ : μ ν) :

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 α} (h : measure_theory.integrable_on f t μ) (hst : s t) :

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 α} (h : measure_theory.integrable_on f s ν) (hμ : μ ν) :

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 α} (h : measure_theory.integrable_on f t μ) (hst : s ≤ᵐ[μ] t) :

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 α} (h : measure_theory.integrable f μ) :

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 α} (h : measure_theory.integrable f (μ.restrict s)) :

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 α} (h : measure_theory.integrable_on f (s t) μ) :

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 α} (h : measure_theory.integrable_on f (s t) μ) :

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 α} (hs : measure_theory.integrable_on f s μ) (ht : measure_theory.integrable_on f t μ) :

@[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 α} {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 α} {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 α} (hμ : measure_theory.integrable_on f s μ) (hν : measure_theory.integrable_on f s ν) :

@[simp]

theorem measure_theory.ae_measurable_indicator_iff {α : Type u_1} {E : Type u_3} [measurable_space α] [normed_group E] [measurable_space E] {f : α → E} {s : set α} {μ : measure_theory.measure α} (hs : is_measurable s) :

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 α} (h : measure_theory.integrable_on f s μ) (hs : is_measurable s) :

def measure_theory.integrable_at_filter {α : Type u_1} {E : Type u_3} [measurable_space α] [normed_group E] [measurable_space E] (f : α → E) (l : 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 α} (h : measure_theory.integrable_at_filter f l μ) :
∀ᶠ (s : set α) in l.lift' set.powerset, measure_theory.integrable_on f s μ

theorem measure_theory.integrable_at_filter.filter_mono {α : Type u_1} {E : Type u_3} [measurable_space α] [normed_group E] [measurable_space E] {f : α → E} {μ : measure_theory.measure α} {l l' : filter α} (hl : l l') (hl' : measure_theory.integrable_at_filter f l' μ) :

Alias of integrable_at_filter.inf_ae_iff.

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 filter.tendsto.integrable_at_filter_ae {α : Type u_1} {E : Type u_3} [measurable_space α] [normed_group E] [measurable_space E] {f : α → E} {μ : measure_theory.measure α} {l : filter α} [l.is_measurably_generated] (hfm : measurable_at_filter f l μ) (hμ : μ.finite_at_filter l) {b : E} (hf : filter.tendsto f (l μ.ae) (𝓝 b)) :

Alias of measure.finite_at_filter.integrable_at_filter_of_tendsto_ae.

theorem filter.tendsto.integrable_at_filter {α : Type u_1} {E : Type u_3} [measurable_space α] [normed_group E] [measurable_space E] {f : α → E} {μ : measure_theory.measure α} {l : filter α} [l.is_measurably_generated] (hfm : measurable_at_filter f l μ) (hμ : μ.finite_at_filter l) {b : E} (hf : filter.tendsto f l (𝓝 b)) :

Alias of measure.finite_at_filter.integrable_at_filter_of_tendsto.

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 μP fP g) ⦃f : α → E⦄ (hf : measure_theory.integrable f μ) :
P f

To prove something for an arbitrary 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.set_integral_congr_ae {α : Type u_1} {E : Type u_3} [measurable_space α] [normed_group E] [measurable_space E] {f g : α → E} {s : set α} {μ : measure_theory.measure α} [borel_space E] [topological_space.second_countable_topology E] [complete_space E] [normed_space E] (hs : is_measurable s) (h : ∀ᵐ (x : α) ∂μ, x sf x = g x) :
(x : α) in s, f x μ = (x : α) in s, g x μ

theorem measure_theory.set_integral_congr {α : Type u_1} {E : Type u_3} [measurable_space α] [normed_group E] [measurable_space E] {f g : α → E} {s : set α} {μ : measure_theory.measure α} [borel_space E] [topological_space.second_countable_topology E] [complete_space E] [normed_space E] (hs : is_measurable s) (h : set.eq_on f g s) :
(x : α) in s, f x μ = (x : α) in s, g x μ

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] (hst : disjoint s t) (hs : is_measurable s) (ht : is_measurable t) (hfs : measure_theory.integrable_on f s μ) (hft : 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] (hs : is_measurable s) (hfi : measure_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] (hs : is_measurable s) :
(x : α), s.indicator f x μ = (x : α) in s, f x μ

For a 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 α⦄ (s_meas : 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 β} (hs : is_measurable s) (hf : ae_measurable f ((measure_theory.measure.map g) μ)) (hg : measurable 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 : } (hs : μ s < ) (hC : ∀ᵐ (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 : } (hs : μ s < ) (hC : ∀ᵐ (x : α) ∂μ, x sf x C) (hfm : ae_measurable f (μ.restrict s)) :
(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 : } (hs : μ s < ) (hsm : is_measurable s) (hC : ∀ᵐ (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 : } (hs : μ s < ) (hC : ∀ (x : α), x sf x C) (hfm : ae_measurable f (μ.restrict s)) :
(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 : } (hs : μ s < ) (hsm : is_measurable s) (hC : ∀ (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 : α → } (hf : 0 ≤ᵐ[μ.restrict s] f) (hfi : measure_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 : α → } (hf : 0 ≤ᵐ[μ.restrict s] f) (hfi : measure_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 α] {ι : Type u_5} [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} (h : filter.tendsto f (l μ.ae) (𝓝 b)) (hfm : measurable_at_filter f l μ) (hμ : μ.finite_at_filter l) {s : ι → set α} {li : filter ι} (hs : filter.tendsto s li (l.lift' set.powerset)) (m : ι → := λ (i : ι), (μ (s i)).to_real) (hsμ : (λ (i : ι), (μ (s i)).to_real) =ᶠ[li] m . "refl") :
asymptotics.is_o (λ (i : ι), (x : α) in s i, f x μ - m i b) m li

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 i, f x ∂μ = μ (s i) • b + o(μ (s i)) at a filter li provided that s i tends to l.lift' powerset along li. Since μ (s i) is an ennreal number, we use (μ (s i)).to_real in the actual statement.

Often there is a good formula for (μ (s i)).to_real, so the formalization can take an optional argument m with this formula and a proof of(λ i, (μ (s i)).to_real) =ᶠ[li] m. Without these arguments,m i = (μ (s i)).to_real` is used in the output.

theorem continuous_within_at.integral_sub_linear_is_o_ae {α : Type u_1} {E : Type u_3} [measurable_space α] {ι : Type u_5} [measurable_space E] [normed_group E] [topological_space α] [opens_measurable_space α] [normed_space E] [topological_space.second_countable_topology E] [complete_space E] [borel_space E] {μ : measure_theory.measure α} [measure_theory.locally_finite_measure μ] {a : α} {t : set α} {f : α → E} (ha : continuous_within_at f t a) (ht : is_measurable t) (hfm : measurable_at_filter f (𝓝[t] a) μ) {s : ι → set α} {li : filter ι} (hs : filter.tendsto s li ((𝓝[t] a).lift' set.powerset)) (m : ι → := λ (i : ι), (μ (s i)).to_real) (hsμ : (λ (i : ι), (μ (s i)).to_real) =ᶠ[li] m . "refl") :
asymptotics.is_o (λ (i : ι), (x : α) in s i, f x μ - m i f a) m li

Fundamental theorem of calculus for set integrals, nhds_within version: if μ is a locally finite measure and f is an almost everywhere measurable function that is continuous at a point a within a measurable set t, then ∫ x in s i, f x ∂μ = μ (s i) • f a + o(μ (s i)) at a filter li provided that s i tends to (𝓝[t] a).lift' powerset along li. Since μ (s i) is an ennreal number, we use (μ (s i)).to_real in the actual statement.

Often there is a good formula for (μ (s i)).to_real, so the formalization can take an optional argument m with this formula and a proof of(λ i, (μ (s i)).to_real) =ᶠ[li] m. Without these arguments,m i = (μ (s i)).to_real` is used in the output.

theorem continuous_at.integral_sub_linear_is_o_ae {α : Type u_1} {E : Type u_3} [measurable_space α] {ι : Type u_5} [measurable_space E] [normed_group E] [topological_space α] [opens_measurable_space α] [normed_space E] [topological_space.second_countable_topology E] [complete_space E] [borel_space E] {μ : measure_theory.measure α} [measure_theory.locally_finite_measure μ] {a : α} {f : α → E} (ha : continuous_at f a) (hfm : measurable_at_filter f (𝓝 a) μ) {s : ι → set α} {li : filter ι} (hs : filter.tendsto s li ((𝓝 a).lift' set.powerset)) (m : ι → := λ (i : ι), (μ (s i)).to_real) (hsμ : (λ (i : ι), (μ (s i)).to_real) =ᶠ[li] m . "refl") :
asymptotics.is_o (λ (i : ι), (x : α) in s i, f x μ - m i f a) m li

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

Often there is a good formula for (μ (s i)).to_real, so the formalization can take an optional argument m with this formula and a proof of(λ i, (μ (s i)).to_real) =ᶠ[li] m. Without these arguments,m i = (μ (s i)).to_real` is used in the output.

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} (hf : ∀ (x : α), x smeasure_theory.integrable_at_filter f (𝓝[s] x) μ) :

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

theorem continuous_on.ae_measurable {α : Type u_1} {E : Type u_3} [measurable_space α] [measurable_space E] [normed_group E] [topological_space α] [opens_measurable_space α] [borel_space E] {f : α → E} {s : set α} {μ : measure_theory.measure α} (hf : continuous_on f s) (hs : is_measurable s) :

A function which is continuous on a set s is almost everywhere measurable with respect to μ.restrict s.

theorem continuous_on.integral_sub_linear_is_o_ae {α : Type u_1} {E : Type u_3} [measurable_space α] {ι : Type u_5} [measurable_space E] [normed_group E] [topological_space α] [opens_measurable_space α] [normed_space E] [topological_space.second_countable_topology E] [complete_space E] [borel_space E] {μ : measure_theory.measure α} [measure_theory.locally_finite_measure μ] {a : α} {t : set α} {f : α → E} (hft : continuous_on f t) (ha : a t) (ht : is_measurable t) {s : ι → set α} {li : filter ι} (hs : filter.tendsto s li ((𝓝[t] a).lift' set.powerset)) (m : ι → := λ (i : ι), (μ (s i)).to_real) (hsμ : (λ (i : ι), (μ (s i)).to_real) =ᶠ[li] m . "refl") :
asymptotics.is_o (λ (i : ι), (x : α) in s i, f x μ - m i f a) m li

Fundamental theorem of calculus for set integrals, nhds_within version: if μ is a locally finite measure, f is continuous on a measurable set t, and a ∈ t, then ∫ x in (s i), f x ∂μ = μ (s i) • f a + o(μ (s i)) at li provided that s i tends to (𝓝[t] a).lift' powerset along li. Since μ (s i) is an ennreal number, we use (μ (s i)).to_real in the actual statement.

Often there is a good formula for (μ (s i)).to_real, so the formalization can take an optional argument m with this formula and a proof of(λ i, (μ (s i)).to_real) =ᶠ[li] m. Without these arguments,m i = (μ (s i)).to_real` is used in the output.

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.

### 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) (φ_int : 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} (hf : measure_theory.integrable f μ) (hg : 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