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.
setIntegral_union, setIntegral_empty, setIntegral_univ.
We use the property IntegrableOn f s μ := Integrable f (μ.restrict s), defined in
MeasureTheory.IntegrableOn. We also defined in that same file a predicate
IntegrableAtFilter (f : X → E) (l : Filter X) (μ : Measure X) saying that f is integrable at
some set s ∈ l.
Finally, we prove a version of the
Fundamental theorem of calculus
for set integral, see Filter.Tendsto.integral_sub_linear_isLittleO_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.smallSets, 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 :
∫ x in s, f x ∂μisMeasureTheory.integral (μ.restrict s) f∫ x in s, f xis∫ x in s, f x ∂volume
Note that the set notations are defined in the file Mathlib/MeasureTheory/Integral/Bochner.lean,
but we reference them here because all theorems about set integrals are in this file.
theorem
MeasureTheory.setIntegral_congr_ae₀
{X : Type u_1}
{E : Type u_3}
[MeasurableSpace X]
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{f : X → E}
{g : X → E}
{s : Set X}
{μ : MeasureTheory.Measure X}
(hs : MeasureTheory.NullMeasurableSet s μ)
(h : ∀ᵐ (x : X) ∂μ, x ∈ s → f x = g x)
:
∫ (x : X) in s, f x ∂μ = ∫ (x : X) in s, g x ∂μ
@[deprecated MeasureTheory.setIntegral_congr_ae₀]
theorem
MeasureTheory.set_integral_congr_ae₀
{X : Type u_1}
{E : Type u_3}
[MeasurableSpace X]
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{f : X → E}
{g : X → E}
{s : Set X}
{μ : MeasureTheory.Measure X}
(hs : MeasureTheory.NullMeasurableSet s μ)
(h : ∀ᵐ (x : X) ∂μ, x ∈ s → f x = g x)
:
∫ (x : X) in s, f x ∂μ = ∫ (x : X) in s, g x ∂μ
Alias of MeasureTheory.setIntegral_congr_ae₀.
theorem
MeasureTheory.setIntegral_congr_ae
{X : Type u_1}
{E : Type u_3}
[MeasurableSpace X]
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{f : X → E}
{g : X → E}
{s : Set X}
{μ : MeasureTheory.Measure X}
(hs : MeasurableSet s)
(h : ∀ᵐ (x : X) ∂μ, x ∈ s → f x = g x)
:
∫ (x : X) in s, f x ∂μ = ∫ (x : X) in s, g x ∂μ
@[deprecated MeasureTheory.setIntegral_congr_ae]
theorem
MeasureTheory.set_integral_congr_ae
{X : Type u_1}
{E : Type u_3}
[MeasurableSpace X]
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{f : X → E}
{g : X → E}
{s : Set X}
{μ : MeasureTheory.Measure X}
(hs : MeasurableSet s)
(h : ∀ᵐ (x : X) ∂μ, x ∈ s → f x = g x)
:
∫ (x : X) in s, f x ∂μ = ∫ (x : X) in s, g x ∂μ
Alias of MeasureTheory.setIntegral_congr_ae.
theorem
MeasureTheory.setIntegral_congr_fun₀
{X : Type u_1}
{E : Type u_3}
[MeasurableSpace X]
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{f : X → E}
{g : X → E}
{s : Set X}
{μ : MeasureTheory.Measure X}
(hs : MeasureTheory.NullMeasurableSet s μ)
(h : Set.EqOn f g s)
:
∫ (x : X) in s, f x ∂μ = ∫ (x : X) in s, g x ∂μ
@[deprecated MeasureTheory.setIntegral_congr_fun₀]
theorem
MeasureTheory.setIntegral_congr₀
{X : Type u_1}
{E : Type u_3}
[MeasurableSpace X]
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{f : X → E}
{g : X → E}
{s : Set X}
{μ : MeasureTheory.Measure X}
(hs : MeasureTheory.NullMeasurableSet s μ)
(h : Set.EqOn f g s)
:
∫ (x : X) in s, f x ∂μ = ∫ (x : X) in s, g x ∂μ
Alias of MeasureTheory.setIntegral_congr_fun₀.
@[deprecated MeasureTheory.setIntegral_congr_fun₀]
theorem
MeasureTheory.set_integral_congr₀
{X : Type u_1}
{E : Type u_3}
[MeasurableSpace X]
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{f : X → E}
{g : X → E}
{s : Set X}
{μ : MeasureTheory.Measure X}
(hs : MeasureTheory.NullMeasurableSet s μ)
(h : Set.EqOn f g s)
:
∫ (x : X) in s, f x ∂μ = ∫ (x : X) in s, g x ∂μ
Alias of MeasureTheory.setIntegral_congr_fun₀.
theorem
MeasureTheory.setIntegral_congr_fun
{X : Type u_1}
{E : Type u_3}
[MeasurableSpace X]
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{f : X → E}
{g : X → E}
{s : Set X}
{μ : MeasureTheory.Measure X}
(hs : MeasurableSet s)
(h : Set.EqOn f g s)
:
∫ (x : X) in s, f x ∂μ = ∫ (x : X) in s, g x ∂μ
@[deprecated MeasureTheory.setIntegral_congr_fun]
theorem
MeasureTheory.setIntegral_congr
{X : Type u_1}
{E : Type u_3}
[MeasurableSpace X]
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{f : X → E}
{g : X → E}
{s : Set X}
{μ : MeasureTheory.Measure X}
(hs : MeasurableSet s)
(h : Set.EqOn f g s)
:
∫ (x : X) in s, f x ∂μ = ∫ (x : X) in s, g x ∂μ
Alias of MeasureTheory.setIntegral_congr_fun.
@[deprecated MeasureTheory.setIntegral_congr_fun]
theorem
MeasureTheory.set_integral_congr
{X : Type u_1}
{E : Type u_3}
[MeasurableSpace X]
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{f : X → E}
{g : X → E}
{s : Set X}
{μ : MeasureTheory.Measure X}
(hs : MeasurableSet s)
(h : Set.EqOn f g s)
:
∫ (x : X) in s, f x ∂μ = ∫ (x : X) in s, g x ∂μ
Alias of MeasureTheory.setIntegral_congr_fun.
theorem
MeasureTheory.setIntegral_congr_set
{X : Type u_1}
{E : Type u_3}
[MeasurableSpace X]
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{f : X → E}
{s : Set X}
{t : Set X}
{μ : MeasureTheory.Measure X}
(hst : s =ᵐ[μ] t)
:
∫ (x : X) in s, f x ∂μ = ∫ (x : X) in t, f x ∂μ
@[deprecated MeasureTheory.setIntegral_congr_set]
theorem
MeasureTheory.setIntegral_congr_set_ae
{X : Type u_1}
{E : Type u_3}
[MeasurableSpace X]
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{f : X → E}
{s : Set X}
{t : Set X}
{μ : MeasureTheory.Measure X}
(hst : s =ᵐ[μ] t)
:
∫ (x : X) in s, f x ∂μ = ∫ (x : X) in t, f x ∂μ
Alias of MeasureTheory.setIntegral_congr_set.
@[deprecated MeasureTheory.setIntegral_congr_set]
theorem
MeasureTheory.set_integral_congr_set_ae
{X : Type u_1}
{E : Type u_3}
[MeasurableSpace X]
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{f : X → E}
{s : Set X}
{t : Set X}
{μ : MeasureTheory.Measure X}
(hst : s =ᵐ[μ] t)
:
∫ (x : X) in s, f x ∂μ = ∫ (x : X) in t, f x ∂μ
Alias of MeasureTheory.setIntegral_congr_set.
theorem
MeasureTheory.integral_union_ae
{X : Type u_1}
{E : Type u_3}
[MeasurableSpace X]
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{f : X → E}
{s : Set X}
{t : Set X}
{μ : MeasureTheory.Measure X}
(hst : MeasureTheory.AEDisjoint μ s t)
(ht : MeasureTheory.NullMeasurableSet t μ)
(hfs : MeasureTheory.IntegrableOn f s μ)
(hft : MeasureTheory.IntegrableOn f t μ)
:
theorem
MeasureTheory.setIntegral_union
{X : Type u_1}
{E : Type u_3}
[MeasurableSpace X]
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{f : X → E}
{s : Set X}
{t : Set X}
{μ : MeasureTheory.Measure X}
(hst : Disjoint s t)
(ht : MeasurableSet t)
(hfs : MeasureTheory.IntegrableOn f s μ)
(hft : MeasureTheory.IntegrableOn f t μ)
:
@[deprecated MeasureTheory.setIntegral_union]
theorem
MeasureTheory.integral_union
{X : Type u_1}
{E : Type u_3}
[MeasurableSpace X]
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{f : X → E}
{s : Set X}
{t : Set X}
{μ : MeasureTheory.Measure X}
(hst : Disjoint s t)
(ht : MeasurableSet t)
(hfs : MeasureTheory.IntegrableOn f s μ)
(hft : MeasureTheory.IntegrableOn f t μ)
:
Alias of MeasureTheory.setIntegral_union.
theorem
MeasureTheory.integral_diff
{X : Type u_1}
{E : Type u_3}
[MeasurableSpace X]
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{f : X → E}
{s : Set X}
{t : Set X}
{μ : MeasureTheory.Measure X}
(ht : MeasurableSet t)
(hfs : MeasureTheory.IntegrableOn f s μ)
(hts : t ⊆ s)
:
theorem
MeasureTheory.integral_inter_add_diff₀
{X : Type u_1}
{E : Type u_3}
[MeasurableSpace X]
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{f : X → E}
{s : Set X}
{t : Set X}
{μ : MeasureTheory.Measure X}
(ht : MeasureTheory.NullMeasurableSet t μ)
(hfs : MeasureTheory.IntegrableOn f s μ)
:
theorem
MeasureTheory.integral_inter_add_diff
{X : Type u_1}
{E : Type u_3}
[MeasurableSpace X]
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{f : X → E}
{s : Set X}
{t : Set X}
{μ : MeasureTheory.Measure X}
(ht : MeasurableSet t)
(hfs : MeasureTheory.IntegrableOn f s μ)
:
theorem
MeasureTheory.integral_finset_biUnion
{X : Type u_1}
{E : Type u_3}
[MeasurableSpace X]
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{f : X → E}
{μ : MeasureTheory.Measure X}
{ι : Type u_5}
(t : Finset ι)
{s : ι → Set X}
(hs : ∀ i ∈ t, MeasurableSet (s i))
(h's : (↑t).Pairwise (Disjoint on s))
(hf : ∀ i ∈ t, MeasureTheory.IntegrableOn f (s i) μ)
:
∫ (x : X) in ⋃ i ∈ t, s i, f x ∂μ = ∑ i ∈ t, ∫ (x : X) in s i, f x ∂μ
theorem
MeasureTheory.integral_fintype_iUnion
{X : Type u_1}
{E : Type u_3}
[MeasurableSpace X]
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{f : X → E}
{μ : MeasureTheory.Measure X}
{ι : Type u_5}
[Fintype ι]
{s : ι → Set X}
(hs : ∀ (i : ι), MeasurableSet (s i))
(h's : Pairwise (Disjoint on s))
(hf : ∀ (i : ι), MeasureTheory.IntegrableOn f (s i) μ)
:
∫ (x : X) in ⋃ (i : ι), s i, f x ∂μ = ∑ i : ι, ∫ (x : X) in s i, f x ∂μ
theorem
MeasureTheory.setIntegral_empty
{X : Type u_1}
{E : Type u_3}
[MeasurableSpace X]
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{f : X → E}
{μ : MeasureTheory.Measure X}
:
@[deprecated MeasureTheory.setIntegral_empty]
theorem
MeasureTheory.integral_empty
{X : Type u_1}
{E : Type u_3}
[MeasurableSpace X]
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{f : X → E}
{μ : MeasureTheory.Measure X}
:
Alias of MeasureTheory.setIntegral_empty.
theorem
MeasureTheory.setIntegral_univ
{X : Type u_1}
{E : Type u_3}
[MeasurableSpace X]
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{f : X → E}
{μ : MeasureTheory.Measure X}
:
∫ (x : X) in Set.univ, f x ∂μ = ∫ (x : X), f x ∂μ
@[deprecated MeasureTheory.setIntegral_univ]
theorem
MeasureTheory.integral_univ
{X : Type u_1}
{E : Type u_3}
[MeasurableSpace X]
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{f : X → E}
{μ : MeasureTheory.Measure X}
:
∫ (x : X) in Set.univ, f x ∂μ = ∫ (x : X), f x ∂μ
Alias of MeasureTheory.setIntegral_univ.
theorem
MeasureTheory.integral_add_compl₀
{X : Type u_1}
{E : Type u_3}
[MeasurableSpace X]
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{f : X → E}
{s : Set X}
{μ : MeasureTheory.Measure X}
(hs : MeasureTheory.NullMeasurableSet s μ)
(hfi : MeasureTheory.Integrable f μ)
:
theorem
MeasureTheory.integral_add_compl
{X : Type u_1}
{E : Type u_3}
[MeasurableSpace X]
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{f : X → E}
{s : Set X}
{μ : MeasureTheory.Measure X}
(hs : MeasurableSet s)
(hfi : MeasureTheory.Integrable f μ)
:
theorem
MeasureTheory.setIntegral_compl
{X : Type u_1}
{E : Type u_3}
[MeasurableSpace X]
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{f : X → E}
{s : Set X}
{μ : MeasureTheory.Measure X}
(hs : MeasurableSet s)
(hfi : MeasureTheory.Integrable f μ)
:
theorem
MeasureTheory.integral_indicator
{X : Type u_1}
{E : Type u_3}
[MeasurableSpace X]
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{f : X → E}
{s : Set X}
{μ : MeasureTheory.Measure X}
(hs : MeasurableSet s)
:
∫ (x : X), s.indicator f x ∂μ = ∫ (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).
theorem
MeasureTheory.setIntegral_indicator
{X : Type u_1}
{E : Type u_3}
[MeasurableSpace X]
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{f : X → E}
{s : Set X}
{t : Set X}
{μ : MeasureTheory.Measure X}
(ht : MeasurableSet t)
:
@[deprecated MeasureTheory.setIntegral_indicator]
theorem
MeasureTheory.set_integral_indicator
{X : Type u_1}
{E : Type u_3}
[MeasurableSpace X]
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{f : X → E}
{s : Set X}
{t : Set X}
{μ : MeasureTheory.Measure X}
(ht : MeasurableSet t)
:
Alias of MeasureTheory.setIntegral_indicator.
theorem
MeasureTheory.ofReal_setIntegral_one_of_measure_ne_top
{X : Type u_5}
{m : MeasurableSpace X}
{μ : MeasureTheory.Measure X}
{s : Set X}
(hs : μ s ≠ ⊤)
:
ENNReal.ofReal (∫ (x : X) in s, 1 ∂μ) = μ s
@[deprecated MeasureTheory.ofReal_setIntegral_one_of_measure_ne_top]
theorem
MeasureTheory.ofReal_set_integral_one_of_measure_ne_top
{X : Type u_5}
{m : MeasurableSpace X}
{μ : MeasureTheory.Measure X}
{s : Set X}
(hs : μ s ≠ ⊤)
:
ENNReal.ofReal (∫ (x : X) in s, 1 ∂μ) = μ s
Alias of MeasureTheory.ofReal_setIntegral_one_of_measure_ne_top.
theorem
MeasureTheory.ofReal_setIntegral_one
{X : Type u_5}
:
∀ {x : MeasurableSpace X} (μ : MeasureTheory.Measure X) [inst : MeasureTheory.IsFiniteMeasure μ] (s : Set X),
ENNReal.ofReal (∫ (x : X) in s, 1 ∂μ) = μ s
@[deprecated MeasureTheory.ofReal_setIntegral_one]
theorem
MeasureTheory.ofReal_set_integral_one
{X : Type u_5}
:
∀ {x : MeasurableSpace X} (μ : MeasureTheory.Measure X) [inst : MeasureTheory.IsFiniteMeasure μ] (s : Set X),
ENNReal.ofReal (∫ (x : X) in s, 1 ∂μ) = μ s
Alias of MeasureTheory.ofReal_setIntegral_one.
theorem
MeasureTheory.integral_piecewise
{X : Type u_1}
{E : Type u_3}
[MeasurableSpace X]
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{f : X → E}
{g : X → E}
{s : Set X}
{μ : MeasureTheory.Measure X}
[DecidablePred fun (x : X) => x ∈ s]
(hs : MeasurableSet s)
(hf : MeasureTheory.IntegrableOn f s μ)
(hg : MeasureTheory.IntegrableOn g sᶜ μ)
:
theorem
MeasureTheory.tendsto_setIntegral_of_monotone
{X : Type u_1}
{E : Type u_3}
[MeasurableSpace X]
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{f : X → E}
{μ : MeasureTheory.Measure X}
{ι : Type u_5}
[Countable ι]
[SemilatticeSup ι]
{s : ι → Set X}
(hsm : ∀ (i : ι), MeasurableSet (s i))
(h_mono : Monotone s)
(hfi : MeasureTheory.IntegrableOn f (⋃ (n : ι), s n) μ)
:
Filter.Tendsto (fun (i : ι) => ∫ (x : X) in s i, f x ∂μ) Filter.atTop (nhds (∫ (x : X) in ⋃ (n : ι), s n, f x ∂μ))
@[deprecated MeasureTheory.tendsto_setIntegral_of_monotone]
theorem
MeasureTheory.tendsto_set_integral_of_monotone
{X : Type u_1}
{E : Type u_3}
[MeasurableSpace X]
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{f : X → E}
{μ : MeasureTheory.Measure X}
{ι : Type u_5}
[Countable ι]
[SemilatticeSup ι]
{s : ι → Set X}
(hsm : ∀ (i : ι), MeasurableSet (s i))
(h_mono : Monotone s)
(hfi : MeasureTheory.IntegrableOn f (⋃ (n : ι), s n) μ)
:
Filter.Tendsto (fun (i : ι) => ∫ (x : X) in s i, f x ∂μ) Filter.atTop (nhds (∫ (x : X) in ⋃ (n : ι), s n, f x ∂μ))
theorem
MeasureTheory.tendsto_setIntegral_of_antitone
{X : Type u_1}
{E : Type u_3}
[MeasurableSpace X]
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{f : X → E}
{μ : MeasureTheory.Measure X}
{ι : Type u_5}
[Countable ι]
[SemilatticeSup ι]
{s : ι → Set X}
(hsm : ∀ (i : ι), MeasurableSet (s i))
(h_anti : Antitone s)
(hfi : ∃ (i : ι), MeasureTheory.IntegrableOn f (s i) μ)
:
Filter.Tendsto (fun (i : ι) => ∫ (x : X) in s i, f x ∂μ) Filter.atTop (nhds (∫ (x : X) in ⋂ (n : ι), s n, f x ∂μ))
@[deprecated MeasureTheory.tendsto_setIntegral_of_antitone]
theorem
MeasureTheory.tendsto_set_integral_of_antitone
{X : Type u_1}
{E : Type u_3}
[MeasurableSpace X]
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{f : X → E}
{μ : MeasureTheory.Measure X}
{ι : Type u_5}
[Countable ι]
[SemilatticeSup ι]
{s : ι → Set X}
(hsm : ∀ (i : ι), MeasurableSet (s i))
(h_anti : Antitone s)
(hfi : ∃ (i : ι), MeasureTheory.IntegrableOn f (s i) μ)
:
Filter.Tendsto (fun (i : ι) => ∫ (x : X) in s i, f x ∂μ) Filter.atTop (nhds (∫ (x : X) in ⋂ (n : ι), s n, f x ∂μ))
theorem
MeasureTheory.hasSum_integral_iUnion_ae
{X : Type u_1}
{E : Type u_3}
[MeasurableSpace X]
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{f : X → E}
{μ : MeasureTheory.Measure X}
{ι : Type u_5}
[Countable ι]
{s : ι → Set X}
(hm : ∀ (i : ι), MeasureTheory.NullMeasurableSet (s i) μ)
(hd : Pairwise (MeasureTheory.AEDisjoint μ on s))
(hfi : MeasureTheory.IntegrableOn f (⋃ (i : ι), s i) μ)
:
HasSum (fun (n : ι) => ∫ (x : X) in s n, f x ∂μ) (∫ (x : X) in ⋃ (n : ι), s n, f x ∂μ)
theorem
MeasureTheory.hasSum_integral_iUnion
{X : Type u_1}
{E : Type u_3}
[MeasurableSpace X]
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{f : X → E}
{μ : MeasureTheory.Measure X}
{ι : Type u_5}
[Countable ι]
{s : ι → Set X}
(hm : ∀ (i : ι), MeasurableSet (s i))
(hd : Pairwise (Disjoint on s))
(hfi : MeasureTheory.IntegrableOn f (⋃ (i : ι), s i) μ)
:
HasSum (fun (n : ι) => ∫ (x : X) in s n, f x ∂μ) (∫ (x : X) in ⋃ (n : ι), s n, f x ∂μ)
theorem
MeasureTheory.integral_iUnion
{X : Type u_1}
{E : Type u_3}
[MeasurableSpace X]
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{f : X → E}
{μ : MeasureTheory.Measure X}
{ι : Type u_5}
[Countable ι]
{s : ι → Set X}
(hm : ∀ (i : ι), MeasurableSet (s i))
(hd : Pairwise (Disjoint on s))
(hfi : MeasureTheory.IntegrableOn f (⋃ (i : ι), s i) μ)
:
∫ (x : X) in ⋃ (n : ι), s n, f x ∂μ = ∑' (n : ι), ∫ (x : X) in s n, f x ∂μ
theorem
MeasureTheory.integral_iUnion_ae
{X : Type u_1}
{E : Type u_3}
[MeasurableSpace X]
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{f : X → E}
{μ : MeasureTheory.Measure X}
{ι : Type u_5}
[Countable ι]
{s : ι → Set X}
(hm : ∀ (i : ι), MeasureTheory.NullMeasurableSet (s i) μ)
(hd : Pairwise (MeasureTheory.AEDisjoint μ on s))
(hfi : MeasureTheory.IntegrableOn f (⋃ (i : ι), s i) μ)
:
∫ (x : X) in ⋃ (n : ι), s n, f x ∂μ = ∑' (n : ι), ∫ (x : X) in s n, f x ∂μ
theorem
MeasureTheory.setIntegral_eq_zero_of_ae_eq_zero
{X : Type u_1}
{E : Type u_3}
[MeasurableSpace X]
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{f : X → E}
{t : Set X}
{μ : MeasureTheory.Measure X}
(ht_eq : ∀ᵐ (x : X) ∂μ, x ∈ t → f x = 0)
:
∫ (x : X) in t, f x ∂μ = 0
@[deprecated MeasureTheory.setIntegral_eq_zero_of_ae_eq_zero]
theorem
MeasureTheory.set_integral_eq_zero_of_ae_eq_zero
{X : Type u_1}
{E : Type u_3}
[MeasurableSpace X]
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{f : X → E}
{t : Set X}
{μ : MeasureTheory.Measure X}
(ht_eq : ∀ᵐ (x : X) ∂μ, x ∈ t → f x = 0)
:
∫ (x : X) in t, f x ∂μ = 0
theorem
MeasureTheory.setIntegral_eq_zero_of_forall_eq_zero
{X : Type u_1}
{E : Type u_3}
[MeasurableSpace X]
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{f : X → E}
{t : Set X}
{μ : MeasureTheory.Measure X}
(ht_eq : ∀ x ∈ t, f x = 0)
:
∫ (x : X) in t, f x ∂μ = 0
@[deprecated MeasureTheory.setIntegral_eq_zero_of_forall_eq_zero]
theorem
MeasureTheory.set_integral_eq_zero_of_forall_eq_zero
{X : Type u_1}
{E : Type u_3}
[MeasurableSpace X]
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{f : X → E}
{t : Set X}
{μ : MeasureTheory.Measure X}
(ht_eq : ∀ x ∈ t, f x = 0)
:
∫ (x : X) in t, f x ∂μ = 0
Alias of MeasureTheory.setIntegral_eq_zero_of_forall_eq_zero.
theorem
MeasureTheory.integral_union_eq_left_of_ae_aux
{X : Type u_1}
{E : Type u_3}
[MeasurableSpace X]
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{f : X → E}
{s : Set X}
{t : Set X}
{μ : MeasureTheory.Measure X}
(ht_eq : ∀ᵐ (x : X) ∂μ.restrict t, f x = 0)
(haux : MeasureTheory.StronglyMeasurable f)
(H : MeasureTheory.IntegrableOn f (s ∪ t) μ)
:
theorem
MeasureTheory.integral_union_eq_left_of_ae
{X : Type u_1}
{E : Type u_3}
[MeasurableSpace X]
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{f : X → E}
{s : Set X}
{t : Set X}
{μ : MeasureTheory.Measure X}
(ht_eq : ∀ᵐ (x : X) ∂μ.restrict t, f x = 0)
:
theorem
MeasureTheory.integral_union_eq_left_of_forall₀
{X : Type u_1}
{E : Type u_3}
[MeasurableSpace X]
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{s : Set X}
{t : Set X}
{μ : MeasureTheory.Measure X}
{f : X → E}
(ht : MeasureTheory.NullMeasurableSet t μ)
(ht_eq : ∀ x ∈ t, f x = 0)
:
theorem
MeasureTheory.integral_union_eq_left_of_forall
{X : Type u_1}
{E : Type u_3}
[MeasurableSpace X]
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{s : Set X}
{t : Set X}
{μ : MeasureTheory.Measure X}
{f : X → E}
(ht : MeasurableSet t)
(ht_eq : ∀ x ∈ t, f x = 0)
:
theorem
MeasureTheory.setIntegral_eq_of_subset_of_ae_diff_eq_zero_aux
{X : Type u_1}
{E : Type u_3}
[MeasurableSpace X]
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{f : X → E}
{s : Set X}
{t : Set X}
{μ : MeasureTheory.Measure X}
(hts : s ⊆ t)
(h't : ∀ᵐ (x : X) ∂μ, x ∈ t \ s → f x = 0)
(haux : MeasureTheory.StronglyMeasurable f)
(h'aux : MeasureTheory.IntegrableOn f t μ)
:
∫ (x : X) in t, f x ∂μ = ∫ (x : X) in s, f x ∂μ
@[deprecated MeasureTheory.setIntegral_eq_of_subset_of_ae_diff_eq_zero_aux]
theorem
MeasureTheory.set_integral_eq_of_subset_of_ae_diff_eq_zero_aux
{X : Type u_1}
{E : Type u_3}
[MeasurableSpace X]
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{f : X → E}
{s : Set X}
{t : Set X}
{μ : MeasureTheory.Measure X}
(hts : s ⊆ t)
(h't : ∀ᵐ (x : X) ∂μ, x ∈ t \ s → f x = 0)
(haux : MeasureTheory.StronglyMeasurable f)
(h'aux : MeasureTheory.IntegrableOn f t μ)
:
∫ (x : X) in t, f x ∂μ = ∫ (x : X) in s, f x ∂μ
Alias of MeasureTheory.setIntegral_eq_of_subset_of_ae_diff_eq_zero_aux.
theorem
MeasureTheory.setIntegral_eq_of_subset_of_ae_diff_eq_zero
{X : Type u_1}
{E : Type u_3}
[MeasurableSpace X]
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{f : X → E}
{s : Set X}
{t : Set X}
{μ : MeasureTheory.Measure X}
(ht : MeasureTheory.NullMeasurableSet t μ)
(hts : s ⊆ t)
(h't : ∀ᵐ (x : X) ∂μ, x ∈ t \ s → f x = 0)
:
∫ (x : X) in t, f x ∂μ = ∫ (x : X) in s, f x ∂μ
If a function vanishes almost everywhere on t \ s with s ⊆ t, then its integrals on s
and t coincide if t is null-measurable.
@[deprecated MeasureTheory.setIntegral_eq_of_subset_of_ae_diff_eq_zero]
theorem
MeasureTheory.set_integral_eq_of_subset_of_ae_diff_eq_zero
{X : Type u_1}
{E : Type u_3}
[MeasurableSpace X]
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{f : X → E}
{s : Set X}
{t : Set X}
{μ : MeasureTheory.Measure X}
(ht : MeasureTheory.NullMeasurableSet t μ)
(hts : s ⊆ t)
(h't : ∀ᵐ (x : X) ∂μ, x ∈ t \ s → f x = 0)
:
∫ (x : X) in t, f x ∂μ = ∫ (x : X) in s, f x ∂μ
Alias of MeasureTheory.setIntegral_eq_of_subset_of_ae_diff_eq_zero.
If a function vanishes almost everywhere on t \ s with s ⊆ t, then its integrals on s
and t coincide if t is null-measurable.
theorem
MeasureTheory.setIntegral_eq_of_subset_of_forall_diff_eq_zero
{X : Type u_1}
{E : Type u_3}
[MeasurableSpace X]
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{f : X → E}
{s : Set X}
{t : Set X}
{μ : MeasureTheory.Measure X}
(ht : MeasurableSet t)
(hts : s ⊆ t)
(h't : ∀ x ∈ t \ s, f x = 0)
:
∫ (x : X) in t, f x ∂μ = ∫ (x : X) in s, f x ∂μ
If a function vanishes on t \ s with s ⊆ t, then its integrals on s
and t coincide if t is measurable.
@[deprecated MeasureTheory.setIntegral_eq_of_subset_of_forall_diff_eq_zero]
theorem
MeasureTheory.set_integral_eq_of_subset_of_forall_diff_eq_zero
{X : Type u_1}
{E : Type u_3}
[MeasurableSpace X]
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{f : X → E}
{s : Set X}
{t : Set X}
{μ : MeasureTheory.Measure X}
(ht : MeasurableSet t)
(hts : s ⊆ t)
(h't : ∀ x ∈ t \ s, f x = 0)
:
∫ (x : X) in t, f x ∂μ = ∫ (x : X) in s, f x ∂μ
Alias of MeasureTheory.setIntegral_eq_of_subset_of_forall_diff_eq_zero.
If a function vanishes on t \ s with s ⊆ t, then its integrals on s
and t coincide if t is measurable.
theorem
MeasureTheory.setIntegral_eq_integral_of_ae_compl_eq_zero
{X : Type u_1}
{E : Type u_3}
[MeasurableSpace X]
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{f : X → E}
{s : Set X}
{μ : MeasureTheory.Measure X}
(h : ∀ᵐ (x : X) ∂μ, x ∉ s → f x = 0)
:
∫ (x : X) in s, f x ∂μ = ∫ (x : X), f x ∂μ
If a function vanishes almost everywhere on sᶜ, then its integral on s
coincides with its integral on the whole space.
@[deprecated MeasureTheory.setIntegral_eq_integral_of_ae_compl_eq_zero]
theorem
MeasureTheory.set_integral_eq_integral_of_ae_compl_eq_zero
{X : Type u_1}
{E : Type u_3}
[MeasurableSpace X]
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{f : X → E}
{s : Set X}
{μ : MeasureTheory.Measure X}
(h : ∀ᵐ (x : X) ∂μ, x ∉ s → f x = 0)
:
∫ (x : X) in s, f x ∂μ = ∫ (x : X), f x ∂μ
Alias of MeasureTheory.setIntegral_eq_integral_of_ae_compl_eq_zero.
If a function vanishes almost everywhere on sᶜ, then its integral on s
coincides with its integral on the whole space.
theorem
MeasureTheory.setIntegral_eq_integral_of_forall_compl_eq_zero
{X : Type u_1}
{E : Type u_3}
[MeasurableSpace X]
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{f : X → E}
{s : Set X}
{μ : MeasureTheory.Measure X}
(h : ∀ x ∉ s, f x = 0)
:
∫ (x : X) in s, f x ∂μ = ∫ (x : X), f x ∂μ
If a function vanishes on sᶜ, then its integral on s coincides with its integral on the
whole space.
@[deprecated MeasureTheory.setIntegral_eq_integral_of_forall_compl_eq_zero]
theorem
MeasureTheory.set_integral_eq_integral_of_forall_compl_eq_zero
{X : Type u_1}
{E : Type u_3}
[MeasurableSpace X]
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{f : X → E}
{s : Set X}
{μ : MeasureTheory.Measure X}
(h : ∀ x ∉ s, f x = 0)
:
∫ (x : X) in s, f x ∂μ = ∫ (x : X), f x ∂μ
Alias of MeasureTheory.setIntegral_eq_integral_of_forall_compl_eq_zero.
If a function vanishes on sᶜ, then its integral on s coincides with its integral on the
whole space.
theorem
MeasureTheory.setIntegral_neg_eq_setIntegral_nonpos
{X : Type u_1}
{E : Type u_3}
[MeasurableSpace X]
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{μ : MeasureTheory.Measure X}
[LinearOrder E]
{f : X → E}
(hf : MeasureTheory.AEStronglyMeasurable f μ)
:
@[deprecated MeasureTheory.setIntegral_neg_eq_setIntegral_nonpos]
theorem
MeasureTheory.set_integral_neg_eq_set_integral_nonpos
{X : Type u_1}
{E : Type u_3}
[MeasurableSpace X]
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{μ : MeasureTheory.Measure X}
[LinearOrder E]
{f : X → E}
(hf : MeasureTheory.AEStronglyMeasurable f μ)
:
Alias of MeasureTheory.setIntegral_neg_eq_setIntegral_nonpos.
theorem
MeasureTheory.integral_norm_eq_pos_sub_neg
{X : Type u_1}
[MeasurableSpace X]
{μ : MeasureTheory.Measure X}
{f : X → ℝ}
(hfi : MeasureTheory.Integrable f μ)
:
theorem
MeasureTheory.setIntegral_const
{X : Type u_1}
{E : Type u_3}
[MeasurableSpace X]
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{s : Set X}
{μ : MeasureTheory.Measure X}
[CompleteSpace E]
(c : E)
:
@[deprecated MeasureTheory.setIntegral_const]
theorem
MeasureTheory.set_integral_const
{X : Type u_1}
{E : Type u_3}
[MeasurableSpace X]
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{s : Set X}
{μ : MeasureTheory.Measure X}
[CompleteSpace E]
(c : E)
:
Alias of MeasureTheory.setIntegral_const.
@[simp]
theorem
MeasureTheory.integral_indicator_const
{X : Type u_1}
{E : Type u_3}
[MeasurableSpace X]
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{μ : MeasureTheory.Measure X}
[CompleteSpace E]
(e : E)
⦃s : Set X⦄
(s_meas : MeasurableSet s)
:
@[simp]
theorem
MeasureTheory.integral_indicator_one
{X : Type u_1}
[MeasurableSpace X]
{μ : MeasureTheory.Measure X}
⦃s : Set X⦄
(hs : MeasurableSet s)
:
∫ (x : X), s.indicator 1 x ∂μ = (μ s).toReal
theorem
MeasureTheory.setIntegral_indicatorConstLp
{X : Type u_1}
{E : Type u_3}
[MeasurableSpace X]
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{s : Set X}
{t : Set X}
{μ : MeasureTheory.Measure X}
[CompleteSpace E]
{p : ENNReal}
(hs : MeasurableSet s)
(ht : MeasurableSet t)
(hμt : μ t ≠ ⊤)
(e : E)
:
∫ (x : X) in s, ↑↑(MeasureTheory.indicatorConstLp p ht hμt e) x ∂μ = (μ (t ∩ s)).toReal • e
@[deprecated MeasureTheory.setIntegral_indicatorConstLp]
theorem
MeasureTheory.set_integral_indicatorConstLp
{X : Type u_1}
{E : Type u_3}
[MeasurableSpace X]
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{s : Set X}
{t : Set X}
{μ : MeasureTheory.Measure X}
[CompleteSpace E]
{p : ENNReal}
(hs : MeasurableSet s)
(ht : MeasurableSet t)
(hμt : μ t ≠ ⊤)
(e : E)
:
∫ (x : X) in s, ↑↑(MeasureTheory.indicatorConstLp p ht hμt e) x ∂μ = (μ (t ∩ s)).toReal • e
theorem
MeasureTheory.integral_indicatorConstLp
{X : Type u_1}
{E : Type u_3}
[MeasurableSpace X]
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{t : Set X}
{μ : MeasureTheory.Measure X}
[CompleteSpace E]
{p : ENNReal}
(ht : MeasurableSet t)
(hμt : μ t ≠ ⊤)
(e : E)
:
∫ (x : X), ↑↑(MeasureTheory.indicatorConstLp p ht hμt e) x ∂μ = (μ t).toReal • e
theorem
MeasureTheory.setIntegral_map
{X : Type u_1}
{E : Type u_3}
[MeasurableSpace X]
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{μ : MeasureTheory.Measure X}
{Y : Type u_5}
[MeasurableSpace Y]
{g : X → Y}
{f : Y → E}
{s : Set Y}
(hs : MeasurableSet s)
(hf : MeasureTheory.AEStronglyMeasurable f (MeasureTheory.Measure.map g μ))
(hg : AEMeasurable g μ)
:
∫ (y : Y) in s, f y ∂MeasureTheory.Measure.map g μ = ∫ (x : X) in g ⁻¹' s, f (g x) ∂μ
@[deprecated MeasureTheory.setIntegral_map]
theorem
MeasureTheory.set_integral_map
{X : Type u_1}
{E : Type u_3}
[MeasurableSpace X]
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{μ : MeasureTheory.Measure X}
{Y : Type u_5}
[MeasurableSpace Y]
{g : X → Y}
{f : Y → E}
{s : Set Y}
(hs : MeasurableSet s)
(hf : MeasureTheory.AEStronglyMeasurable f (MeasureTheory.Measure.map g μ))
(hg : AEMeasurable g μ)
:
∫ (y : Y) in s, f y ∂MeasureTheory.Measure.map g μ = ∫ (x : X) in g ⁻¹' s, f (g x) ∂μ
Alias of MeasureTheory.setIntegral_map.
theorem
MeasurableEmbedding.setIntegral_map
{X : Type u_1}
{E : Type u_3}
[MeasurableSpace X]
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{μ : MeasureTheory.Measure X}
{Y : Type u_5}
:
∀ {x : MeasurableSpace Y} {f : X → Y},
MeasurableEmbedding f →
∀ (g : Y → E) (s : Set Y), ∫ (y : Y) in s, g y ∂MeasureTheory.Measure.map f μ = ∫ (x : X) in f ⁻¹' s, g (f x) ∂μ
@[deprecated MeasurableEmbedding.setIntegral_map]
theorem
MeasurableEmbedding.set_integral_map
{X : Type u_1}
{E : Type u_3}
[MeasurableSpace X]
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{μ : MeasureTheory.Measure X}
{Y : Type u_5}
:
∀ {x : MeasurableSpace Y} {f : X → Y},
MeasurableEmbedding f →
∀ (g : Y → E) (s : Set Y), ∫ (y : Y) in s, g y ∂MeasureTheory.Measure.map f μ = ∫ (x : X) in f ⁻¹' s, g (f x) ∂μ
Alias of MeasurableEmbedding.setIntegral_map.
theorem
IsClosedEmbedding.setIntegral_map
{X : Type u_1}
{E : Type u_3}
[MeasurableSpace X]
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{μ : MeasureTheory.Measure X}
[TopologicalSpace X]
[BorelSpace X]
{Y : Type u_5}
[MeasurableSpace Y]
[TopologicalSpace Y]
[BorelSpace Y]
{g : X → Y}
{f : Y → E}
(s : Set Y)
(hg : IsClosedEmbedding g)
:
∫ (y : Y) in s, f y ∂MeasureTheory.Measure.map g μ = ∫ (x : X) in g ⁻¹' s, f (g x) ∂μ
@[deprecated IsClosedEmbedding.setIntegral_map]
theorem
ClosedEmbedding.setIntegral_map
{X : Type u_1}
{E : Type u_3}
[MeasurableSpace X]
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{μ : MeasureTheory.Measure X}
[TopologicalSpace X]
[BorelSpace X]
{Y : Type u_5}
[MeasurableSpace Y]
[TopologicalSpace Y]
[BorelSpace Y]
{g : X → Y}
{f : Y → E}
(s : Set Y)
(hg : IsClosedEmbedding g)
:
∫ (y : Y) in s, f y ∂MeasureTheory.Measure.map g μ = ∫ (x : X) in g ⁻¹' s, f (g x) ∂μ
Alias of IsClosedEmbedding.setIntegral_map.
@[deprecated IsClosedEmbedding.setIntegral_map]
theorem
IsClosedEmbedding.set_integral_map
{X : Type u_1}
{E : Type u_3}
[MeasurableSpace X]
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{μ : MeasureTheory.Measure X}
[TopologicalSpace X]
[BorelSpace X]
{Y : Type u_5}
[MeasurableSpace Y]
[TopologicalSpace Y]
[BorelSpace Y]
{g : X → Y}
{f : Y → E}
(s : Set Y)
(hg : IsClosedEmbedding g)
:
∫ (y : Y) in s, f y ∂MeasureTheory.Measure.map g μ = ∫ (x : X) in g ⁻¹' s, f (g x) ∂μ
Alias of IsClosedEmbedding.setIntegral_map.
@[deprecated IsClosedEmbedding.set_integral_map]
theorem
ClosedEmbedding.set_integral_map
{X : Type u_1}
{E : Type u_3}
[MeasurableSpace X]
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{μ : MeasureTheory.Measure X}
[TopologicalSpace X]
[BorelSpace X]
{Y : Type u_5}
[MeasurableSpace Y]
[TopologicalSpace Y]
[BorelSpace Y]
{g : X → Y}
{f : Y → E}
(s : Set Y)
(hg : IsClosedEmbedding g)
:
∫ (y : Y) in s, f y ∂MeasureTheory.Measure.map g μ = ∫ (x : X) in g ⁻¹' s, f (g x) ∂μ
Alias of IsClosedEmbedding.setIntegral_map.
Alias of IsClosedEmbedding.setIntegral_map.
theorem
MeasureTheory.MeasurePreserving.setIntegral_preimage_emb
{X : Type u_1}
{E : Type u_3}
[MeasurableSpace X]
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{μ : MeasureTheory.Measure X}
{Y : Type u_5}
:
∀ {x : MeasurableSpace Y} {f : X → Y} {ν : MeasureTheory.Measure Y},
MeasureTheory.MeasurePreserving f μ ν →
MeasurableEmbedding f → ∀ (g : Y → E) (s : Set Y), ∫ (x : X) in f ⁻¹' s, g (f x) ∂μ = ∫ (y : Y) in s, g y ∂ν
@[deprecated MeasureTheory.MeasurePreserving.setIntegral_preimage_emb]
theorem
MeasureTheory.MeasurePreserving.set_integral_preimage_emb
{X : Type u_1}
{E : Type u_3}
[MeasurableSpace X]
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{μ : MeasureTheory.Measure X}
{Y : Type u_5}
:
∀ {x : MeasurableSpace Y} {f : X → Y} {ν : MeasureTheory.Measure Y},
MeasureTheory.MeasurePreserving f μ ν →
MeasurableEmbedding f → ∀ (g : Y → E) (s : Set Y), ∫ (x : X) in f ⁻¹' s, g (f x) ∂μ = ∫ (y : Y) in s, g y ∂ν
Alias of MeasureTheory.MeasurePreserving.setIntegral_preimage_emb.
theorem
MeasureTheory.MeasurePreserving.setIntegral_image_emb
{X : Type u_1}
{E : Type u_3}
[MeasurableSpace X]
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{μ : MeasureTheory.Measure X}
{Y : Type u_5}
:
∀ {x : MeasurableSpace Y} {f : X → Y} {ν : MeasureTheory.Measure Y},
MeasureTheory.MeasurePreserving f μ ν →
MeasurableEmbedding f → ∀ (g : Y → E) (s : Set X), ∫ (y : Y) in f '' s, g y ∂ν = ∫ (x : X) in s, g (f x) ∂μ
@[deprecated MeasureTheory.MeasurePreserving.setIntegral_image_emb]
theorem
MeasureTheory.MeasurePreserving.set_integral_image_emb
{X : Type u_1}
{E : Type u_3}
[MeasurableSpace X]
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{μ : MeasureTheory.Measure X}
{Y : Type u_5}
:
∀ {x : MeasurableSpace Y} {f : X → Y} {ν : MeasureTheory.Measure Y},
MeasureTheory.MeasurePreserving f μ ν →
MeasurableEmbedding f → ∀ (g : Y → E) (s : Set X), ∫ (y : Y) in f '' s, g y ∂ν = ∫ (x : X) in s, g (f x) ∂μ
Alias of MeasureTheory.MeasurePreserving.setIntegral_image_emb.
theorem
MeasureTheory.setIntegral_map_equiv
{X : Type u_1}
{E : Type u_3}
[MeasurableSpace X]
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{μ : MeasureTheory.Measure X}
{Y : Type u_5}
[MeasurableSpace Y]
(e : X ≃ᵐ Y)
(f : Y → E)
(s : Set Y)
:
∫ (y : Y) in s, f y ∂MeasureTheory.Measure.map (⇑e) μ = ∫ (x : X) in ⇑e ⁻¹' s, f (e x) ∂μ
@[deprecated MeasureTheory.setIntegral_map_equiv]
theorem
MeasureTheory.set_integral_map_equiv
{X : Type u_1}
{E : Type u_3}
[MeasurableSpace X]
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{μ : MeasureTheory.Measure X}
{Y : Type u_5}
[MeasurableSpace Y]
(e : X ≃ᵐ Y)
(f : Y → E)
(s : Set Y)
:
∫ (y : Y) in s, f y ∂MeasureTheory.Measure.map (⇑e) μ = ∫ (x : X) in ⇑e ⁻¹' s, f (e x) ∂μ
Alias of MeasureTheory.setIntegral_map_equiv.
theorem
MeasureTheory.norm_setIntegral_le_of_norm_le_const_ae
{X : Type u_1}
{E : Type u_3}
[MeasurableSpace X]
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{f : X → E}
{s : Set X}
{μ : MeasureTheory.Measure X}
{C : ℝ}
(hs : μ s < ⊤)
(hC : ∀ᵐ (x : X) ∂μ.restrict s, ‖f x‖ ≤ C)
:
@[deprecated MeasureTheory.norm_setIntegral_le_of_norm_le_const_ae]
theorem
MeasureTheory.norm_set_integral_le_of_norm_le_const_ae
{X : Type u_1}
{E : Type u_3}
[MeasurableSpace X]
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{f : X → E}
{s : Set X}
{μ : MeasureTheory.Measure X}
{C : ℝ}
(hs : μ s < ⊤)
(hC : ∀ᵐ (x : X) ∂μ.restrict s, ‖f x‖ ≤ C)
:
Alias of MeasureTheory.norm_setIntegral_le_of_norm_le_const_ae.
theorem
MeasureTheory.norm_setIntegral_le_of_norm_le_const_ae'
{X : Type u_1}
{E : Type u_3}
[MeasurableSpace X]
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{f : X → E}
{s : Set X}
{μ : MeasureTheory.Measure X}
{C : ℝ}
(hs : μ s < ⊤)
(hC : ∀ᵐ (x : X) ∂μ, x ∈ s → ‖f x‖ ≤ C)
(hfm : MeasureTheory.AEStronglyMeasurable f (μ.restrict s))
:
@[deprecated MeasureTheory.norm_setIntegral_le_of_norm_le_const_ae']
theorem
MeasureTheory.norm_set_integral_le_of_norm_le_const_ae'
{X : Type u_1}
{E : Type u_3}
[MeasurableSpace X]
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{f : X → E}
{s : Set X}
{μ : MeasureTheory.Measure X}
{C : ℝ}
(hs : μ s < ⊤)
(hC : ∀ᵐ (x : X) ∂μ, x ∈ s → ‖f x‖ ≤ C)
(hfm : MeasureTheory.AEStronglyMeasurable f (μ.restrict s))
:
Alias of MeasureTheory.norm_setIntegral_le_of_norm_le_const_ae'.
theorem
MeasureTheory.norm_setIntegral_le_of_norm_le_const_ae''
{X : Type u_1}
{E : Type u_3}
[MeasurableSpace X]
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{f : X → E}
{s : Set X}
{μ : MeasureTheory.Measure X}
{C : ℝ}
(hs : μ s < ⊤)
(hsm : MeasurableSet s)
(hC : ∀ᵐ (x : X) ∂μ, x ∈ s → ‖f x‖ ≤ C)
:
@[deprecated MeasureTheory.norm_setIntegral_le_of_norm_le_const_ae'']
theorem
MeasureTheory.norm_set_integral_le_of_norm_le_const_ae''
{X : Type u_1}
{E : Type u_3}
[MeasurableSpace X]
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{f : X → E}
{s : Set X}
{μ : MeasureTheory.Measure X}
{C : ℝ}
(hs : μ s < ⊤)
(hsm : MeasurableSet s)
(hC : ∀ᵐ (x : X) ∂μ, x ∈ s → ‖f x‖ ≤ C)
:
Alias of MeasureTheory.norm_setIntegral_le_of_norm_le_const_ae''.
theorem
MeasureTheory.norm_setIntegral_le_of_norm_le_const
{X : Type u_1}
{E : Type u_3}
[MeasurableSpace X]
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{f : X → E}
{s : Set X}
{μ : MeasureTheory.Measure X}
{C : ℝ}
(hs : μ s < ⊤)
(hC : ∀ x ∈ s, ‖f x‖ ≤ C)
(hfm : MeasureTheory.AEStronglyMeasurable f (μ.restrict s))
:
@[deprecated MeasureTheory.norm_setIntegral_le_of_norm_le_const]
theorem
MeasureTheory.norm_set_integral_le_of_norm_le_const
{X : Type u_1}
{E : Type u_3}
[MeasurableSpace X]
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{f : X → E}
{s : Set X}
{μ : MeasureTheory.Measure X}
{C : ℝ}
(hs : μ s < ⊤)
(hC : ∀ x ∈ s, ‖f x‖ ≤ C)
(hfm : MeasureTheory.AEStronglyMeasurable f (μ.restrict s))
:
Alias of MeasureTheory.norm_setIntegral_le_of_norm_le_const.
theorem
MeasureTheory.norm_setIntegral_le_of_norm_le_const'
{X : Type u_1}
{E : Type u_3}
[MeasurableSpace X]
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{f : X → E}
{s : Set X}
{μ : MeasureTheory.Measure X}
{C : ℝ}
(hs : μ s < ⊤)
(hsm : MeasurableSet s)
(hC : ∀ x ∈ s, ‖f x‖ ≤ C)
:
@[deprecated MeasureTheory.norm_setIntegral_le_of_norm_le_const']
theorem
MeasureTheory.norm_set_integral_le_of_norm_le_const'
{X : Type u_1}
{E : Type u_3}
[MeasurableSpace X]
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{f : X → E}
{s : Set X}
{μ : MeasureTheory.Measure X}
{C : ℝ}
(hs : μ s < ⊤)
(hsm : MeasurableSet s)
(hC : ∀ x ∈ s, ‖f x‖ ≤ C)
:
Alias of MeasureTheory.norm_setIntegral_le_of_norm_le_const'.
theorem
MeasureTheory.setIntegral_eq_zero_iff_of_nonneg_ae
{X : Type u_1}
[MeasurableSpace X]
{s : Set X}
{μ : MeasureTheory.Measure X}
{f : X → ℝ}
(hf : 0 ≤ᵐ[μ.restrict s] f)
(hfi : MeasureTheory.IntegrableOn f s μ)
:
@[deprecated MeasureTheory.setIntegral_eq_zero_iff_of_nonneg_ae]
theorem
MeasureTheory.set_integral_eq_zero_iff_of_nonneg_ae
{X : Type u_1}
[MeasurableSpace X]
{s : Set X}
{μ : MeasureTheory.Measure X}
{f : X → ℝ}
(hf : 0 ≤ᵐ[μ.restrict s] f)
(hfi : MeasureTheory.IntegrableOn f s μ)
:
Alias of MeasureTheory.setIntegral_eq_zero_iff_of_nonneg_ae.
theorem
MeasureTheory.setIntegral_pos_iff_support_of_nonneg_ae
{X : Type u_1}
[MeasurableSpace X]
{s : Set X}
{μ : MeasureTheory.Measure X}
{f : X → ℝ}
(hf : 0 ≤ᵐ[μ.restrict s] f)
(hfi : MeasureTheory.IntegrableOn f s μ)
:
0 < ∫ (x : X) in s, f x ∂μ ↔ 0 < μ (Function.support f ∩ s)
@[deprecated MeasureTheory.setIntegral_pos_iff_support_of_nonneg_ae]
theorem
MeasureTheory.set_integral_pos_iff_support_of_nonneg_ae
{X : Type u_1}
[MeasurableSpace X]
{s : Set X}
{μ : MeasureTheory.Measure X}
{f : X → ℝ}
(hf : 0 ≤ᵐ[μ.restrict s] f)
(hfi : MeasureTheory.IntegrableOn f s μ)
:
0 < ∫ (x : X) in s, f x ∂μ ↔ 0 < μ (Function.support f ∩ s)
Alias of MeasureTheory.setIntegral_pos_iff_support_of_nonneg_ae.
theorem
MeasureTheory.setIntegral_gt_gt
{X : Type u_1}
[MeasurableSpace X]
{μ : MeasureTheory.Measure X}
{R : ℝ}
{f : X → ℝ}
(hR : 0 ≤ R)
(hfint : MeasureTheory.IntegrableOn f {x : X | R < f x} μ)
(hμ : μ {x : X | R < f x} ≠ 0)
:
@[deprecated MeasureTheory.setIntegral_gt_gt]
theorem
MeasureTheory.set_integral_gt_gt
{X : Type u_1}
[MeasurableSpace X]
{μ : MeasureTheory.Measure X}
{R : ℝ}
{f : X → ℝ}
(hR : 0 ≤ R)
(hfint : MeasureTheory.IntegrableOn f {x : X | R < f x} μ)
(hμ : μ {x : X | R < f x} ≠ 0)
:
Alias of MeasureTheory.setIntegral_gt_gt.
theorem
MeasureTheory.setIntegral_trim
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{X : Type u_5}
{m : MeasurableSpace X}
{m0 : MeasurableSpace X}
{μ : MeasureTheory.Measure X}
(hm : m ≤ m0)
{f : X → E}
(hf_meas : MeasureTheory.StronglyMeasurable f)
{s : Set X}
(hs : MeasurableSet s)
:
∫ (x : X) in s, f x ∂μ = ∫ (x : X) in s, f x ∂μ.trim hm
@[deprecated MeasureTheory.setIntegral_trim]
theorem
MeasureTheory.set_integral_trim
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{X : Type u_5}
{m : MeasurableSpace X}
{m0 : MeasurableSpace X}
{μ : MeasureTheory.Measure X}
(hm : m ≤ m0)
{f : X → E}
(hf_meas : MeasureTheory.StronglyMeasurable f)
{s : Set X}
(hs : MeasurableSet s)
:
∫ (x : X) in s, f x ∂μ = ∫ (x : X) in s, f x ∂μ.trim hm
Alias of MeasureTheory.setIntegral_trim.
Lemmas about adding and removing interval boundaries #
The primed lemmas take explicit arguments about the endpoint having zero measure, while the
unprimed ones use [NoAtoms μ].
theorem
MeasureTheory.integral_Icc_eq_integral_Ioc'
{X : Type u_1}
{E : Type u_3}
[MeasurableSpace X]
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{f : X → E}
{μ : MeasureTheory.Measure X}
[PartialOrder X]
{x : X}
{y : X}
(hx : μ {x} = 0)
:
theorem
MeasureTheory.integral_Icc_eq_integral_Ico'
{X : Type u_1}
{E : Type u_3}
[MeasurableSpace X]
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{f : X → E}
{μ : MeasureTheory.Measure X}
[PartialOrder X]
{x : X}
{y : X}
(hy : μ {y} = 0)
:
theorem
MeasureTheory.integral_Ioc_eq_integral_Ioo'
{X : Type u_1}
{E : Type u_3}
[MeasurableSpace X]
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{f : X → E}
{μ : MeasureTheory.Measure X}
[PartialOrder X]
{x : X}
{y : X}
(hy : μ {y} = 0)
:
theorem
MeasureTheory.integral_Ico_eq_integral_Ioo'
{X : Type u_1}
{E : Type u_3}
[MeasurableSpace X]
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{f : X → E}
{μ : MeasureTheory.Measure X}
[PartialOrder X]
{x : X}
{y : X}
(hx : μ {x} = 0)
:
theorem
MeasureTheory.integral_Icc_eq_integral_Ioo'
{X : Type u_1}
{E : Type u_3}
[MeasurableSpace X]
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{f : X → E}
{μ : MeasureTheory.Measure X}
[PartialOrder X]
{x : X}
{y : X}
(hx : μ {x} = 0)
(hy : μ {y} = 0)
:
theorem
MeasureTheory.integral_Iic_eq_integral_Iio'
{X : Type u_1}
{E : Type u_3}
[MeasurableSpace X]
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{f : X → E}
{μ : MeasureTheory.Measure X}
[PartialOrder X]
{x : X}
(hx : μ {x} = 0)
:
theorem
MeasureTheory.integral_Ici_eq_integral_Ioi'
{X : Type u_1}
{E : Type u_3}
[MeasurableSpace X]
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{f : X → E}
{μ : MeasureTheory.Measure X}
[PartialOrder X]
{x : X}
(hx : μ {x} = 0)
:
theorem
MeasureTheory.integral_Icc_eq_integral_Ioc
{X : Type u_1}
{E : Type u_3}
[MeasurableSpace X]
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{f : X → E}
{μ : MeasureTheory.Measure X}
[PartialOrder X]
{x : X}
{y : X}
[MeasureTheory.NoAtoms μ]
:
theorem
MeasureTheory.integral_Icc_eq_integral_Ico
{X : Type u_1}
{E : Type u_3}
[MeasurableSpace X]
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{f : X → E}
{μ : MeasureTheory.Measure X}
[PartialOrder X]
{x : X}
{y : X}
[MeasureTheory.NoAtoms μ]
:
theorem
MeasureTheory.integral_Ioc_eq_integral_Ioo
{X : Type u_1}
{E : Type u_3}
[MeasurableSpace X]
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{f : X → E}
{μ : MeasureTheory.Measure X}
[PartialOrder X]
{x : X}
{y : X}
[MeasureTheory.NoAtoms μ]
:
theorem
MeasureTheory.integral_Ico_eq_integral_Ioo
{X : Type u_1}
{E : Type u_3}
[MeasurableSpace X]
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{f : X → E}
{μ : MeasureTheory.Measure X}
[PartialOrder X]
{x : X}
{y : X}
[MeasureTheory.NoAtoms μ]
:
theorem
MeasureTheory.integral_Icc_eq_integral_Ioo
{X : Type u_1}
{E : Type u_3}
[MeasurableSpace X]
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{f : X → E}
{μ : MeasureTheory.Measure X}
[PartialOrder X]
{x : X}
{y : X}
[MeasureTheory.NoAtoms μ]
:
theorem
MeasureTheory.integral_Iic_eq_integral_Iio
{X : Type u_1}
{E : Type u_3}
[MeasurableSpace X]
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{f : X → E}
{μ : MeasureTheory.Measure X}
[PartialOrder X]
{x : X}
[MeasureTheory.NoAtoms μ]
:
theorem
MeasureTheory.integral_Ici_eq_integral_Ioi
{X : Type u_1}
{E : Type u_3}
[MeasurableSpace X]
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{f : X → E}
{μ : MeasureTheory.Measure X}
[PartialOrder X]
{x : X}
[MeasureTheory.NoAtoms μ]
:
theorem
MeasureTheory.setIntegral_mono_ae_restrict
{X : Type u_1}
[MeasurableSpace X]
{μ : MeasureTheory.Measure X}
{f : X → ℝ}
{g : X → ℝ}
{s : Set X}
(hf : MeasureTheory.IntegrableOn f s μ)
(hg : MeasureTheory.IntegrableOn g s μ)
(h : f ≤ᵐ[μ.restrict s] g)
:
∫ (x : X) in s, f x ∂μ ≤ ∫ (x : X) in s, g x ∂μ
@[deprecated MeasureTheory.setIntegral_mono_ae_restrict]
theorem
MeasureTheory.set_integral_mono_ae_restrict
{X : Type u_1}
[MeasurableSpace X]
{μ : MeasureTheory.Measure X}
{f : X → ℝ}
{g : X → ℝ}
{s : Set X}
(hf : MeasureTheory.IntegrableOn f s μ)
(hg : MeasureTheory.IntegrableOn g s μ)
(h : f ≤ᵐ[μ.restrict s] g)
:
∫ (x : X) in s, f x ∂μ ≤ ∫ (x : X) in s, g x ∂μ
theorem
MeasureTheory.setIntegral_mono_ae
{X : Type u_1}
[MeasurableSpace X]
{μ : MeasureTheory.Measure X}
{f : X → ℝ}
{g : X → ℝ}
{s : Set X}
(hf : MeasureTheory.IntegrableOn f s μ)
(hg : MeasureTheory.IntegrableOn g s μ)
(h : f ≤ᵐ[μ] g)
:
∫ (x : X) in s, f x ∂μ ≤ ∫ (x : X) in s, g x ∂μ
@[deprecated MeasureTheory.setIntegral_mono_ae]
theorem
MeasureTheory.set_integral_mono_ae
{X : Type u_1}
[MeasurableSpace X]
{μ : MeasureTheory.Measure X}
{f : X → ℝ}
{g : X → ℝ}
{s : Set X}
(hf : MeasureTheory.IntegrableOn f s μ)
(hg : MeasureTheory.IntegrableOn g s μ)
(h : f ≤ᵐ[μ] g)
:
∫ (x : X) in s, f x ∂μ ≤ ∫ (x : X) in s, g x ∂μ
Alias of MeasureTheory.setIntegral_mono_ae.
theorem
MeasureTheory.setIntegral_mono_on
{X : Type u_1}
[MeasurableSpace X]
{μ : MeasureTheory.Measure X}
{f : X → ℝ}
{g : X → ℝ}
{s : Set X}
(hf : MeasureTheory.IntegrableOn f s μ)
(hg : MeasureTheory.IntegrableOn g s μ)
(hs : MeasurableSet s)
(h : ∀ x ∈ s, f x ≤ g x)
:
∫ (x : X) in s, f x ∂μ ≤ ∫ (x : X) in s, g x ∂μ
@[deprecated MeasureTheory.setIntegral_mono_on]
theorem
MeasureTheory.set_integral_mono_on
{X : Type u_1}
[MeasurableSpace X]
{μ : MeasureTheory.Measure X}
{f : X → ℝ}
{g : X → ℝ}
{s : Set X}
(hf : MeasureTheory.IntegrableOn f s μ)
(hg : MeasureTheory.IntegrableOn g s μ)
(hs : MeasurableSet s)
(h : ∀ x ∈ s, f x ≤ g x)
:
∫ (x : X) in s, f x ∂μ ≤ ∫ (x : X) in s, g x ∂μ
Alias of MeasureTheory.setIntegral_mono_on.
theorem
MeasureTheory.setIntegral_mono_on_ae
{X : Type u_1}
[MeasurableSpace X]
{μ : MeasureTheory.Measure X}
{f : X → ℝ}
{g : X → ℝ}
{s : Set X}
(hf : MeasureTheory.IntegrableOn f s μ)
(hg : MeasureTheory.IntegrableOn g s μ)
(hs : MeasurableSet s)
(h : ∀ᵐ (x : X) ∂μ, x ∈ s → f x ≤ g x)
:
∫ (x : X) in s, f x ∂μ ≤ ∫ (x : X) in s, g x ∂μ
@[deprecated MeasureTheory.setIntegral_mono_on_ae]
theorem
MeasureTheory.set_integral_mono_on_ae
{X : Type u_1}
[MeasurableSpace X]
{μ : MeasureTheory.Measure X}
{f : X → ℝ}
{g : X → ℝ}
{s : Set X}
(hf : MeasureTheory.IntegrableOn f s μ)
(hg : MeasureTheory.IntegrableOn g s μ)
(hs : MeasurableSet s)
(h : ∀ᵐ (x : X) ∂μ, x ∈ s → f x ≤ g x)
:
∫ (x : X) in s, f x ∂μ ≤ ∫ (x : X) in s, g x ∂μ
Alias of MeasureTheory.setIntegral_mono_on_ae.
theorem
MeasureTheory.setIntegral_mono
{X : Type u_1}
[MeasurableSpace X]
{μ : MeasureTheory.Measure X}
{f : X → ℝ}
{g : X → ℝ}
{s : Set X}
(hf : MeasureTheory.IntegrableOn f s μ)
(hg : MeasureTheory.IntegrableOn g s μ)
(h : f ≤ g)
:
∫ (x : X) in s, f x ∂μ ≤ ∫ (x : X) in s, g x ∂μ
@[deprecated MeasureTheory.setIntegral_mono]
theorem
MeasureTheory.set_integral_mono
{X : Type u_1}
[MeasurableSpace X]
{μ : MeasureTheory.Measure X}
{f : X → ℝ}
{g : X → ℝ}
{s : Set X}
(hf : MeasureTheory.IntegrableOn f s μ)
(hg : MeasureTheory.IntegrableOn g s μ)
(h : f ≤ g)
:
∫ (x : X) in s, f x ∂μ ≤ ∫ (x : X) in s, g x ∂μ
Alias of MeasureTheory.setIntegral_mono.
theorem
MeasureTheory.setIntegral_mono_set
{X : Type u_1}
[MeasurableSpace X]
{μ : MeasureTheory.Measure X}
{f : X → ℝ}
{s : Set X}
{t : Set X}
(hfi : MeasureTheory.IntegrableOn f t μ)
(hf : 0 ≤ᵐ[μ.restrict t] f)
(hst : s ≤ᵐ[μ] t)
:
∫ (x : X) in s, f x ∂μ ≤ ∫ (x : X) in t, f x ∂μ
@[deprecated MeasureTheory.setIntegral_mono_set]
theorem
MeasureTheory.set_integral_mono_set
{X : Type u_1}
[MeasurableSpace X]
{μ : MeasureTheory.Measure X}
{f : X → ℝ}
{s : Set X}
{t : Set X}
(hfi : MeasureTheory.IntegrableOn f t μ)
(hf : 0 ≤ᵐ[μ.restrict t] f)
(hst : s ≤ᵐ[μ] t)
:
∫ (x : X) in s, f x ∂μ ≤ ∫ (x : X) in t, f x ∂μ
Alias of MeasureTheory.setIntegral_mono_set.
theorem
MeasureTheory.setIntegral_le_integral
{X : Type u_1}
[MeasurableSpace X]
{μ : MeasureTheory.Measure X}
{f : X → ℝ}
{s : Set X}
(hfi : MeasureTheory.Integrable f μ)
(hf : 0 ≤ᵐ[μ] f)
:
∫ (x : X) in s, f x ∂μ ≤ ∫ (x : X), f x ∂μ
@[deprecated MeasureTheory.setIntegral_le_integral]
theorem
MeasureTheory.set_integral_le_integral
{X : Type u_1}
[MeasurableSpace X]
{μ : MeasureTheory.Measure X}
{f : X → ℝ}
{s : Set X}
(hfi : MeasureTheory.Integrable f μ)
(hf : 0 ≤ᵐ[μ] f)
:
∫ (x : X) in s, f x ∂μ ≤ ∫ (x : X), f x ∂μ
Alias of MeasureTheory.setIntegral_le_integral.
theorem
MeasureTheory.setIntegral_ge_of_const_le
{X : Type u_1}
[MeasurableSpace X]
{μ : MeasureTheory.Measure X}
{f : X → ℝ}
{s : Set X}
{c : ℝ}
(hs : MeasurableSet s)
(hμs : μ s ≠ ⊤)
(hf : ∀ x ∈ s, c ≤ f x)
(hfint : MeasureTheory.IntegrableOn (fun (x : X) => f x) s μ)
:
@[deprecated MeasureTheory.setIntegral_ge_of_const_le]
theorem
MeasureTheory.set_integral_ge_of_const_le
{X : Type u_1}
[MeasurableSpace X]
{μ : MeasureTheory.Measure X}
{f : X → ℝ}
{s : Set X}
{c : ℝ}
(hs : MeasurableSet s)
(hμs : μ s ≠ ⊤)
(hf : ∀ x ∈ s, c ≤ f x)
(hfint : MeasureTheory.IntegrableOn (fun (x : X) => f x) s μ)
:
Alias of MeasureTheory.setIntegral_ge_of_const_le.
theorem
MeasureTheory.setIntegral_nonneg_of_ae_restrict
{X : Type u_1}
[MeasurableSpace X]
{μ : MeasureTheory.Measure X}
{f : X → ℝ}
{s : Set X}
(hf : 0 ≤ᵐ[μ.restrict s] f)
:
0 ≤ ∫ (x : X) in s, f x ∂μ
@[deprecated MeasureTheory.setIntegral_nonneg_of_ae_restrict]
theorem
MeasureTheory.set_integral_nonneg_of_ae_restrict
{X : Type u_1}
[MeasurableSpace X]
{μ : MeasureTheory.Measure X}
{f : X → ℝ}
{s : Set X}
(hf : 0 ≤ᵐ[μ.restrict s] f)
:
0 ≤ ∫ (x : X) in s, f x ∂μ
theorem
MeasureTheory.setIntegral_nonneg_of_ae
{X : Type u_1}
[MeasurableSpace X]
{μ : MeasureTheory.Measure X}
{f : X → ℝ}
{s : Set X}
(hf : 0 ≤ᵐ[μ] f)
:
0 ≤ ∫ (x : X) in s, f x ∂μ
@[deprecated MeasureTheory.setIntegral_nonneg_of_ae]
theorem
MeasureTheory.set_integral_nonneg_of_ae
{X : Type u_1}
[MeasurableSpace X]
{μ : MeasureTheory.Measure X}
{f : X → ℝ}
{s : Set X}
(hf : 0 ≤ᵐ[μ] f)
:
0 ≤ ∫ (x : X) in s, f x ∂μ
Alias of MeasureTheory.setIntegral_nonneg_of_ae.
theorem
MeasureTheory.setIntegral_nonneg
{X : Type u_1}
[MeasurableSpace X]
{μ : MeasureTheory.Measure X}
{f : X → ℝ}
{s : Set X}
(hs : MeasurableSet s)
(hf : ∀ x ∈ s, 0 ≤ f x)
:
0 ≤ ∫ (x : X) in s, f x ∂μ
@[deprecated MeasureTheory.setIntegral_nonneg]
theorem
MeasureTheory.set_integral_nonneg
{X : Type u_1}
[MeasurableSpace X]
{μ : MeasureTheory.Measure X}
{f : X → ℝ}
{s : Set X}
(hs : MeasurableSet s)
(hf : ∀ x ∈ s, 0 ≤ f x)
:
0 ≤ ∫ (x : X) in s, f x ∂μ
Alias of MeasureTheory.setIntegral_nonneg.
theorem
MeasureTheory.setIntegral_nonneg_ae
{X : Type u_1}
[MeasurableSpace X]
{μ : MeasureTheory.Measure X}
{f : X → ℝ}
{s : Set X}
(hs : MeasurableSet s)
(hf : ∀ᵐ (x : X) ∂μ, x ∈ s → 0 ≤ f x)
:
0 ≤ ∫ (x : X) in s, f x ∂μ
@[deprecated MeasureTheory.setIntegral_nonneg_ae]
theorem
MeasureTheory.set_integral_nonneg_ae
{X : Type u_1}
[MeasurableSpace X]
{μ : MeasureTheory.Measure X}
{f : X → ℝ}
{s : Set X}
(hs : MeasurableSet s)
(hf : ∀ᵐ (x : X) ∂μ, x ∈ s → 0 ≤ f x)
:
0 ≤ ∫ (x : X) in s, f x ∂μ
Alias of MeasureTheory.setIntegral_nonneg_ae.
theorem
MeasureTheory.setIntegral_le_nonneg
{X : Type u_1}
[MeasurableSpace X]
{μ : MeasureTheory.Measure X}
{f : X → ℝ}
{s : Set X}
(hs : MeasurableSet s)
(hf : MeasureTheory.StronglyMeasurable f)
(hfi : MeasureTheory.Integrable f μ)
:
@[deprecated MeasureTheory.setIntegral_le_nonneg]
theorem
MeasureTheory.set_integral_le_nonneg
{X : Type u_1}
[MeasurableSpace X]
{μ : MeasureTheory.Measure X}
{f : X → ℝ}
{s : Set X}
(hs : MeasurableSet s)
(hf : MeasureTheory.StronglyMeasurable f)
(hfi : MeasureTheory.Integrable f μ)
:
Alias of MeasureTheory.setIntegral_le_nonneg.
theorem
MeasureTheory.setIntegral_nonpos_of_ae_restrict
{X : Type u_1}
[MeasurableSpace X]
{μ : MeasureTheory.Measure X}
{f : X → ℝ}
{s : Set X}
(hf : f ≤ᵐ[μ.restrict s] 0)
:
∫ (x : X) in s, f x ∂μ ≤ 0
@[deprecated MeasureTheory.setIntegral_nonpos_of_ae_restrict]
theorem
MeasureTheory.set_integral_nonpos_of_ae_restrict
{X : Type u_1}
[MeasurableSpace X]
{μ : MeasureTheory.Measure X}
{f : X → ℝ}
{s : Set X}
(hf : f ≤ᵐ[μ.restrict s] 0)
:
∫ (x : X) in s, f x ∂μ ≤ 0
theorem
MeasureTheory.setIntegral_nonpos_of_ae
{X : Type u_1}
[MeasurableSpace X]
{μ : MeasureTheory.Measure X}
{f : X → ℝ}
{s : Set X}
(hf : f ≤ᵐ[μ] 0)
:
∫ (x : X) in s, f x ∂μ ≤ 0
@[deprecated MeasureTheory.setIntegral_nonpos_of_ae]
theorem
MeasureTheory.set_integral_nonpos_of_ae
{X : Type u_1}
[MeasurableSpace X]
{μ : MeasureTheory.Measure X}
{f : X → ℝ}
{s : Set X}
(hf : f ≤ᵐ[μ] 0)
:
∫ (x : X) in s, f x ∂μ ≤ 0
Alias of MeasureTheory.setIntegral_nonpos_of_ae.
theorem
MeasureTheory.setIntegral_nonpos_ae
{X : Type u_1}
[MeasurableSpace X]
{μ : MeasureTheory.Measure X}
{f : X → ℝ}
{s : Set X}
(hs : MeasurableSet s)
(hf : ∀ᵐ (x : X) ∂μ, x ∈ s → f x ≤ 0)
:
∫ (x : X) in s, f x ∂μ ≤ 0
@[deprecated MeasureTheory.setIntegral_nonpos_ae]
theorem
MeasureTheory.set_integral_nonpos_ae
{X : Type u_1}
[MeasurableSpace X]
{μ : MeasureTheory.Measure X}
{f : X → ℝ}
{s : Set X}
(hs : MeasurableSet s)
(hf : ∀ᵐ (x : X) ∂μ, x ∈ s → f x ≤ 0)
:
∫ (x : X) in s, f x ∂μ ≤ 0
Alias of MeasureTheory.setIntegral_nonpos_ae.
theorem
MeasureTheory.setIntegral_nonpos
{X : Type u_1}
[MeasurableSpace X]
{μ : MeasureTheory.Measure X}
{f : X → ℝ}
{s : Set X}
(hs : MeasurableSet s)
(hf : ∀ x ∈ s, f x ≤ 0)
:
∫ (x : X) in s, f x ∂μ ≤ 0
@[deprecated MeasureTheory.setIntegral_nonpos]
theorem
MeasureTheory.set_integral_nonpos
{X : Type u_1}
[MeasurableSpace X]
{μ : MeasureTheory.Measure X}
{f : X → ℝ}
{s : Set X}
(hs : MeasurableSet s)
(hf : ∀ x ∈ s, f x ≤ 0)
:
∫ (x : X) in s, f x ∂μ ≤ 0
Alias of MeasureTheory.setIntegral_nonpos.
theorem
MeasureTheory.setIntegral_nonpos_le
{X : Type u_1}
[MeasurableSpace X]
{μ : MeasureTheory.Measure X}
{f : X → ℝ}
{s : Set X}
(hs : MeasurableSet s)
(hf : MeasureTheory.StronglyMeasurable f)
(hfi : MeasureTheory.Integrable f μ)
:
@[deprecated MeasureTheory.setIntegral_nonpos_le]
theorem
MeasureTheory.set_integral_nonpos_le
{X : Type u_1}
[MeasurableSpace X]
{μ : MeasureTheory.Measure X}
{f : X → ℝ}
{s : Set X}
(hs : MeasurableSet s)
(hf : MeasureTheory.StronglyMeasurable f)
(hfi : MeasureTheory.Integrable f μ)
:
Alias of MeasureTheory.setIntegral_nonpos_le.
theorem
MeasureTheory.Integrable.measure_le_integral
{X : Type u_1}
[MeasurableSpace X]
{μ : MeasureTheory.Measure X}
{f : X → ℝ}
(f_int : MeasureTheory.Integrable f μ)
(f_nonneg : 0 ≤ᵐ[μ] f)
{s : Set X}
(hs : ∀ x ∈ s, 1 ≤ f x)
:
μ s ≤ ENNReal.ofReal (∫ (x : X), f x ∂μ)
theorem
MeasureTheory.integral_le_measure
{X : Type u_1}
[MeasurableSpace X]
{μ : MeasureTheory.Measure X}
{f : X → ℝ}
{s : Set X}
(hs : ∀ x ∈ s, f x ≤ 1)
(h's : ∀ x ∈ sᶜ, f x ≤ 0)
:
ENNReal.ofReal (∫ (x : X), f x ∂μ) ≤ μ s
theorem
MeasureTheory.integrableOn_iUnion_of_summable_integral_norm
{X : Type u_1}
{E : Type u_3}
[MeasurableSpace X]
{ι : Type u_5}
[Countable ι]
{μ : MeasureTheory.Measure X}
[NormedAddCommGroup E]
{f : X → E}
{s : ι → Set X}
(hs : ∀ (i : ι), MeasurableSet (s i))
(hi : ∀ (i : ι), MeasureTheory.IntegrableOn f (s i) μ)
(h : Summable fun (i : ι) => ∫ (x : X) in s i, ‖f x‖ ∂μ)
:
MeasureTheory.IntegrableOn f (Set.iUnion s) μ
theorem
MeasureTheory.integrableOn_iUnion_of_summable_norm_restrict
{X : Type u_1}
{E : Type u_3}
[MeasurableSpace X]
{ι : Type u_5}
[Countable ι]
{μ : MeasureTheory.Measure X}
[NormedAddCommGroup E]
[TopologicalSpace X]
[BorelSpace X]
[TopologicalSpace.MetrizableSpace X]
[MeasureTheory.IsLocallyFiniteMeasure μ]
{f : C(X, E)}
{s : ι → TopologicalSpace.Compacts X}
(hf : Summable fun (i : ι) => ‖ContinuousMap.restrict (↑(s i)) f‖ * (μ ↑(s i)).toReal)
:
MeasureTheory.IntegrableOn (⇑f) (⋃ (i : ι), ↑(s i)) μ
If s is a countable family of compact sets, f is a continuous function, and the sequence
‖f.restrict (s i)‖ * μ (s i) is summable, then f is integrable on the union of the s i.
theorem
MeasureTheory.integrable_of_summable_norm_restrict
{X : Type u_1}
{E : Type u_3}
[MeasurableSpace X]
{ι : Type u_5}
[Countable ι]
{μ : MeasureTheory.Measure X}
[NormedAddCommGroup E]
[TopologicalSpace X]
[BorelSpace X]
[TopologicalSpace.MetrizableSpace X]
[MeasureTheory.IsLocallyFiniteMeasure μ]
{f : C(X, E)}
{s : ι → TopologicalSpace.Compacts X}
(hf : Summable fun (i : ι) => ‖ContinuousMap.restrict (↑(s i)) f‖ * (μ ↑(s i)).toReal)
(hs : ⋃ (i : ι), ↑(s i) = Set.univ)
:
MeasureTheory.Integrable (⇑f) μ
If s is a countable family of compact sets covering X, f is a continuous function, and
the sequence ‖f.restrict (s i)‖ * μ (s i) is summable, then f is integrable.
Continuity of the set integral #
We prove that for any set s, the function
fun f : X →₁[μ] E => ∫ x in s, f x ∂μ is continuous.
theorem
MeasureTheory.Lp_toLp_restrict_add
{X : Type u_1}
{E : Type u_3}
[MeasurableSpace X]
[NormedAddCommGroup E]
{p : ENNReal}
{μ : MeasureTheory.Measure X}
(f : ↥(MeasureTheory.Lp E p μ))
(g : ↥(MeasureTheory.Lp E p μ))
(s : Set X)
:
MeasureTheory.Memℒp.toLp ↑↑(f + g) ⋯ = MeasureTheory.Memℒp.toLp ↑↑f ⋯ + MeasureTheory.Memℒp.toLp ↑↑g ⋯
For f : Lp E p μ, we can define an element of Lp E p (μ.restrict s) by
(Lp.memℒp f).restrict s).toLp f. This map is additive.
theorem
MeasureTheory.Lp_toLp_restrict_smul
{X : Type u_1}
{F : Type u_4}
[MeasurableSpace X]
{𝕜 : Type u_5}
[NormedField 𝕜]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{p : ENNReal}
{μ : MeasureTheory.Measure X}
(c : 𝕜)
(f : ↥(MeasureTheory.Lp F p μ))
(s : Set X)
:
MeasureTheory.Memℒp.toLp ↑↑(c • f) ⋯ = c • MeasureTheory.Memℒp.toLp ↑↑f ⋯
For f : Lp E p μ, we can define an element of Lp E p (μ.restrict s) by
(Lp.memℒp f).restrict s).toLp f. This map commutes with scalar multiplication.
theorem
MeasureTheory.norm_Lp_toLp_restrict_le
{X : Type u_1}
{E : Type u_3}
[MeasurableSpace X]
[NormedAddCommGroup E]
{p : ENNReal}
{μ : MeasureTheory.Measure X}
(s : Set X)
(f : ↥(MeasureTheory.Lp E p μ))
:
For f : Lp E p μ, we can define an element of Lp E p (μ.restrict s) by
(Lp.memℒp f).restrict s).toLp f. This map is non-expansive.
def
MeasureTheory.LpToLpRestrictCLM
(X : Type u_1)
(F : Type u_4)
[MeasurableSpace X]
(𝕜 : Type u_5)
[NormedField 𝕜]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
(μ : MeasureTheory.Measure X)
(p : ENNReal)
[hp : Fact (1 ≤ p)]
(s : Set X)
:
↥(MeasureTheory.Lp F p μ) →L[𝕜] ↥(MeasureTheory.Lp F p (μ.restrict s))
Continuous linear map sending a function of Lp F p μ to the same function in
Lp F p (μ.restrict s).
Equations
- MeasureTheory.LpToLpRestrictCLM X F 𝕜 μ p s = { toFun := fun (f : ↥(MeasureTheory.Lp F p μ)) => MeasureTheory.Memℒp.toLp ↑↑f ⋯, map_add' := ⋯, map_smul' := ⋯ }.mkContinuous 1 ⋯
Instances For
theorem
MeasureTheory.LpToLpRestrictCLM_coeFn
{X : Type u_1}
{F : Type u_4}
[MeasurableSpace X]
(𝕜 : Type u_5)
[NormedField 𝕜]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{p : ENNReal}
{μ : MeasureTheory.Measure X}
[Fact (1 ≤ p)]
(s : Set X)
(f : ↥(MeasureTheory.Lp F p μ))
:
↑↑((MeasureTheory.LpToLpRestrictCLM X F 𝕜 μ p s) f) =ᵐ[μ.restrict s] ↑↑f
theorem
MeasureTheory.continuous_setIntegral
{X : Type u_1}
{E : Type u_3}
[MeasurableSpace X]
[NormedAddCommGroup E]
{μ : MeasureTheory.Measure X}
[NormedSpace ℝ E]
(s : Set X)
:
Continuous fun (f : ↥(MeasureTheory.Lp E 1 μ)) => ∫ (x : X) in s, ↑↑f x ∂μ
@[deprecated MeasureTheory.continuous_setIntegral]
theorem
MeasureTheory.continuous_set_integral
{X : Type u_1}
{E : Type u_3}
[MeasurableSpace X]
[NormedAddCommGroup E]
{μ : MeasureTheory.Measure X}
[NormedSpace ℝ E]
(s : Set X)
:
Continuous fun (f : ↥(MeasureTheory.Lp E 1 μ)) => ∫ (x : X) in s, ↑↑f x ∂μ
Alias of MeasureTheory.continuous_setIntegral.
theorem
Continuous.integral_pos_of_hasCompactSupport_nonneg_nonzero
{X : Type u_1}
[MeasurableSpace X]
[TopologicalSpace X]
[OpensMeasurableSpace X]
{μ : MeasureTheory.Measure X}
[μ.IsOpenPosMeasure]
[MeasureTheory.IsFiniteMeasureOnCompacts μ]
{f : X → ℝ}
{x : X}
(f_cont : Continuous f)
(f_comp : HasCompactSupport f)
(f_nonneg : 0 ≤ f)
(f_x : f x ≠ 0)
:
0 < ∫ (x : X), f x ∂μ
Fundamental theorem of calculus for set integrals
theorem
Filter.Tendsto.integral_sub_linear_isLittleO_ae
{X : Type u_1}
{E : Type u_3}
[MeasurableSpace X]
{ι : Type u_5}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[CompleteSpace E]
{μ : MeasureTheory.Measure X}
{l : Filter X}
[l.IsMeasurablyGenerated]
{f : X → E}
{b : E}
(h : Filter.Tendsto f (l ⊓ MeasureTheory.ae μ) (nhds b))
(hfm : StronglyMeasurableAtFilter f l μ)
(hμ : μ.FiniteAtFilter l)
{s : ι → Set X}
{li : Filter ι}
(hs : Filter.Tendsto s li l.smallSets)
(m : optParam (ι → ℝ) fun (i : ι) => (μ (s i)).toReal)
(hsμ : autoParam ((fun (i : ι) => (μ (s i)).toReal) =ᶠ[li] m) _auto✝)
:
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.smallSets along li.
Since μ (s i) is an ℝ≥0∞ number, we use (μ (s i)).toReal in the actual statement.
Often there is a good formula for (μ (s i)).toReal, so the formalization can take an optional
argument m with this formula and a proof of (fun i => (μ (s i)).toReal) =ᶠ[li] m. Without these
arguments, m i = (μ (s i)).toReal is used in the output.
theorem
ContinuousWithinAt.integral_sub_linear_isLittleO_ae
{X : Type u_1}
{E : Type u_3}
[MeasurableSpace X]
{ι : Type u_5}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[CompleteSpace E]
[TopologicalSpace X]
[OpensMeasurableSpace X]
{μ : MeasureTheory.Measure X}
[MeasureTheory.IsLocallyFiniteMeasure μ]
{x : X}
{t : Set X}
{f : X → E}
(hx : ContinuousWithinAt f t x)
(ht : MeasurableSet t)
(hfm : StronglyMeasurableAtFilter f (nhdsWithin x t) μ)
{s : ι → Set X}
{li : Filter ι}
(hs : Filter.Tendsto s li (nhdsWithin x t).smallSets)
(m : optParam (ι → ℝ) fun (i : ι) => (μ (s i)).toReal)
(hsμ : autoParam ((fun (i : ι) => (μ (s i)).toReal) =ᶠ[li] m) _auto✝)
:
Fundamental theorem of calculus for set integrals, nhdsWithin 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).smallSets along li. Since μ (s i) is an ℝ≥0∞
number, we use (μ (s i)).toReal in the actual statement.
Often there is a good formula for (μ (s i)).toReal, so the formalization can take an optional
argument m with this formula and a proof of (fun i => (μ (s i)).toReal) =ᶠ[li] m. Without these
arguments, m i = (μ (s i)).toReal is used in the output.
theorem
ContinuousAt.integral_sub_linear_isLittleO_ae
{X : Type u_1}
{E : Type u_3}
[MeasurableSpace X]
{ι : Type u_5}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[CompleteSpace E]
[TopologicalSpace X]
[OpensMeasurableSpace X]
{μ : MeasureTheory.Measure X}
[MeasureTheory.IsLocallyFiniteMeasure μ]
{x : X}
{f : X → E}
(hx : ContinuousAt f x)
(hfm : StronglyMeasurableAtFilter f (nhds x) μ)
{s : ι → Set X}
{li : Filter ι}
(hs : Filter.Tendsto s li (nhds x).smallSets)
(m : optParam (ι → ℝ) fun (i : ι) => (μ (s i)).toReal)
(hsμ : autoParam ((fun (i : ι) => (μ (s i)).toReal) =ᶠ[li] m) _auto✝)
:
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).smallSets along li. Since μ (s i) is an ℝ≥0∞ number, we use (μ (s i)).toReal in
the actual statement.
Often there is a good formula for (μ (s i)).toReal, so the formalization can take an optional
argument m with this formula and a proof of (fun i => (μ (s i)).toReal) =ᶠ[li] m. Without these
arguments, m i = (μ (s i)).toReal is used in the output.
theorem
ContinuousOn.integral_sub_linear_isLittleO_ae
{X : Type u_1}
{E : Type u_3}
[MeasurableSpace X]
{ι : Type u_5}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[CompleteSpace E]
[TopologicalSpace X]
[OpensMeasurableSpace X]
[SecondCountableTopologyEither X E]
{μ : MeasureTheory.Measure X}
[MeasureTheory.IsLocallyFiniteMeasure μ]
{x : X}
{t : Set X}
{f : X → E}
(hft : ContinuousOn f t)
(hx : x ∈ t)
(ht : MeasurableSet t)
{s : ι → Set X}
{li : Filter ι}
(hs : Filter.Tendsto s li (nhdsWithin x t).smallSets)
(m : optParam (ι → ℝ) fun (i : ι) => (μ (s i)).toReal)
(hsμ : autoParam ((fun (i : ι) => (μ (s i)).toReal) =ᶠ[li] m) _auto✝)
:
Fundamental theorem of calculus for set integrals, nhdsWithin 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).smallSets along li.
Since μ (s i) is an ℝ≥0∞ number, we use (μ (s i)).toReal in the actual statement.
Often there is a good formula for (μ (s i)).toReal, so the formalization can take an optional
argument m with this formula and a proof of (fun i => (μ (s i)).toReal) =ᶠ[li] m. Without these
arguments, m i = (μ (s i)).toReal is used in the output.
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 ContinuousLinearMap.compLp. We take advantage of this construction here.
theorem
ContinuousLinearMap.integral_compLp
{X : Type u_1}
{E : Type u_3}
{F : Type u_4}
[MeasurableSpace X]
{μ : MeasureTheory.Measure X}
{𝕜 : Type u_5}
[RCLike 𝕜]
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{p : ENNReal}
[NormedSpace ℝ F]
(L : E →L[𝕜] F)
(φ : ↥(MeasureTheory.Lp E p μ))
:
∫ (x : X), ↑↑(L.compLp φ) x ∂μ = ∫ (x : X), L (↑↑φ x) ∂μ
theorem
ContinuousLinearMap.setIntegral_compLp
{X : Type u_1}
{E : Type u_3}
{F : Type u_4}
[MeasurableSpace X]
{μ : MeasureTheory.Measure X}
{𝕜 : Type u_5}
[RCLike 𝕜]
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{p : ENNReal}
[NormedSpace ℝ F]
(L : E →L[𝕜] F)
(φ : ↥(MeasureTheory.Lp E p μ))
{s : Set X}
(hs : MeasurableSet s)
:
∫ (x : X) in s, ↑↑(L.compLp φ) x ∂μ = ∫ (x : X) in s, L (↑↑φ x) ∂μ
@[deprecated ContinuousLinearMap.setIntegral_compLp]
theorem
ContinuousLinearMap.set_integral_compLp
{X : Type u_1}
{E : Type u_3}
{F : Type u_4}
[MeasurableSpace X]
{μ : MeasureTheory.Measure X}
{𝕜 : Type u_5}
[RCLike 𝕜]
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{p : ENNReal}
[NormedSpace ℝ F]
(L : E →L[𝕜] F)
(φ : ↥(MeasureTheory.Lp E p μ))
{s : Set X}
(hs : MeasurableSet s)
:
∫ (x : X) in s, ↑↑(L.compLp φ) x ∂μ = ∫ (x : X) in s, L (↑↑φ x) ∂μ
Alias of ContinuousLinearMap.setIntegral_compLp.
theorem
ContinuousLinearMap.continuous_integral_comp_L1
{X : Type u_1}
{E : Type u_3}
{F : Type u_4}
[MeasurableSpace X]
{μ : MeasureTheory.Measure X}
{𝕜 : Type u_5}
[RCLike 𝕜]
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
[NormedSpace ℝ F]
(L : E →L[𝕜] F)
:
Continuous fun (φ : ↥(MeasureTheory.Lp E 1 μ)) => ∫ (x : X), L (↑↑φ x) ∂μ
theorem
ContinuousLinearMap.integral_comp_comm
{X : Type u_1}
{E : Type u_3}
{F : Type u_4}
[MeasurableSpace X]
{μ : MeasureTheory.Measure X}
{𝕜 : Type u_5}
[RCLike 𝕜]
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
[NormedSpace ℝ F]
[CompleteSpace F]
[NormedSpace ℝ E]
[CompleteSpace E]
(L : E →L[𝕜] F)
{φ : X → E}
(φ_int : MeasureTheory.Integrable φ μ)
:
∫ (x : X), L (φ x) ∂μ = L (∫ (x : X), φ x ∂μ)
theorem
ContinuousLinearMap.integral_apply
{X : Type u_1}
{E : Type u_3}
[MeasurableSpace X]
{μ : MeasureTheory.Measure X}
{𝕜 : Type u_5}
[RCLike 𝕜]
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[NormedSpace ℝ E]
{H : Type u_6}
[NormedAddCommGroup H]
[NormedSpace 𝕜 H]
{φ : X → H →L[𝕜] E}
(φ_int : MeasureTheory.Integrable φ μ)
(v : H)
:
(∫ (x : X), φ x ∂μ) v = ∫ (x : X), (φ x) v ∂μ
theorem
ContinuousMultilinearMap.integral_apply
{X : Type u_1}
{E : Type u_3}
[MeasurableSpace X]
{μ : MeasureTheory.Measure X}
{𝕜 : Type u_5}
[RCLike 𝕜]
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[NormedSpace ℝ E]
{ι : Type u_6}
[Fintype ι]
{M : ι → Type u_7}
[(i : ι) → NormedAddCommGroup (M i)]
[(i : ι) → NormedSpace 𝕜 (M i)]
{φ : X → ContinuousMultilinearMap 𝕜 M E}
(φ_int : MeasureTheory.Integrable φ μ)
(m : (i : ι) → M i)
:
(∫ (x : X), φ x ∂μ) m = ∫ (x : X), (φ x) m ∂μ
theorem
ContinuousLinearMap.integral_comp_comm'
{X : Type u_1}
{E : Type u_3}
{F : Type u_4}
[MeasurableSpace X]
{μ : MeasureTheory.Measure X}
{𝕜 : Type u_5}
[RCLike 𝕜]
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
[NormedSpace ℝ F]
[CompleteSpace F]
[NormedSpace ℝ E]
[CompleteSpace E]
(L : E →L[𝕜] F)
{K : NNReal}
(hL : AntilipschitzWith K ⇑L)
(φ : X → E)
:
∫ (x : X), L (φ x) ∂μ = L (∫ (x : X), φ x ∂μ)
theorem
ContinuousLinearMap.integral_comp_L1_comm
{X : Type u_1}
{E : Type u_3}
{F : Type u_4}
[MeasurableSpace X]
{μ : MeasureTheory.Measure X}
{𝕜 : Type u_5}
[RCLike 𝕜]
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
[NormedSpace ℝ F]
[CompleteSpace F]
[NormedSpace ℝ E]
[CompleteSpace E]
(L : E →L[𝕜] F)
(φ : ↥(MeasureTheory.Lp E 1 μ))
:
∫ (x : X), L (↑↑φ x) ∂μ = L (∫ (x : X), ↑↑φ x ∂μ)
theorem
LinearIsometry.integral_comp_comm
{X : Type u_1}
{E : Type u_3}
{F : Type u_4}
[MeasurableSpace X]
{μ : MeasureTheory.Measure X}
{𝕜 : Type u_5}
[RCLike 𝕜]
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
[CompleteSpace F]
[NormedSpace ℝ F]
[CompleteSpace E]
[NormedSpace ℝ E]
(L : E →ₗᵢ[𝕜] F)
(φ : X → E)
:
∫ (x : X), L (φ x) ∂μ = L (∫ (x : X), φ x ∂μ)
theorem
ContinuousLinearEquiv.integral_comp_comm
{X : Type u_1}
{E : Type u_3}
{F : Type u_4}
[MeasurableSpace X]
{μ : MeasureTheory.Measure X}
{𝕜 : Type u_5}
[RCLike 𝕜]
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
[NormedSpace ℝ F]
[NormedSpace ℝ E]
(L : E ≃L[𝕜] F)
(φ : X → E)
:
∫ (x : X), L (φ x) ∂μ = L (∫ (x : X), φ x ∂μ)
theorem
ContinuousMap.integral_apply
{X : Type u_1}
{Y : Type u_2}
{E : Type u_3}
[MeasurableSpace X]
{μ : MeasureTheory.Measure X}
[NormedAddCommGroup E]
[TopologicalSpace Y]
[CompactSpace Y]
[NormedSpace ℝ E]
[CompleteSpace E]
{f : X → C(Y, E)}
(hf : MeasureTheory.Integrable f μ)
(y : Y)
:
(∫ (x : X), f x ∂μ) y = ∫ (x : X), (f x) y ∂μ
theorem
ContinuousMapZero.integral_apply
{X : Type u_1}
{Y : Type u_2}
[MeasurableSpace X]
{μ : MeasureTheory.Measure X}
[TopologicalSpace Y]
[CompactSpace Y]
{R : Type u_6}
[NormedCommRing R]
[Zero Y]
[NormedAlgebra ℝ R]
[CompleteSpace R]
{f : X → ContinuousMapZero Y R}
(hf : MeasureTheory.Integrable f μ)
(y : Y)
:
(∫ (x : X), f x ∂μ) y = ∫ (x : X), (f x) y ∂μ
theorem
integral_ofReal
{X : Type u_1}
[MeasurableSpace X]
{μ : MeasureTheory.Measure X}
{𝕜 : Type u_5}
[RCLike 𝕜]
{f : X → ℝ}
:
∫ (x : X), ↑(f x) ∂μ = ↑(∫ (x : X), f x ∂μ)
theorem
integral_re
{X : Type u_1}
[MeasurableSpace X]
{μ : MeasureTheory.Measure X}
{𝕜 : Type u_5}
[RCLike 𝕜]
{f : X → 𝕜}
(hf : MeasureTheory.Integrable f μ)
:
∫ (x : X), RCLike.re (f x) ∂μ = RCLike.re (∫ (x : X), f x ∂μ)
theorem
integral_im
{X : Type u_1}
[MeasurableSpace X]
{μ : MeasureTheory.Measure X}
{𝕜 : Type u_5}
[RCLike 𝕜]
{f : X → 𝕜}
(hf : MeasureTheory.Integrable f μ)
:
∫ (x : X), RCLike.im (f x) ∂μ = RCLike.im (∫ (x : X), f x ∂μ)
theorem
integral_conj
{X : Type u_1}
[MeasurableSpace X]
{μ : MeasureTheory.Measure X}
{𝕜 : Type u_5}
[RCLike 𝕜]
{f : X → 𝕜}
:
∫ (x : X), (starRingEnd 𝕜) (f x) ∂μ = (starRingEnd 𝕜) (∫ (x : X), f x ∂μ)
theorem
integral_coe_re_add_coe_im
{X : Type u_1}
[MeasurableSpace X]
{μ : MeasureTheory.Measure X}
{𝕜 : Type u_5}
[RCLike 𝕜]
{f : X → 𝕜}
(hf : MeasureTheory.Integrable f μ)
:
theorem
integral_re_add_im
{X : Type u_1}
[MeasurableSpace X]
{μ : MeasureTheory.Measure X}
{𝕜 : Type u_5}
[RCLike 𝕜]
{f : X → 𝕜}
(hf : MeasureTheory.Integrable f μ)
:
theorem
setIntegral_re_add_im
{X : Type u_1}
[MeasurableSpace X]
{μ : MeasureTheory.Measure X}
{𝕜 : Type u_5}
[RCLike 𝕜]
{f : X → 𝕜}
{i : Set X}
(hf : MeasureTheory.IntegrableOn f i μ)
:
@[deprecated setIntegral_re_add_im]
theorem
set_integral_re_add_im
{X : Type u_1}
[MeasurableSpace X]
{μ : MeasureTheory.Measure X}
{𝕜 : Type u_5}
[RCLike 𝕜]
{f : X → 𝕜}
{i : Set X}
(hf : MeasureTheory.IntegrableOn f i μ)
:
Alias of setIntegral_re_add_im.
theorem
swap_integral
{X : Type u_1}
{E : Type u_3}
{F : Type u_4}
[MeasurableSpace X]
{μ : MeasureTheory.Measure X}
[NormedAddCommGroup E]
[NormedAddCommGroup F]
[NormedSpace ℝ E]
[NormedSpace ℝ F]
(f : X → E × F)
:
(∫ (x : X), f x ∂μ).swap = ∫ (x : X), (f x).swap ∂μ
theorem
fst_integral
{X : Type u_1}
{E : Type u_3}
{F : Type u_4}
[MeasurableSpace X]
{μ : MeasureTheory.Measure X}
[NormedAddCommGroup E]
[NormedAddCommGroup F]
[NormedSpace ℝ E]
[NormedSpace ℝ F]
[CompleteSpace F]
{f : X → E × F}
(hf : MeasureTheory.Integrable f μ)
:
(∫ (x : X), f x ∂μ).1 = ∫ (x : X), (f x).1 ∂μ
theorem
snd_integral
{X : Type u_1}
{E : Type u_3}
{F : Type u_4}
[MeasurableSpace X]
{μ : MeasureTheory.Measure X}
[NormedAddCommGroup E]
[NormedAddCommGroup F]
[NormedSpace ℝ E]
[NormedSpace ℝ F]
[CompleteSpace E]
{f : X → E × F}
(hf : MeasureTheory.Integrable f μ)
:
(∫ (x : X), f x ∂μ).2 = ∫ (x : X), (f x).2 ∂μ
theorem
integral_pair
{X : Type u_1}
{E : Type u_3}
{F : Type u_4}
[MeasurableSpace X]
{μ : MeasureTheory.Measure X}
[NormedAddCommGroup E]
[NormedAddCommGroup F]
[NormedSpace ℝ E]
[NormedSpace ℝ F]
[CompleteSpace E]
[CompleteSpace F]
{f : X → E}
{g : X → F}
(hf : MeasureTheory.Integrable f μ)
(hg : MeasureTheory.Integrable g μ)
:
∫ (x : X), (f x, g x) ∂μ = (∫ (x : X), f x ∂μ, ∫ (x : X), g x ∂μ)
theorem
integral_smul_const
{X : Type u_1}
{E : Type u_3}
[MeasurableSpace X]
{μ : MeasureTheory.Measure X}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{𝕜 : Type u_6}
[RCLike 𝕜]
[NormedSpace 𝕜 E]
[CompleteSpace E]
(f : X → 𝕜)
(c : E)
:
theorem
integral_withDensity_eq_integral_smul
{X : Type u_1}
{E : Type u_3}
[MeasurableSpace X]
{μ : MeasureTheory.Measure X}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{f : X → NNReal}
(f_meas : Measurable f)
(g : X → E)
:
theorem
integral_withDensity_eq_integral_smul₀
{X : Type u_1}
{E : Type u_3}
[MeasurableSpace X]
{μ : MeasureTheory.Measure X}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{f : X → NNReal}
(hf : AEMeasurable f μ)
(g : X → E)
:
theorem
setIntegral_withDensity_eq_setIntegral_smul
{X : Type u_1}
{E : Type u_3}
[MeasurableSpace X]
{μ : MeasureTheory.Measure X}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{f : X → NNReal}
(f_meas : Measurable f)
(g : X → E)
{s : Set X}
(hs : MeasurableSet s)
:
@[deprecated setIntegral_withDensity_eq_setIntegral_smul]
theorem
set_integral_withDensity_eq_set_integral_smul
{X : Type u_1}
{E : Type u_3}
[MeasurableSpace X]
{μ : MeasureTheory.Measure X}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{f : X → NNReal}
(f_meas : Measurable f)
(g : X → E)
{s : Set X}
(hs : MeasurableSet s)
:
theorem
setIntegral_withDensity_eq_setIntegral_smul₀
{X : Type u_1}
{E : Type u_3}
[MeasurableSpace X]
{μ : MeasureTheory.Measure X}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{f : X → NNReal}
{s : Set X}
(hf : AEMeasurable f (μ.restrict s))
(g : X → E)
(hs : MeasurableSet s)
:
@[deprecated setIntegral_withDensity_eq_setIntegral_smul₀]
theorem
set_integral_withDensity_eq_set_integral_smul₀
{X : Type u_1}
{E : Type u_3}
[MeasurableSpace X]
{μ : MeasureTheory.Measure X}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{f : X → NNReal}
{s : Set X}
(hf : AEMeasurable f (μ.restrict s))
(g : X → E)
(hs : MeasurableSet s)
:
theorem
setIntegral_withDensity_eq_setIntegral_smul₀'
{X : Type u_1}
{E : Type u_3}
[MeasurableSpace X]
{μ : MeasureTheory.Measure X}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[MeasureTheory.SFinite μ]
{f : X → NNReal}
(s : Set X)
(hf : AEMeasurable f (μ.restrict s))
(g : X → E)
:
@[deprecated setIntegral_withDensity_eq_setIntegral_smul₀']
theorem
set_integral_withDensity_eq_set_integral_smul₀'
{X : Type u_1}
{E : Type u_3}
[MeasurableSpace X]
{μ : MeasureTheory.Measure X}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[MeasureTheory.SFinite μ]
{f : X → NNReal}
(s : Set X)
(hf : AEMeasurable f (μ.restrict s))
(g : X → E)
:
theorem
measure_le_lintegral_thickenedIndicatorAux
{X : Type u_1}
[MeasurableSpace X]
[PseudoEMetricSpace X]
(μ : MeasureTheory.Measure X)
{E : Set X}
(E_mble : MeasurableSet E)
(δ : ℝ)
:
μ E ≤ ∫⁻ (x : X), thickenedIndicatorAux δ E x ∂μ
theorem
measure_le_lintegral_thickenedIndicator
{X : Type u_1}
[MeasurableSpace X]
[PseudoEMetricSpace X]
(μ : MeasureTheory.Measure X)
{E : Set X}
(E_mble : MeasurableSet E)
{δ : ℝ}
(δ_pos : 0 < δ)
:
μ E ≤ ∫⁻ (x : X), ↑((thickenedIndicator δ_pos E) x) ∂μ
theorem
MeasureTheory.Integrable.simpleFunc_mul
{X : Type u_6}
{f : X → ℝ}
{m0 : MeasurableSpace X}
{μ : MeasureTheory.Measure X}
(g : MeasureTheory.SimpleFunc X ℝ)
(hf : MeasureTheory.Integrable f μ)
:
MeasureTheory.Integrable (⇑g * f) μ
theorem
MeasureTheory.Integrable.simpleFunc_mul'
{X : Type u_6}
{f : X → ℝ}
{m : MeasurableSpace X}
{m0 : MeasurableSpace X}
{μ : MeasureTheory.Measure X}
(hm : m ≤ m0)
(g : MeasureTheory.SimpleFunc X ℝ)
(hf : MeasureTheory.Integrable f μ)
:
MeasureTheory.Integrable (⇑g * f) μ
theorem
continuous_parametric_integral_of_continuous
{Y : Type u_2}
{E : Type u_3}
{X : Type u_5}
[TopologicalSpace X]
[TopologicalSpace Y]
[MeasurableSpace Y]
[OpensMeasurableSpace Y]
{μ : MeasureTheory.Measure Y}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[FirstCountableTopology X]
[LocallyCompactSpace X]
[SecondCountableTopologyEither Y E]
[MeasureTheory.IsLocallyFiniteMeasure μ]
{f : X → Y → E}
(hf : Continuous (Function.uncurry f))
{s : Set Y}
(hs : IsCompact s)
:
Continuous fun (x : X) => ∫ (y : Y) in s, f x y ∂μ
The parametric integral over a continuous function on a compact set is continuous, under mild assumptions on the topologies involved.
theorem
continuousOn_integral_bilinear_of_locally_integrable_of_compact_support
{Y : Type u_2}
{E : Type u_3}
{F : Type u_4}
{X : Type u_5}
{G : Type u_6}
{𝕜 : Type u_7}
[TopologicalSpace X]
[TopologicalSpace Y]
[MeasurableSpace Y]
[OpensMeasurableSpace Y]
{μ : MeasureTheory.Measure Y}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
[NormedSpace 𝕜 E]
(L : F →L[𝕜] G →L[𝕜] E)
{f : X → Y → G}
{s : Set X}
{k : Set Y}
{g : Y → F}
(hk : IsCompact k)
(hf : ContinuousOn (Function.uncurry f) (s ×ˢ Set.univ))
(hfs : ∀ (p : X) (x : Y), p ∈ s → x ∉ k → f p x = 0)
(hg : MeasureTheory.IntegrableOn g k μ)
:
ContinuousOn (fun (x : X) => ∫ (y : Y), (L (g y)) (f x y) ∂μ) s
Consider a parameterized integral x ↦ ∫ y, L (g y) (f x y) where L is bilinear,
g is locally integrable and f is continuous and uniformly compactly supported. Then the
integral depends continuously on x.
theorem
continuousOn_integral_of_compact_support
{Y : Type u_2}
{E : Type u_3}
{X : Type u_5}
[TopologicalSpace X]
[TopologicalSpace Y]
[MeasurableSpace Y]
[OpensMeasurableSpace Y]
{μ : MeasureTheory.Measure Y}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{f : X → Y → E}
{s : Set X}
{k : Set Y}
[MeasureTheory.IsFiniteMeasureOnCompacts μ]
(hk : IsCompact k)
(hf : ContinuousOn (Function.uncurry f) (s ×ˢ Set.univ))
(hfs : ∀ (p : X) (x : Y), p ∈ s → x ∉ k → f p x = 0)
:
ContinuousOn (fun (x : X) => ∫ (y : Y), f x y ∂μ) s
Consider a parameterized integral x ↦ ∫ y, f x y where f is continuous and uniformly
compactly supported. Then the integral depends continuously on x.