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 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 : α → β} :
is_measurable s → s.piecewise f g =ᵐ[μ.restrict s] f
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 : α → β} :
is_measurable s → s.indicator f =ᵐ[μ.restrict s] f
theorem
indicator_ae_eq_restrict_compl
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
[has_zero β]
{μ : measure_theory.measure α}
{s : set α}
{f : α → β} :
def
measure_theory.integrable_on
{α : Type u_1}
{E : Type u_3}
[measurable_space α]
[normed_group E] :
(α → E) → set α → (measure_theory.measure α . "volume_tac") → Prop
A function is integrable_on a set s 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]
{f : α → E}
{s : set α}
{μ : measure_theory.measure α} :
measure_theory.integrable_on f s μ → measure_theory.integrable f (μ.restrict s)
@[simp]
theorem
measure_theory.integrable_on_empty
{α : Type u_1}
{E : Type u_3}
[measurable_space α]
[normed_group E]
{f : α → E}
{μ : measure_theory.measure α} :
@[simp]
theorem
measure_theory.integrable_on_univ
{α : Type u_1}
{E : Type u_3}
[measurable_space α]
[normed_group E]
{f : α → E}
{μ : measure_theory.measure α} :
theorem
measure_theory.integrable_on_zero
{α : Type u_1}
{E : Type u_3}
[measurable_space α]
[normed_group 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]
{s : set α}
{μ : measure_theory.measure α}
{C : E} :
theorem
measure_theory.integrable_on.mono
{α : Type u_1}
{E : Type u_3}
[measurable_space α]
[normed_group E]
{f : α → E}
{s t : set α}
{μ ν : measure_theory.measure α} :
measure_theory.integrable_on f t ν → s ⊆ t → μ ≤ ν → measure_theory.integrable_on f s μ
theorem
measure_theory.integrable_on.mono_set
{α : Type u_1}
{E : Type u_3}
[measurable_space α]
[normed_group E]
{f : α → E}
{s t : set α}
{μ : measure_theory.measure α} :
measure_theory.integrable_on f t μ → s ⊆ t → measure_theory.integrable_on f s μ
theorem
measure_theory.integrable_on.mono_measure
{α : Type u_1}
{E : Type u_3}
[measurable_space α]
[normed_group E]
{f : α → E}
{s : set α}
{μ ν : measure_theory.measure α} :
measure_theory.integrable_on f s ν → μ ≤ ν → measure_theory.integrable_on f s μ
theorem
measure_theory.integrable_on.mono_set_ae
{α : Type u_1}
{E : Type u_3}
[measurable_space α]
[normed_group E]
{f : α → E}
{s t : set α}
{μ : measure_theory.measure α} :
measure_theory.integrable_on f t μ → s ≤ᵐ[μ] t → measure_theory.integrable_on f s μ
theorem
measure_theory.integrable.integrable_on
{α : Type u_1}
{E : Type u_3}
[measurable_space α]
[normed_group 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]
{f : α → E}
{s : set α}
{μ : measure_theory.measure α} :
measure_theory.integrable f (μ.restrict s) → measure_theory.integrable_on f s μ
theorem
measure_theory.integrable_on.left_of_union
{α : Type u_1}
{E : Type u_3}
[measurable_space α]
[normed_group E]
{f : α → E}
{s t : set α}
{μ : measure_theory.measure α} :
measure_theory.integrable_on f (s ∪ t) μ → measure_theory.integrable_on f s μ
theorem
measure_theory.integrable_on.right_of_union
{α : Type u_1}
{E : Type u_3}
[measurable_space α]
[normed_group E]
{f : α → E}
{s t : set α}
{μ : measure_theory.measure α} :
measure_theory.integrable_on f (s ∪ t) μ → measure_theory.integrable_on f t μ
theorem
measure_theory.integrable_on.union
{α : Type u_1}
{E : Type u_3}
[measurable_space α]
[normed_group E]
{f : α → E}
{s t : set α}
{μ : measure_theory.measure α} :
measure_theory.integrable_on f s μ → measure_theory.integrable_on f t μ → measure_theory.integrable_on f (s ∪ t) μ
@[simp]
theorem
measure_theory.integrable_on_union
{α : Type u_1}
{E : Type u_3}
[measurable_space α]
[normed_group E]
{f : α → E}
{s t : set α}
{μ : measure_theory.measure α} :
measure_theory.integrable_on f (s ∪ t) μ ↔ measure_theory.integrable_on f s μ ∧ measure_theory.integrable_on f t μ
@[simp]
theorem
measure_theory.integrable_on_finite_union
{α : Type u_1}
{β : Type u_2}
{E : Type u_3}
[measurable_space α]
[normed_group 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 ∈ s → measure_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]
{f : α → E}
{μ : measure_theory.measure α}
{s : finset β}
{t : β → set α} :
measure_theory.integrable_on f (⋃ (i : β) (H : i ∈ s), t i) μ ↔ ∀ (i : β), i ∈ s → measure_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]
{f : α → E}
{s : set α}
{μ ν : measure_theory.measure α} :
measure_theory.integrable_on f s μ → measure_theory.integrable_on f s ν → measure_theory.integrable_on f s (μ + ν)
@[simp]
theorem
measure_theory.integrable_on_add_measure
{α : Type u_1}
{E : Type u_3}
[measurable_space α]
[normed_group E]
{f : α → E}
{s : set α}
{μ ν : measure_theory.measure α} :
measure_theory.integrable_on f s (μ + ν) ↔ measure_theory.integrable_on f s μ ∧ measure_theory.integrable_on f s ν
theorem
measure_theory.integrable_indicator_iff
{α : Type u_1}
{E : Type u_3}
[measurable_space α]
[normed_group E]
{f : α → E}
{s : set α}
{μ : measure_theory.measure α} :
is_measurable s → (measure_theory.integrable (s.indicator f) μ ↔ measure_theory.integrable_on f s μ)
theorem
measure_theory.integrable_on.indicator
{α : Type u_1}
{E : Type u_3}
[measurable_space α]
[normed_group E]
{f : α → E}
{s : set α}
{μ : measure_theory.measure α} :
measure_theory.integrable_on f s μ → is_measurable s → measure_theory.integrable (s.indicator f) μ
theorem
measure_theory.integrable_on_of_bounded
{α : Type u_1}
{E : Type u_3}
[measurable_space α]
[normed_group E]
{f : α → E}
{s : set α}
{μ : measure_theory.measure α}
{C : ℝ} :
def
measure_theory.integrable_at_filter
{α : Type u_1}
{E : Type u_3}
[measurable_space α]
[normed_group 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
- measure_theory.integrable_at_filter f l μ = ∃ (s : set α) (H : s ∈ l), measure_theory.integrable_on f s μ
theorem
measure_theory.integrable_at_filter.eventually
{α : Type u_1}
{E : Type u_3}
[measurable_space α]
[normed_group E]
{f : α → E}
{μ : measure_theory.measure α}
{l : filter α} :
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]
{f : α → E}
{μ : measure_theory.measure α}
{l l' : filter α} :
l ≤ l' → measure_theory.integrable_at_filter f l' μ → measure_theory.integrable_at_filter f l μ
theorem
measure_theory.integrable_at_filter.inf_of_left
{α : Type u_1}
{E : Type u_3}
[measurable_space α]
[normed_group E]
{f : α → E}
{μ : measure_theory.measure α}
{l l' : filter α} :
measure_theory.integrable_at_filter f l μ → measure_theory.integrable_at_filter f (l ⊓ l') μ
theorem
measure_theory.integrable_at_filter.inf_of_right
{α : Type u_1}
{E : Type u_3}
[measurable_space α]
[normed_group E]
{f : α → E}
{μ : measure_theory.measure α}
{l l' : filter α} :
measure_theory.integrable_at_filter f l μ → measure_theory.integrable_at_filter f (l' ⊓ l) μ
@[simp]
theorem
measure_theory.integrable_at_filter.inf_ae_iff
{α : Type u_1}
{E : Type u_3}
[measurable_space α]
[normed_group E]
{f : α → E}
{μ : measure_theory.measure α}
{l : filter α} :
measure_theory.integrable_at_filter f (l ⊓ μ.ae) μ ↔ measure_theory.integrable_at_filter f l μ
theorem
measure_theory.measure.finite_at_filter.integrable_at_filter
{α : Type u_1}
{E : Type u_3}
[measurable_space α]
[normed_group E]
{f : α → E}
{μ : measure_theory.measure α}
{l : filter α}
[l.is_measurably_generated] :
μ.finite_at_filter l → filter.is_bounded_under has_le.le l (has_norm.norm ∘ f) → measure_theory.integrable_at_filter f l μ
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.measure.finite_at_filter.integrable_at_filter_of_tendsto_ae
{α : Type u_1}
{E : Type u_3}
[measurable_space α]
[normed_group E]
{f : α → E}
{μ : measure_theory.measure α}
{l : filter α}
[l.is_measurably_generated]
(hμ : μ.finite_at_filter l)
{b : E} :
filter.tendsto f (l ⊓ μ.ae) (nhds b) → measure_theory.integrable_at_filter f l μ
theorem
measure_theory.measure.finite_at_filter.integrable_at_filter_of_tendsto
{α : Type u_1}
{E : Type u_3}
[measurable_space α]
[normed_group E]
{f : α → E}
{μ : measure_theory.measure α}
{l : filter α}
[l.is_measurably_generated]
(hμ : μ.finite_at_filter l)
{b : E} :
filter.tendsto f l (nhds b) → measure_theory.integrable_at_filter f l μ
theorem
measure_theory.integral_union
{α : Type u_1}
{E : Type u_3}
[measurable_space α]
[normed_group E]
{f : α → E}
{s t : set α}
{μ : measure_theory.measure α}
[measurable_space E]
[borel_space E]
[complete_space E]
[topological_space.second_countable_topology E]
[normed_space ℝ E] :
disjoint s t → is_measurable s → is_measurable t → measure_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_empty
{α : Type u_1}
{E : Type u_3}
[measurable_space α]
[normed_group E]
{f : α → E}
{μ : measure_theory.measure α}
[measurable_space E]
[borel_space E]
[complete_space E]
[topological_space.second_countable_topology E]
[normed_space ℝ E] :
theorem
measure_theory.integral_univ
{α : Type u_1}
{E : Type u_3}
[measurable_space α]
[normed_group E]
{f : α → E}
{μ : measure_theory.measure α}
[measurable_space E]
[borel_space E]
[complete_space E]
[topological_space.second_countable_topology E]
[normed_space ℝ E] :
theorem
measure_theory.integral_add_compl
{α : Type u_1}
{E : Type u_3}
[measurable_space α]
[normed_group E]
{f : α → E}
{s : set α}
{μ : measure_theory.measure α}
[measurable_space E]
[borel_space E]
[complete_space E]
[topological_space.second_countable_topology E]
[normed_space ℝ E] :
theorem
measure_theory.integral_indicator
{α : Type u_1}
{E : Type u_3}
[measurable_space α]
[normed_group E]
{f : α → E}
{s : set α}
{μ : measure_theory.measure α}
[measurable_space E]
[borel_space E]
[complete_space E]
[topological_space.second_countable_topology E]
[normed_space ℝ E] :
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).
theorem
measure_theory.set_integral_const
{α : Type u_1}
{E : Type u_3}
[measurable_space α]
[normed_group E]
{s : set α}
{μ : measure_theory.measure α}
[measurable_space E]
[borel_space E]
[complete_space E]
[topological_space.second_countable_topology E]
[normed_space ℝ E]
(c : E) :
theorem
measure_theory.norm_set_integral_le_of_norm_le_const_ae
{α : Type u_1}
{E : Type u_3}
[measurable_space α]
[normed_group E]
{f : α → E}
{s : set α}
{μ : measure_theory.measure α}
[measurable_space E]
[borel_space E]
[complete_space E]
[topological_space.second_countable_topology E]
[normed_space ℝ E]
{C : ℝ} :
theorem
measure_theory.norm_set_integral_le_of_norm_le_const_ae'
{α : Type u_1}
{E : Type u_3}
[measurable_space α]
[normed_group E]
{f : α → E}
{s : set α}
{μ : measure_theory.measure α}
[measurable_space E]
[borel_space E]
[complete_space E]
[topological_space.second_countable_topology E]
[normed_space ℝ E]
{C : ℝ} :
theorem
measure_theory.norm_set_integral_le_of_norm_le_const_ae''
{α : Type u_1}
{E : Type u_3}
[measurable_space α]
[normed_group E]
{f : α → E}
{s : set α}
{μ : measure_theory.measure α}
[measurable_space E]
[borel_space E]
[complete_space E]
[topological_space.second_countable_topology E]
[normed_space ℝ E]
{C : ℝ} :
theorem
measure_theory.norm_set_integral_le_of_norm_le_const
{α : Type u_1}
{E : Type u_3}
[measurable_space α]
[normed_group E]
{f : α → E}
{s : set α}
{μ : measure_theory.measure α}
[measurable_space E]
[borel_space E]
[complete_space E]
[topological_space.second_countable_topology E]
[normed_space ℝ E]
{C : ℝ} :
theorem
measure_theory.norm_set_integral_le_of_norm_le_const'
{α : Type u_1}
{E : Type u_3}
[measurable_space α]
[normed_group E]
{f : α → E}
{s : set α}
{μ : measure_theory.measure α}
[measurable_space E]
[borel_space E]
[complete_space E]
[topological_space.second_countable_topology E]
[normed_space ℝ E]
{C : ℝ} :
theorem
filter.tendsto.integral_sub_linear_is_o_ae
{α : Type u_1}
{E : Type u_3}
[measurable_space α]
[normed_group E]
[normed_space ℝ E]
[topological_space.second_countable_topology E]
[complete_space E]
[measurable_space E]
[borel_space E]
{μ : measure_theory.measure α}
{l : filter α}
[l.is_measurably_generated]
{f : α → E}
{b : E} :
filter.tendsto f (l ⊓ μ.ae) (nhds b) → measurable f → μ.finite_at_filter l → asymptotics.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 α]
[topological_space α]
[normed_group E]
{μ : measure_theory.measure α}
{s : set α}
(hs : is_compact s)
{f : α → E} :
(∀ (x : α), x ∈ s → measure_theory.integrable_at_filter f (nhds_within x s) μ) → 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.
theorem
continuous_on.integrable_on_compact
{α : Type u_1}
{E : Type u_3}
[measurable_space α]
[topological_space α]
[opens_measurable_space α]
[t2_space α]
[normed_group E]
{μ : measure_theory.measure α}
[measure_theory.locally_finite_measure μ]
{s : set α}
(hs : is_compact s)
{f : α → E} :
continuous_on f s → measure_theory.integrable_on f s μ
A function f continuous on a compact set s is integrable on this set with respect to any
locally finite measure.
theorem
continuous.integrable_on_compact
{α : Type u_1}
{E : Type u_3}
[measurable_space α]
[topological_space α]
[opens_measurable_space α]
[t2_space α]
[normed_group E]
{μ : measure_theory.measure α}
[measure_theory.locally_finite_measure μ]
{s : set α}
(hs : is_compact s)
{f : α → E} :
continuous f → measure_theory.integrable_on f s μ
A continuous function f is integrable on any compact set with respect to any locally finite
measure.
theorem
continuous_at.integral_sub_linear_is_o_ae
{α : Type u_1}
{E : Type u_3}
[measurable_space α]
[topological_space α]
[opens_measurable_space α]
[normed_group E]
[normed_space ℝ E]
[topological_space.second_countable_topology E]
[complete_space E]
[measurable_space E]
[borel_space E]
{μ : measure_theory.measure α}
[measure_theory.locally_finite_measure μ]
{a : α}
{f : α → E} :
continuous_at f a → measurable f → asymptotics.is_o (λ (s : set α), ∫ (x : α) in s, f x ∂μ - (⇑μ s).to_real • f a) (λ (s : set α), (⇑μ s).to_real) ((nhds a).lift' set.powerset)
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.