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) :
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 μ) :
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]
[measurable_space E]
{f : α → E}
{μ : measure_theory.measure α}
(hf : measurable f) :
@[simp]
theorem
measure_theory.integrable_on_univ
{α : 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} :
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 μ) :
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]
[measurable_space 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]
[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 ∈ 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]
[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 ∈ 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]
[measurable_space E]
{f : α → E}
{s : set α}
{μ ν : measure_theory.measure α}
(hμ : measure_theory.integrable_on f s μ)
(hν : 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]
[measurable_space 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]
[measurable_space E]
{f : α → E}
{s : set α}
{μ : measure_theory.measure α}
(hf : measurable f)
(hs : 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]
[measurable_space E]
{f : α → E}
{s : set α}
{μ : measure_theory.measure α}
(h : measure_theory.integrable_on f s μ)
(hs : is_measurable s) :
measure_theory.integrable (s.indicator f) μ
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
- 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]
[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' μ) :
theorem
measure_theory.integrable_at_filter.inf_of_left
{α : Type u_1}
{E : Type u_3}
[measurable_space α]
[normed_group E]
[measurable_space E]
{f : α → E}
{μ : measure_theory.measure α}
{l l' : filter α}
(hl : 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]
[measurable_space E]
{f : α → E}
{μ : measure_theory.measure α}
{l l' : filter α}
(hl : 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]
[measurable_space 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]
[measurable_space E]
{f : α → E}
{μ : measure_theory.measure α}
(hfm : measurable f)
{l : filter α}
[l.is_measurably_generated]
(hμ : μ.finite_at_filter l)
(hf : filter.is_bounded_under has_le.le l (norm ∘ f)) :
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]
[measurable_space E]
{f : α → E}
{μ : measure_theory.measure α}
(hfm : measurable f)
{l : filter α}
[l.is_measurably_generated]
(hμ : μ.finite_at_filter l)
{b : E}
(hf : filter.tendsto f (l ⊓ μ.ae) (𝓝 b)) :
theorem
measure_theory.measure.finite_at_filter.integrable_at_filter_of_tendsto
{α : Type u_1}
{E : Type u_3}
[measurable_space α]
[normed_group E]
[measurable_space E]
{f : α → E}
{μ : measure_theory.measure α}
(hfm : measurable f)
{l : filter α}
[l.is_measurably_generated]
(hμ : μ.finite_at_filter l)
{b : E}
(hf : filter.tendsto f l (𝓝 b)) :
theorem
measure_theory.integrable_add
{α : 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]
[opens_measurable_space E]
{f g : α → E}
(h : set.univ ⊆ f ⁻¹' {0} ∪ g ⁻¹' {0})
(hf : measurable f)
(hg : measurable g) :
measure_theory.integrable (f + g) μ ↔ measure_theory.integrable f μ ∧ measure_theory.integrable g μ
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 f → P g → P (f + g))
(h_closed : is_closed {f : α →₁[μ] E | P ⇑f})
(h_ae : ∀ ⦃f g : α → E⦄, f =ᵐ[μ] g → measure_theory.integrable f μ → measurable g → P f → P g)
⦃f : α → E⦄
(hf : measure_theory.integrable f μ) :
P f
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
L¹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]
(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 μ) :
theorem
measure_theory.integral_empty
{α : 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] :
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] :
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 μ) :
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]
(hfm : measurable f)
(hs : is_measurable s) :
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]
[measurable_space E]
{s : set α}
{μ : measure_theory.measure α}
[borel_space E]
[topological_space.second_countable_topology E]
[complete_space E]
[normed_space ℝ E]
(c : E) :
@[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) :
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 : measurable f)
(hg : measurable g) :
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) :
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 ∈ s → ∥f x∥ ≤ C)
(hfm : measurable f) :
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 ∈ s → ∥f x∥ ≤ C) :
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 ∈ s → ∥f x∥ ≤ C)
(hfm : measurable f) :
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 ∈ s → ∥f x∥ ≤ C) :
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}
(h : filter.tendsto f (l ⊓ μ.ae) (𝓝 b))
(hfm : measurable f)
(hμ : μ.finite_at_filter l) :
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}
(hfm : measurable f)
(hf : ∀ (x : α), x ∈ s → measure_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.integrable_on_compact
{α : Type u_1}
{E : Type u_3}
[measurable_space α]
[measurable_space E]
[normed_group E]
[topological_space α]
[opens_measurable_space α]
[t2_space α]
{μ : measure_theory.measure α}
[measure_theory.locally_finite_measure μ]
{s : set α}
(hs : is_compact s)
{f : α → E}
(hfm : measurable f)
(hf : continuous_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 α]
[measurable_space E]
[normed_group E]
[topological_space α]
[opens_measurable_space α]
[t2_space α]
[borel_space E]
{μ : measure_theory.measure α}
[measure_theory.locally_finite_measure μ]
{s : set α}
(hs : is_compact s)
{f : α → E}
(hf : continuous f) :
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 α]
[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 f) :
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) :
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)) μ
def
continuous_linear_map.comp_l1
{α : 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]
[borel_space E]
[topological_space.second_countable_topology E]
[topological_space.second_countable_topology F]
(L : E →L[ℝ] F)
(φ : α →₁[μ] E) :
Composing φ : α →₁[μ] E with L : E →L[ℝ] F.
Equations
- L.comp_l1 φ = measure_theory.l1.of_fun (λ (a : α), ⇑L (⇑φ a)) _
theorem
continuous_linear_map.comp_l1_apply
{α : 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]
[borel_space E]
[topological_space.second_countable_topology E]
[topological_space.second_countable_topology F]
(L : E →L[ℝ] F)
(φ : α →₁[μ] E) :
theorem
continuous_linear_map.integrable_comp_l1
{α : 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]
[borel_space E]
[topological_space.second_countable_topology E]
(L : E →L[ℝ] F)
(φ : α →₁[μ] E) :
measure_theory.integrable (λ (a : α), ⇑L (⇑φ a)) μ
theorem
continuous_linear_map.measurable_comp_l1
{α : 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]
[borel_space E]
[topological_space.second_countable_topology E]
(L : E →L[ℝ] F)
(φ : α →₁[μ] E) :
measurable (λ (a : α), ⇑L (⇑φ a))
theorem
continuous_linear_map.integral_comp_l1
{α : 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]
[borel_space E]
[topological_space.second_countable_topology E]
[topological_space.second_countable_topology F]
[complete_space F]
(L : E →L[ℝ] F)
(φ : α →₁[μ] E) :
def
continuous_linear_map.comp_l1ₗ
{α : 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]
[borel_space E]
[topological_space.second_countable_topology E]
[topological_space.second_countable_topology F]
(L : E →L[ℝ] F) :
Composing φ : α →₁[μ] E with L : E →L[ℝ] F, seen as a ℝ-linear map on α →₁[μ] E.
theorem
continuous_linear_map.norm_comp_l1_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]
[measurable_space F]
[borel_space F]
[borel_space E]
[topological_space.second_countable_topology E]
[topological_space.second_countable_topology F]
(φ : α →₁[μ] E)
(L : E →L[ℝ] F) :
def
continuous_linear_map.comp_l1L
{α : 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]
[borel_space E]
[topological_space.second_countable_topology E]
[topological_space.second_countable_topology F]
(L : E →L[ℝ] F) :
Composing φ : α →₁[μ] E with L : E →L[ℝ] F, seen as a continuous ℝ-linear map on
α →₁[μ] E.
theorem
continuous_linear_map.norm_compl1L_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]
[measurable_space F]
[borel_space F]
[borel_space E]
[topological_space.second_countable_topology E]
[topological_space.second_countable_topology F]
(L : E →L[ℝ] F) :
theorem
continuous_linear_map.continuous_integral_comp_l1
{α : 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]
[borel_space E]
[topological_space.second_countable_topology E]
[topological_space.second_countable_topology F]
[complete_space F]
(L : E →L[ℝ] F) :
theorem
continuous_linear_map.integral_comp_comm
{α : 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]
[borel_space E]
[topological_space.second_countable_topology E]
[topological_space.second_countable_topology F]
[complete_space F]
[complete_space E]
(L : E →L[ℝ] F)
{φ : α → E}
(φ_int : measure_theory.integrable φ μ) :
theorem
continuous_linear_map.integral_comp_l1_comm
{α : 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]
[borel_space E]
[topological_space.second_countable_topology E]
[topological_space.second_countable_topology F]
[complete_space F]
[complete_space E]
(L : E →L[ℝ] F)
(φ : α →₁[μ] E) :
theorem
fst_integral
{α : 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 × F}
(hf : measure_theory.integrable f μ) :
theorem
snd_integral
{α : 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 × F}
(hf : measure_theory.integrable f μ) :
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 μ) :