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 #
We provide the following notations for expressing the integral of a function on a set :
∫ a in s, f a ∂μismeasure_theory.integral (μ.restrict s) f∫ a in s, f ais∫ a in s, f a ∂volume
Note that the set notations are defined in the file measure_theory/bochner_integration,
but we reference them here because all theorems about set integrals are in this file.
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 : measurable_set s) :
theorem
piecewise_ae_eq_restrict_compl
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
{μ : measure_theory.measure α}
{s : set α}
{f g : α → β}
(hs : measurable_set s) :
theorem
indicator_ae_eq_restrict
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
[has_zero β]
{μ : measure_theory.measure α}
{s : set α}
{f : α → β}
(hs : measurable_set s) :
theorem
indicator_ae_eq_restrict_compl
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
[has_zero β]
{μ : measure_theory.measure α}
{s : set α}
{f : α → β}
(hs : measurable_set 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
- measurable_at_filter f l μ = ∃ (s : set α) (H : s ∈ l), ae_measurable f (measure_theory.measure.restrict μ s)
@[simp]
theorem
measurable_at_bot
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
[measurable_space β]
{μ : measure_theory.measure α}
{f : α → β} :
@[protected]
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)
@[protected]
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) :
measurable_at_filter f l' μ
@[protected]
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 μ) :
measurable_at_filter f l μ
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) :
measurable_at_filter f l μ
@[protected]
theorem
measurable.measurable_at_filter
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
[measurable_space β]
{l : filter α}
{f : α → β}
{μ : measure_theory.measure α}
(h : measurable f) :
measurable_at_filter f l μ
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 α} :
@[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 α}
{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 α}
{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.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 : measurable_set s) :
ae_measurable f (μ.restrict s) ↔ ae_measurable (s.indicator f) μ
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 α}
(hs : measurable_set 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 : measurable_set s) :
measure_theory.integrable (s.indicator f) μ
theorem
measure_theory.integrable.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 f μ)
(hs : measurable_set 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 μ
@[protected]
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.integrable_at_filter.of_inf_ae
{α : 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 μ
Alias of integrable_at_filter.inf_ae_iff.
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 α}
{l : filter α}
[l.is_measurably_generated]
(hfm : measurable_at_filter f l μ)
(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 α}
{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)) :
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
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 α}
{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)) :
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_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 : disjoint (function.support f) (function.support g))
(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 α⦄, measurable_set s → ⇑μ s < ⊤ → P (s.indicator (λ (_x : α), c)))
(h_add : ∀ ⦃f g : α → E⦄, disjoint (function.support f) (function.support g) → measure_theory.integrable f μ → measure_theory.integrable g μ → P f → P g → P (f + g))
(h_closed : is_closed {f : ↥(measure_theory.Lp E 1 μ) | P ⇑f})
(h_ae : ∀ ⦃f g : α → E⦄, f =ᵐ[μ] g → measure_theory.integrable f μ → P f → P 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
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_add 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 : measurable_set s)
(h : ∀ᵐ (x : α) ∂μ, x ∈ s → f x = 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 : measurable_set s)
(h : set.eq_on f g s) :
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 : measurable_set s)
(ht : measurable_set 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 : measurable_set 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]
(hs : measurable_set s) :
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).
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 : measurable_set 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 : measurable_set s)
(hf : ae_measurable f (⇑(measure_theory.measure.map g) μ))
(hg : measurable g) :
theorem
measure_theory.set_integral_map_of_closed_embedding
{α : 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]
[topological_space α]
[borel_space α]
{β : Type u_2}
[measurable_space β]
[topological_space β]
[borel_space β]
{g : α → β}
{f : β → E}
{s : set β}
(hs : measurable_set s)
(hg : closed_embedding 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 : ae_measurable f (μ.restrict s)) :
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 : measurable_set 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 : ae_measurable f (μ.restrict s)) :
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 : measurable_set s)
(hC : ∀ (x : α), x ∈ s → ∥f x∥ ≤ C) :
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 μ) :
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 μ) :
theorem
measure_theory.set_integral_mono_ae_restrict
{α : Type u_1}
[measurable_space α]
{μ : measure_theory.measure α}
{f g : α → ℝ}
{s : set α}
(hf : measure_theory.integrable_on f s μ)
(hg : measure_theory.integrable_on g s μ)
(h : f ≤ᵐ[μ.restrict s] g) :
theorem
measure_theory.set_integral_mono_ae
{α : Type u_1}
[measurable_space α]
{μ : measure_theory.measure α}
{f g : α → ℝ}
{s : set α}
(hf : measure_theory.integrable_on f s μ)
(hg : measure_theory.integrable_on g s μ)
(h : f ≤ᵐ[μ] g) :
theorem
measure_theory.set_integral_mono_on
{α : Type u_1}
[measurable_space α]
{μ : measure_theory.measure α}
{f g : α → ℝ}
{s : set α}
(hf : measure_theory.integrable_on f s μ)
(hg : measure_theory.integrable_on g s μ)
(hs : measurable_set s)
(h : ∀ (x : α), x ∈ s → f x ≤ g x) :
theorem
measure_theory.set_integral_mono
{α : Type u_1}
[measurable_space α]
{μ : measure_theory.measure α}
{f g : α → ℝ}
{s : set α}
(hf : measure_theory.integrable_on f s μ)
(hg : measure_theory.integrable_on g s μ)
(h : f ≤ g) :
theorem
measure_theory.set_integral_nonneg_of_ae_restrict
{α : Type u_1}
[measurable_space α]
{μ : measure_theory.measure α}
{f : α → ℝ}
{s : set α}
(hf : 0 ≤ᵐ[μ.restrict s] f) :
theorem
measure_theory.set_integral_nonneg_of_ae
{α : Type u_1}
[measurable_space α]
{μ : measure_theory.measure α}
{f : α → ℝ}
{s : set α}
(hf : 0 ≤ᵐ[μ] f) :
theorem
measure_theory.set_integral_nonneg
{α : Type u_1}
[measurable_space α]
{μ : measure_theory.measure α}
{f : α → ℝ}
{s : set α}
(hs : measurable_set s)
(hf : ∀ (a : α), a ∈ s → 0 ≤ f a) :
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") :
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 ℝ≥0∞ 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 : measurable_set 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") :
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 ℝ≥0∞
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") :
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 anℝ≥0∞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
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 ∈ 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.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 : measurable_set s) :
ae_measurable f (μ.restrict s)
A function which is continuous on a set s is almost everywhere measurable with respect to
μ.restrict s.
theorem
continuous_on.measurable_at_filter
{α : 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 α}
(hs : is_open s)
(hf : continuous_on f s)
(x : α)
(H : x ∈ s) :
measurable_at_filter f (𝓝 x) μ
If a function is continuous on an open set s, then it is measurable at the filter 𝓝 x for
all x ∈ s.
theorem
continuous_at.measurable_at_filter
{α : 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 α}
(hs : is_open s)
(hf : ∀ (x : α), x ∈ s → continuous_at f x)
(x : α)
(H : x ∈ s) :
measurable_at_filter f (𝓝 x) μ
theorem
continuous_on.integrable_at_nhds_within
{α : Type u_1}
{E : Type u_3}
[measurable_space α]
[measurable_space E]
[normed_group E]
[topological_space α]
[opens_measurable_space α]
[borel_space E]
{μ : measure_theory.measure α}
[measure_theory.locally_finite_measure μ]
{a : α}
{t : set α}
{f : α → E}
(hft : continuous_on f t)
(ht : measurable_set t)
(ha : a ∈ t) :
measure_theory.integrable_at_filter f (𝓝[t] a) μ
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 : measurable_set 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") :
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 ℝ≥0∞ 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_on.integrable_on_compact
{α : Type u_1}
{E : Type u_3}
[measurable_space α]
[measurable_space E]
[normed_group E]
[topological_space α]
[opens_measurable_space α]
[borel_space E]
[t2_space α]
{μ : measure_theory.measure α}
[measure_theory.locally_finite_measure μ]
{s : set α}
(hs : is_compact s)
{f : α → E}
(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.integrable_of_compact_closure_support
{α : 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 μ]
{f : α → E}
(hf : continuous f)
(hfc : is_compact (closure (function.support f))) :
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.
This holds for simple functions. The general result follows from the continuity of all involved
operations on the space L¹. Note that composition by a continuous linear map on L¹ is not just
the composition, as we are dealing with classes of functions, but it has already been defined
as continuous_linear_map.comp_Lp. We take advantage of this construction here.
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)) μ
theorem
continuous_linear_map.integral_comp_Lp
{α : 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]
{p : ℝ≥0∞}
[measurable_space F]
[borel_space F]
[topological_space.second_countable_topology F]
[complete_space F]
[borel_space E]
[topological_space.second_countable_topology E]
(L : E →L[ℝ] F)
(φ : ↥(measure_theory.Lp E p μ)) :
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]
[topological_space.second_countable_topology F]
[complete_space F]
[borel_space E]
[topological_space.second_countable_topology E]
(L : E →L[ℝ] F) :
continuous (λ (φ : ↥(measure_theory.Lp E 1 μ)), ∫ (a : α), ⇑L (⇑φ a) ∂μ)
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]
[topological_space.second_countable_topology F]
[complete_space F]
[borel_space E]
[topological_space.second_countable_topology E]
[complete_space E]
(L : E →L[ℝ] F)
{φ : α → E}
(φ_int : measure_theory.integrable φ μ) :
theorem
continuous_linear_map.integral_apply
{α : 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]
{H : Type u_2}
[normed_group H]
[normed_space ℝ H]
[topological_space.second_countable_topology (H →L[ℝ] E)]
{φ : α → (H →L[ℝ] E)}
(φ_int : measure_theory.integrable φ μ)
(v : H) :
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]
[topological_space.second_countable_topology F]
[complete_space F]
[borel_space E]
[topological_space.second_countable_topology E]
[complete_space E]
(L : E →L[ℝ] F)
{K : ℝ≥0}
(hL : antilipschitz_with K ⇑L)
(φ : α → E) :
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]
[topological_space.second_countable_topology F]
[complete_space F]
[borel_space E]
[topological_space.second_countable_topology E]
[complete_space E]
(L : E →L[ℝ] F)
(φ : ↥(measure_theory.Lp E 1 μ)) :
theorem
linear_isometry.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]
[complete_space E]
[topological_space.second_countable_topology F]
[complete_space F]
[borel_space E]
[topological_space.second_countable_topology E]
(L : E →ₗᵢ[ℝ] F)
(φ : α → E) :
@[norm_cast]
theorem
integral_of_real
{α : Type u_1}
[measurable_space α]
{μ : measure_theory.measure α}
{𝕜 : Type u_2}
[is_R_or_C 𝕜]
[measurable_space 𝕜]
[borel_space 𝕜]
{f : α → ℝ} :
theorem
integral_conj
{α : Type u_1}
[measurable_space α]
{μ : measure_theory.measure α}
{𝕜 : Type u_2}
[is_R_or_C 𝕜]
[measurable_space 𝕜]
[borel_space 𝕜]
{f : α → 𝕜} :
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 μ) :
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) :