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.
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/Basic.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}
{mX : MeasurableSpace X}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{f g : X → E}
{s : Set X}
{μ : Measure X}
(hs : NullMeasurableSet s μ)
(h : ∀ᵐ (x : X) ∂μ, x ∈ s → f x = g x)
:
theorem
MeasureTheory.setIntegral_congr_ae
{X : Type u_1}
{E : Type u_3}
{mX : MeasurableSpace X}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{f g : X → E}
{s : Set X}
{μ : Measure X}
(hs : MeasurableSet s)
(h : ∀ᵐ (x : X) ∂μ, x ∈ s → f x = g x)
:
theorem
MeasureTheory.setIntegral_congr_fun₀
{X : Type u_1}
{E : Type u_3}
{mX : MeasurableSpace X}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{f g : X → E}
{s : Set X}
{μ : Measure X}
(hs : NullMeasurableSet s μ)
(h : Set.EqOn f g s)
:
theorem
MeasureTheory.setIntegral_congr_fun
{X : Type u_1}
{E : Type u_3}
{mX : MeasurableSpace X}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{f g : X → E}
{s : Set X}
{μ : Measure X}
(hs : MeasurableSet s)
(h : Set.EqOn f g s)
:
theorem
MeasureTheory.integral_union_ae
{X : Type u_1}
{E : Type u_3}
{mX : MeasurableSpace X}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{f : X → E}
{s t : Set X}
{μ : Measure X}
(hst : AEDisjoint μ s t)
(ht : NullMeasurableSet t μ)
(hfs : IntegrableOn f s μ)
(hft : IntegrableOn f t μ)
:
theorem
MeasureTheory.setIntegral_union
{X : Type u_1}
{E : Type u_3}
{mX : MeasurableSpace X}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{f : X → E}
{s t : Set X}
{μ : Measure X}
(hst : Disjoint s t)
(ht : MeasurableSet t)
(hfs : IntegrableOn f s μ)
(hft : IntegrableOn f t μ)
:
theorem
MeasureTheory.integral_diff
{X : Type u_1}
{E : Type u_3}
{mX : MeasurableSpace X}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{f : X → E}
{s t : Set X}
{μ : Measure X}
(ht : MeasurableSet t)
(hfs : IntegrableOn f s μ)
(hts : t ⊆ s)
:
theorem
MeasureTheory.integral_inter_add_diff₀
{X : Type u_1}
{E : Type u_3}
{mX : MeasurableSpace X}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{f : X → E}
{s t : Set X}
{μ : Measure X}
(ht : NullMeasurableSet t μ)
(hfs : IntegrableOn f s μ)
:
theorem
MeasureTheory.integral_inter_add_diff
{X : Type u_1}
{E : Type u_3}
{mX : MeasurableSpace X}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{f : X → E}
{s t : Set X}
{μ : Measure X}
(ht : MeasurableSet t)
(hfs : IntegrableOn f s μ)
:
theorem
MeasureTheory.integral_biUnion_finset
{X : Type u_1}
{E : Type u_3}
{mX : MeasurableSpace X}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{f : X → E}
{μ : Measure X}
{ι : Type u_5}
(t : Finset ι)
{s : ι → Set X}
(hs : ∀ i ∈ t, MeasurableSet (s i))
(h's : (↑t).Pairwise (Function.onFun Disjoint s))
(hf : ∀ i ∈ t, IntegrableOn f (s i) μ)
:
@[deprecated MeasureTheory.integral_biUnion_finset (since := "2025-08-28")]
theorem
MeasureTheory.integral_finset_biUnion
{X : Type u_1}
{E : Type u_3}
{mX : MeasurableSpace X}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{f : X → E}
{μ : Measure X}
{ι : Type u_5}
(t : Finset ι)
{s : ι → Set X}
(hs : ∀ i ∈ t, MeasurableSet (s i))
(h's : (↑t).Pairwise (Function.onFun Disjoint s))
(hf : ∀ i ∈ t, IntegrableOn f (s i) μ)
:
Alias of MeasureTheory.integral_biUnion_finset.
theorem
MeasureTheory.integral_iUnion_fintype
{X : Type u_1}
{E : Type u_3}
{mX : MeasurableSpace X}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{f : X → E}
{μ : Measure X}
{ι : Type u_5}
[Fintype ι]
{s : ι → Set X}
(hs : ∀ (i : ι), MeasurableSet (s i))
(h's : Pairwise (Function.onFun Disjoint s))
(hf : ∀ (i : ι), IntegrableOn f (s i) μ)
:
@[deprecated MeasureTheory.integral_iUnion_fintype (since := "2025-08-28")]
theorem
MeasureTheory.integral_fintype_iUnion
{X : Type u_1}
{E : Type u_3}
{mX : MeasurableSpace X}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{f : X → E}
{μ : Measure X}
{ι : Type u_5}
[Fintype ι]
{s : ι → Set X}
(hs : ∀ (i : ι), MeasurableSet (s i))
(h's : Pairwise (Function.onFun Disjoint s))
(hf : ∀ (i : ι), IntegrableOn f (s i) μ)
:
Alias of MeasureTheory.integral_iUnion_fintype.
theorem
MeasureTheory.setIntegral_empty
{X : Type u_1}
{E : Type u_3}
{mX : MeasurableSpace X}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{f : X → E}
{μ : Measure X}
:
theorem
MeasureTheory.setIntegral_univ
{X : Type u_1}
{E : Type u_3}
{mX : MeasurableSpace X}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{f : X → E}
{μ : Measure X}
:
theorem
MeasureTheory.integral_add_compl₀
{X : Type u_1}
{E : Type u_3}
{mX : MeasurableSpace X}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{f : X → E}
{s : Set X}
{μ : Measure X}
(hs : NullMeasurableSet s μ)
(hfi : Integrable f μ)
:
theorem
MeasureTheory.integral_add_compl
{X : Type u_1}
{E : Type u_3}
{mX : MeasurableSpace X}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{f : X → E}
{s : Set X}
{μ : Measure X}
(hs : MeasurableSet s)
(hfi : Integrable f μ)
:
theorem
MeasureTheory.setIntegral_compl
{X : Type u_1}
{E : Type u_3}
{mX : MeasurableSpace X}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{f : X → E}
{s : Set X}
{μ : Measure X}
(hs : MeasurableSet s)
(hfi : Integrable f μ)
:
theorem
MeasureTheory.integral_indicator
{X : Type u_1}
{E : Type u_3}
{mX : MeasurableSpace X}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{f : X → E}
{s : Set X}
{μ : Measure X}
(hs : MeasurableSet 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
MeasureTheory.integral_integral_indicator
{X : Type u_1}
{Y : Type u_2}
{E : Type u_3}
{mX : MeasurableSpace X}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{μ : Measure X}
{mY : MeasurableSpace Y}
{ν : Measure Y}
(f : X → Y → E)
{s : Set X}
(hs : MeasurableSet s)
:
theorem
MeasureTheory.setIntegral_indicator
{X : Type u_1}
{E : Type u_3}
{mX : MeasurableSpace X}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{f : X → E}
{s t : Set X}
{μ : Measure X}
(ht : MeasurableSet t)
:
theorem
MeasureTheory.integral_biUnion_eq_sum_powerset
{X : Type u_1}
{E : Type u_3}
{mX : MeasurableSpace X}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{f : X → E}
{μ : Measure X}
{ι : Type u_5}
{t : Finset ι}
{s : ι → Set X}
(hs : ∀ i ∈ t, MeasurableSet (s i))
(hf : ∀ i ∈ t, IntegrableOn f (s i) μ)
:
Inclusion-exclusion principle for the integral of a function over a union.
The integral of a function f over the union of the s i over i ∈ t is the alternating sum of
the integrals of f over the intersections of the s i.
theorem
MeasureTheory.ofReal_setIntegral_one_of_measure_ne_top
{X : Type u_5}
{m : MeasurableSpace X}
{μ : Measure X}
{s : Set X}
(hs : μ s ≠ ⊤ := by finiteness)
:
theorem
MeasureTheory.ofReal_setIntegral_one
{X : Type u_5}
{x✝ : MeasurableSpace X}
(μ : Measure X)
[IsFiniteMeasure μ]
(s : Set X)
:
theorem
MeasureTheory.measureReal_biUnion_eq_sum_powerset
{X : Type u_1}
{mX : MeasurableSpace X}
{μ : Measure X}
{ι : Type u_5}
{t : Finset ι}
{s : ι → Set X}
(hs : ∀ i ∈ t, MeasurableSet (s i))
(hf : ∀ i ∈ t, μ (s i) ≠ ⊤ := by finiteness)
:
Inclusion-exclusion principle for the measure of a union of sets of finite measure.
The measure of the union of the s i over i ∈ t is the alternating sum of the measures of the
intersections of the s i.
theorem
MeasureTheory.integral_piecewise
{X : Type u_1}
{E : Type u_3}
{mX : MeasurableSpace X}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{f g : X → E}
{s : Set X}
{μ : Measure X}
[DecidablePred fun (x : X) => x ∈ s]
(hs : MeasurableSet s)
(hf : IntegrableOn f s μ)
(hg : IntegrableOn g sᶜ μ)
:
theorem
MeasureTheory.tendsto_setIntegral_of_monotone
{X : Type u_1}
{E : Type u_3}
{mX : MeasurableSpace X}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{f : X → E}
{μ : Measure X}
{ι : Type u_5}
[Preorder ι]
[Filter.atTop.IsCountablyGenerated]
{s : ι → Set X}
(hsm : ∀ (i : ι), MeasurableSet (s i))
(h_mono : Monotone s)
(hfi : IntegrableOn f (⋃ (n : ι), s n) μ)
:
theorem
MeasureTheory.tendsto_setIntegral_of_antitone
{X : Type u_1}
{E : Type u_3}
{mX : MeasurableSpace X}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{f : X → E}
{μ : Measure X}
{ι : Type u_5}
[Preorder ι]
[Filter.atTop.IsCountablyGenerated]
{s : ι → Set X}
(hsm : ∀ (i : ι), MeasurableSet (s i))
(h_anti : Antitone s)
(hfi : ∃ (i : ι), IntegrableOn f (s i) μ)
:
theorem
MeasureTheory.hasSum_integral_iUnion_ae
{X : Type u_1}
{E : Type u_3}
{mX : MeasurableSpace X}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{f : X → E}
{μ : Measure X}
{ι : Type u_5}
[Countable ι]
{s : ι → Set X}
(hm : ∀ (i : ι), NullMeasurableSet (s i) μ)
(hd : Pairwise (Function.onFun (AEDisjoint μ) s))
(hfi : IntegrableOn f (⋃ (i : ι), s i) μ)
:
theorem
MeasureTheory.hasSum_integral_iUnion
{X : Type u_1}
{E : Type u_3}
{mX : MeasurableSpace X}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{f : X → E}
{μ : Measure X}
{ι : Type u_5}
[Countable ι]
{s : ι → Set X}
(hm : ∀ (i : ι), MeasurableSet (s i))
(hd : Pairwise (Function.onFun Disjoint s))
(hfi : IntegrableOn f (⋃ (i : ι), s i) μ)
:
theorem
MeasureTheory.integral_iUnion
{X : Type u_1}
{E : Type u_3}
{mX : MeasurableSpace X}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{f : X → E}
{μ : Measure X}
{ι : Type u_5}
[Countable ι]
{s : ι → Set X}
(hm : ∀ (i : ι), MeasurableSet (s i))
(hd : Pairwise (Function.onFun Disjoint s))
(hfi : IntegrableOn f (⋃ (i : ι), s i) μ)
:
theorem
MeasureTheory.integral_iUnion_ae
{X : Type u_1}
{E : Type u_3}
{mX : MeasurableSpace X}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{f : X → E}
{μ : Measure X}
{ι : Type u_5}
[Countable ι]
{s : ι → Set X}
(hm : ∀ (i : ι), NullMeasurableSet (s i) μ)
(hd : Pairwise (Function.onFun (AEDisjoint μ) s))
(hfi : IntegrableOn f (⋃ (i : ι), s i) μ)
:
theorem
MeasureTheory.setIntegral_eq_zero_of_ae_eq_zero
{X : Type u_1}
{E : Type u_3}
{mX : MeasurableSpace X}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{f : X → E}
{t : Set X}
{μ : Measure X}
(ht_eq : ∀ᵐ (x : X) ∂μ, x ∈ t → f x = 0)
:
theorem
MeasureTheory.setIntegral_eq_zero_of_forall_eq_zero
{X : Type u_1}
{E : Type u_3}
{mX : MeasurableSpace X}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{f : X → E}
{t : Set X}
{μ : Measure X}
(ht_eq : ∀ x ∈ t, f x = 0)
:
theorem
MeasureTheory.integral_union_eq_left_of_ae_aux
{X : Type u_1}
{E : Type u_3}
{mX : MeasurableSpace X}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{f : X → E}
{s t : Set X}
{μ : Measure X}
(ht_eq : ∀ᵐ (x : X) ∂μ.restrict t, f x = 0)
(haux : StronglyMeasurable f)
(H : IntegrableOn f (s ∪ t) μ)
:
theorem
MeasureTheory.integral_union_eq_left_of_forall₀
{X : Type u_1}
{E : Type u_3}
{mX : MeasurableSpace X}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{s t : Set X}
{μ : Measure X}
{f : X → E}
(ht : 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}
{mX : MeasurableSpace X}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{s t : Set X}
{μ : 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}
{mX : MeasurableSpace X}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{f : X → E}
{s t : Set X}
{μ : Measure X}
(hts : s ⊆ t)
(h't : ∀ᵐ (x : X) ∂μ, x ∈ t \ s → f x = 0)
(haux : StronglyMeasurable f)
(h'aux : IntegrableOn f t μ)
:
theorem
MeasureTheory.setIntegral_eq_of_subset_of_ae_diff_eq_zero
{X : Type u_1}
{E : Type u_3}
{mX : MeasurableSpace X}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{f : X → E}
{s t : Set X}
{μ : Measure X}
(ht : NullMeasurableSet t μ)
(hts : s ⊆ t)
(h't : ∀ᵐ (x : X) ∂μ, x ∈ t \ s → f x = 0)
:
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}
{mX : MeasurableSpace X}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{f : X → E}
{s t : Set X}
{μ : Measure X}
(ht : MeasurableSet t)
(hts : s ⊆ t)
(h't : ∀ x ∈ t \ s, f x = 0)
:
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}
{mX : MeasurableSpace X}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{f : X → E}
{s : Set X}
{μ : Measure X}
(h : ∀ᵐ (x : X) ∂μ, x ∉ s → f x = 0)
:
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}
{mX : MeasurableSpace X}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{f : X → E}
{s : Set X}
{μ : Measure X}
(h : ∀ x ∉ s, f x = 0)
:
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}
{mX : MeasurableSpace X}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{μ : Measure X}
[PartialOrder E]
{f : X → E}
(hf : AEStronglyMeasurable f μ)
:
theorem
MeasureTheory.setIntegral_const
{X : Type u_1}
{E : Type u_3}
{mX : MeasurableSpace X}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{s : Set X}
{μ : Measure X}
[CompleteSpace E]
(c : E)
:
@[simp]
theorem
MeasureTheory.integral_indicator_const
{X : Type u_1}
{E : Type u_3}
{mX : MeasurableSpace X}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{μ : Measure X}
[CompleteSpace E]
(e : E)
⦃s : Set X⦄
(s_meas : MeasurableSet s)
:
@[simp]
theorem
MeasureTheory.integral_indicator_one
{X : Type u_1}
{mX : MeasurableSpace X}
{μ : Measure X}
⦃s : Set X⦄
(hs : MeasurableSet s)
:
theorem
MeasureTheory.setIntegral_indicatorConstLp
{X : Type u_1}
{E : Type u_3}
{mX : MeasurableSpace X}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{s t : Set X}
{μ : Measure X}
[CompleteSpace E]
{p : ENNReal}
(hs : MeasurableSet s)
(ht : MeasurableSet t)
(hμt : μ t ≠ ⊤)
(e : E)
:
theorem
MeasureTheory.integral_indicatorConstLp
{X : Type u_1}
{E : Type u_3}
{mX : MeasurableSpace X}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{t : Set X}
{μ : Measure X}
[CompleteSpace E]
{p : ENNReal}
(ht : MeasurableSet t)
(hμt : μ t ≠ ⊤)
(e : E)
:
theorem
MeasureTheory.setIntegral_map
{X : Type u_1}
{E : Type u_3}
{mX : MeasurableSpace X}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{μ : Measure X}
{Y : Type u_5}
[MeasurableSpace Y]
{g : X → Y}
{f : Y → E}
{s : Set Y}
(hs : MeasurableSet s)
(hf : AEStronglyMeasurable f (Measure.map g μ))
(hg : AEMeasurable g μ)
:
theorem
MeasurableEmbedding.setIntegral_map
{X : Type u_1}
{E : Type u_3}
{mX : MeasurableSpace X}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{μ : MeasureTheory.Measure X}
{Y : Type u_5}
{x✝ : MeasurableSpace Y}
{f : X → Y}
(hf : MeasurableEmbedding f)
(g : Y → E)
(s : Set Y)
:
theorem
Topology.IsClosedEmbedding.setIntegral_map
{X : Type u_1}
{E : Type u_3}
{mX : 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)
:
theorem
MeasureTheory.MeasurePreserving.setIntegral_preimage_emb
{X : Type u_1}
{E : Type u_3}
{mX : MeasurableSpace X}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{μ : Measure X}
{Y : Type u_5}
{x✝ : MeasurableSpace Y}
{f : X → Y}
{ν : Measure Y}
(h₁ : MeasurePreserving f μ ν)
(h₂ : MeasurableEmbedding f)
(g : Y → E)
(s : Set Y)
:
theorem
MeasureTheory.MeasurePreserving.setIntegral_image_emb
{X : Type u_1}
{E : Type u_3}
{mX : MeasurableSpace X}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{μ : Measure X}
{Y : Type u_5}
{x✝ : MeasurableSpace Y}
{f : X → Y}
{ν : Measure Y}
(h₁ : MeasurePreserving f μ ν)
(h₂ : MeasurableEmbedding f)
(g : Y → E)
(s : Set X)
:
theorem
MeasureTheory.setIntegral_map_equiv
{X : Type u_1}
{E : Type u_3}
{mX : MeasurableSpace X}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{μ : Measure X}
{Y : Type u_5}
[MeasurableSpace Y]
(e : X ≃ᵐ Y)
(f : Y → E)
(s : Set Y)
:
theorem
MeasureTheory.norm_setIntegral_le_of_norm_le_const_ae
{X : Type u_1}
{E : Type u_3}
{mX : MeasurableSpace X}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{f : X → E}
{s : Set X}
{μ : Measure X}
{C : ℝ}
(hs : μ s < ⊤)
(hC : ∀ᵐ (x : X) ∂μ.restrict s, ‖f x‖ ≤ C)
:
theorem
MeasureTheory.norm_setIntegral_le_of_norm_le_const_ae'
{X : Type u_1}
{E : Type u_3}
{mX : MeasurableSpace X}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{f : X → E}
{s : Set X}
{μ : Measure X}
{C : ℝ}
(hs : μ s < ⊤)
(hC : ∀ᵐ (x : X) ∂μ, x ∈ s → ‖f x‖ ≤ C)
:
@[deprecated MeasureTheory.norm_setIntegral_le_of_norm_le_const_ae' (since := "2025-04-17")]
theorem
MeasureTheory.norm_setIntegral_le_of_norm_le_const_ae''
{X : Type u_1}
{E : Type u_3}
{mX : MeasurableSpace X}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{f : X → E}
{s : Set X}
{μ : Measure X}
{C : ℝ}
(hs : μ s < ⊤)
(hC : ∀ᵐ (x : X) ∂μ, x ∈ s → ‖f x‖ ≤ C)
:
Alias of MeasureTheory.norm_setIntegral_le_of_norm_le_const_ae'.
@[deprecated MeasureTheory.norm_setIntegral_le_of_norm_le_const (since := "2025-04-17")]
theorem
MeasureTheory.norm_setIntegral_le_of_norm_le_const'
{X : Type u_1}
{E : Type u_3}
{mX : MeasurableSpace X}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{f : X → E}
{s : Set X}
{μ : Measure X}
{C : ℝ}
(hs : μ s < ⊤)
(hC : ∀ x ∈ s, ‖f x‖ ≤ C)
:
Alias of MeasureTheory.norm_setIntegral_le_of_norm_le_const.
theorem
MeasureTheory.norm_integral_sub_setIntegral_le
{X : Type u_1}
{E : Type u_3}
{mX : MeasurableSpace X}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{f : X → E}
{μ : Measure X}
[IsFiniteMeasure μ]
{C : ℝ}
(hf : ∀ᵐ (x : X) ∂μ, ‖f x‖ ≤ C)
{s : Set X}
(hs : MeasurableSet s)
(hf1 : Integrable f μ)
:
theorem
MeasureTheory.setIntegral_trim
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{X : Type u_5}
{m m0 : MeasurableSpace X}
{μ : Measure X}
(hm : m ≤ m0)
{f : X → E}
(hf_meas : StronglyMeasurable f)
{s : Set X}
(hs : MeasurableSet s)
:
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}
{mX : MeasurableSpace X}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{f : X → E}
{μ : Measure X}
[PartialOrder X]
{x y : X}
(hx : μ {x} = 0)
:
theorem
MeasureTheory.integral_Icc_eq_integral_Ico'
{X : Type u_1}
{E : Type u_3}
{mX : MeasurableSpace X}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{f : X → E}
{μ : Measure X}
[PartialOrder X]
{x y : X}
(hy : μ {y} = 0)
:
theorem
MeasureTheory.integral_Ioc_eq_integral_Ioo'
{X : Type u_1}
{E : Type u_3}
{mX : MeasurableSpace X}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{f : X → E}
{μ : Measure X}
[PartialOrder X]
{x y : X}
(hy : μ {y} = 0)
:
theorem
MeasureTheory.integral_Ico_eq_integral_Ioo'
{X : Type u_1}
{E : Type u_3}
{mX : MeasurableSpace X}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{f : X → E}
{μ : Measure X}
[PartialOrder X]
{x y : X}
(hx : μ {x} = 0)
:
theorem
MeasureTheory.integral_Icc_eq_integral_Ioo'
{X : Type u_1}
{E : Type u_3}
{mX : MeasurableSpace X}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{f : X → E}
{μ : Measure X}
[PartialOrder 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}
{mX : MeasurableSpace X}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{f : X → E}
{μ : Measure X}
[PartialOrder X]
{x : X}
(hx : μ {x} = 0)
:
theorem
MeasureTheory.integral_Ici_eq_integral_Ioi'
{X : Type u_1}
{E : Type u_3}
{mX : MeasurableSpace X}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{f : X → E}
{μ : Measure X}
[PartialOrder X]
{x : X}
(hx : μ {x} = 0)
:
theorem
MeasureTheory.integral_Icc_eq_integral_Ioc
{X : Type u_1}
{E : Type u_3}
{mX : MeasurableSpace X}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{f : X → E}
{μ : Measure X}
[PartialOrder X]
{x y : X}
[NoAtoms μ]
:
theorem
MeasureTheory.integral_Icc_eq_integral_Ico
{X : Type u_1}
{E : Type u_3}
{mX : MeasurableSpace X}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{f : X → E}
{μ : Measure X}
[PartialOrder X]
{x y : X}
[NoAtoms μ]
:
theorem
MeasureTheory.integral_Ioc_eq_integral_Ioo
{X : Type u_1}
{E : Type u_3}
{mX : MeasurableSpace X}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{f : X → E}
{μ : Measure X}
[PartialOrder X]
{x y : X}
[NoAtoms μ]
:
theorem
MeasureTheory.integral_Ico_eq_integral_Ioo
{X : Type u_1}
{E : Type u_3}
{mX : MeasurableSpace X}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{f : X → E}
{μ : Measure X}
[PartialOrder X]
{x y : X}
[NoAtoms μ]
:
theorem
MeasureTheory.integral_Icc_eq_integral_Ioo
{X : Type u_1}
{E : Type u_3}
{mX : MeasurableSpace X}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{f : X → E}
{μ : Measure X}
[PartialOrder X]
{x y : X}
[NoAtoms μ]
:
theorem
MeasureTheory.integral_Iic_eq_integral_Iio
{X : Type u_1}
{E : Type u_3}
{mX : MeasurableSpace X}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{f : X → E}
{μ : Measure X}
[PartialOrder X]
{x : X}
[NoAtoms μ]
:
theorem
MeasureTheory.integral_Ici_eq_integral_Ioi
{X : Type u_1}
{E : Type u_3}
{mX : MeasurableSpace X}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{f : X → E}
{μ : Measure X}
[PartialOrder X]
{x : X}
[NoAtoms μ]
:
theorem
MeasureTheory.setIntegral_mono_on
{X : Type u_1}
{mX : MeasurableSpace X}
{μ : Measure X}
{f g : X → ℝ}
{s : Set X}
(hf : IntegrableOn f s μ)
(hg : IntegrableOn g s μ)
(hs : MeasurableSet s)
(h : ∀ x ∈ s, f x ≤ g x)
:
theorem
MeasureTheory.setIntegral_mono_on_ae
{X : Type u_1}
{mX : MeasurableSpace X}
{μ : Measure X}
{f g : X → ℝ}
{s : Set X}
(hf : IntegrableOn f s μ)
(hg : IntegrableOn g s μ)
(hs : MeasurableSet s)
(h : ∀ᵐ (x : X) ∂μ, x ∈ s → f x ≤ g x)
:
theorem
MeasureTheory.setIntegral_mono_on_ae₀
{X : Type u_1}
{mX : MeasurableSpace X}
{μ : Measure X}
{f g : X → ℝ}
{s : Set X}
(hf : IntegrableOn f s μ)
(hg : IntegrableOn g s μ)
(hs : NullMeasurableSet s μ)
(h : ∀ᵐ (x : X) ∂μ, x ∈ s → f x ≤ g x)
:
theorem
MeasureTheory.setIntegral_mono_on₀
{X : Type u_1}
{mX : MeasurableSpace X}
{μ : Measure X}
{f g : X → ℝ}
{s : Set X}
(hf : IntegrableOn f s μ)
(hg : IntegrableOn g s μ)
(hs : NullMeasurableSet s μ)
(h : ∀ x ∈ s, f x ≤ g x)
:
theorem
MeasureTheory.setIntegral_mono
{X : Type u_1}
{mX : MeasurableSpace X}
{μ : Measure X}
{f g : X → ℝ}
{s : Set X}
(hf : IntegrableOn f s μ)
(hg : IntegrableOn g s μ)
(h : f ≤ g)
:
theorem
MeasureTheory.setIntegral_ge_of_const_le
{X : Type u_1}
{mX : MeasurableSpace X}
{μ : Measure X}
{f : X → ℝ}
{s : Set X}
{c : ℝ}
(hs : MeasurableSet s)
(hμs : μ s ≠ ⊤)
(hf : ∀ x ∈ s, c ≤ f x)
(hfint : IntegrableOn (fun (x : X) => f x) s μ)
:
theorem
MeasureTheory.setIntegral_nonneg
{X : Type u_1}
{mX : MeasurableSpace X}
{μ : Measure X}
{f : X → ℝ}
{s : Set X}
(hs : MeasurableSet s)
(hf : ∀ x ∈ s, 0 ≤ f x)
:
theorem
MeasureTheory.setIntegral_le_nonneg
{X : Type u_1}
{mX : MeasurableSpace X}
{μ : Measure X}
{f : X → ℝ}
{s : Set X}
(hs : MeasurableSet s)
(hf : StronglyMeasurable f)
(hfi : Integrable f μ)
:
theorem
MeasureTheory.setIntegral_nonpos
{X : Type u_1}
{mX : MeasurableSpace X}
{μ : Measure X}
{f : X → ℝ}
{s : Set X}
(hs : MeasurableSet s)
(hf : ∀ x ∈ s, f x ≤ 0)
:
theorem
MeasureTheory.setIntegral_nonpos_le
{X : Type u_1}
{mX : MeasurableSpace X}
{μ : Measure X}
{f : X → ℝ}
{s : Set X}
(hs : MeasurableSet s)
(hf : StronglyMeasurable f)
(hfi : Integrable f μ)
:
theorem
MeasureTheory.Integrable.measure_le_integral
{X : Type u_1}
{mX : MeasurableSpace X}
{μ : Measure X}
{f : X → ℝ}
(f_int : Integrable f μ)
(f_nonneg : 0 ≤ᶠ[ae μ] f)
{s : Set X}
(hs : ∀ x ∈ s, 1 ≤ f x)
:
theorem
MeasureTheory.integral_le_measure
{X : Type u_1}
{mX : MeasurableSpace X}
{μ : Measure X}
{f : X → ℝ}
{s : Set X}
(hs : ∀ x ∈ s, f x ≤ 1)
(h's : ∀ x ∈ sᶜ, f x ≤ 0)
:
theorem
MeasureTheory.integrableOn_iUnion_of_summable_integral_norm
{X : Type u_1}
{E : Type u_3}
{mX : MeasurableSpace X}
{ι : Type u_5}
[Countable ι]
{μ : Measure X}
[NormedAddCommGroup E]
{f : X → E}
{s : ι → Set X}
(hi : ∀ (i : ι), IntegrableOn f (s i) μ)
(h : Summable fun (i : ι) => ∫ (x : X) in s i, ‖f x‖ ∂μ)
:
IntegrableOn f (Set.iUnion s) μ
theorem
MeasureTheory.integrableOn_iUnion_of_summable_norm_restrict
{X : Type u_1}
{E : Type u_3}
{mX : MeasurableSpace X}
{ι : Type u_5}
[Countable ι]
{μ : Measure X}
[NormedAddCommGroup E]
[TopologicalSpace X]
[BorelSpace X]
[T2Space X]
[IsLocallyFiniteMeasure μ]
{f : C(X, E)}
{s : ι → TopologicalSpace.Compacts X}
(hf : Summable fun (i : ι) => ‖ContinuousMap.restrict (↑(s i)) f‖ * μ.real ↑(s i))
:
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}
{mX : MeasurableSpace X}
{ι : Type u_5}
[Countable ι]
{μ : Measure X}
[NormedAddCommGroup E]
[TopologicalSpace X]
[BorelSpace X]
[T2Space X]
[IsLocallyFiniteMeasure μ]
{f : C(X, E)}
{s : ι → TopologicalSpace.Compacts X}
(hf : Summable fun (i : ι) => ‖ContinuousMap.restrict (↑(s i)) f‖ * μ.real ↑(s i))
(hs : ⋃ (i : ι), ↑(s i) = Set.univ)
:
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}
{mX : MeasurableSpace X}
[NormedAddCommGroup E]
{p : ENNReal}
{μ : Measure X}
(f g : ↥(Lp E p μ))
(s : Set X)
:
For f : Lp E p μ, we can define an element of Lp E p (μ.restrict s) by
(Lp.memLp f).restrict s).toLp f. This map is additive.
theorem
MeasureTheory.Lp_toLp_restrict_smul
{X : Type u_1}
{F : Type u_4}
{mX : MeasurableSpace X}
{𝕜 : Type u_5}
[NormedRing 𝕜]
[NormedAddCommGroup F]
[Module 𝕜 F]
[IsBoundedSMul 𝕜 F]
{p : ENNReal}
{μ : Measure X}
(c : 𝕜)
(f : ↥(Lp F p μ))
(s : Set X)
:
For f : Lp E p μ, we can define an element of Lp E p (μ.restrict s) by
(Lp.memLp 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}
{mX : MeasurableSpace X}
[NormedAddCommGroup E]
{p : ENNReal}
{μ : Measure X}
(s : Set X)
(f : ↥(Lp E p μ))
:
For f : Lp E p μ, we can define an element of Lp E p (μ.restrict s) by
(Lp.memLp f).restrict s).toLp f. This map is non-expansive.
noncomputable def
MeasureTheory.LpToLpRestrictCLM
(X : Type u_1)
(F : Type u_4)
{mX : MeasurableSpace X}
(𝕜 : Type u_5)
[NormedRing 𝕜]
[NormedAddCommGroup F]
[Module 𝕜 F]
[IsBoundedSMul 𝕜 F]
(μ : Measure X)
(p : ENNReal)
[hp : Fact (1 ≤ p)]
(s : Set X)
:
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.MemLp.toLp ↑↑f ⋯, map_add' := ⋯, map_smul' := ⋯ }.mkContinuous 1 ⋯
Instances For
theorem
MeasureTheory.LpToLpRestrictCLM_coeFn
{X : Type u_1}
{F : Type u_4}
{mX : MeasurableSpace X}
(𝕜 : Type u_5)
[NormedRing 𝕜]
[NormedAddCommGroup F]
[Module 𝕜 F]
[IsBoundedSMul 𝕜 F]
{p : ENNReal}
{μ : Measure X}
[Fact (1 ≤ p)]
(s : Set X)
(f : ↥(Lp F p μ))
:
theorem
MeasureTheory.continuous_setIntegral
{X : Type u_1}
{E : Type u_3}
{mX : MeasurableSpace X}
[NormedAddCommGroup E]
{μ : Measure X}
[NormedSpace ℝ E]
(s : Set X)
:
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)
:
theorem
MeasureTheory.setIntegral_support
{X : Type u_1}
{M : Type u_5}
[NormedAddCommGroup M]
[NormedSpace ℝ M]
{mX : MeasurableSpace X}
{ν : Measure X}
{F : X → M}
:
theorem
MeasureTheory.setIntegral_tsupport
{X : Type u_1}
{M : Type u_5}
[NormedAddCommGroup M]
[NormedSpace ℝ M]
{mX : MeasurableSpace X}
{ν : Measure X}
{F : X → M}
[TopologicalSpace X]
:
theorem
measure_le_lintegral_thickenedIndicatorAux
{X : Type u_1}
[MeasurableSpace X]
[PseudoEMetricSpace X]
(μ : MeasureTheory.Measure X)
{E : Set X}
(E_mble : MeasurableSet E)
(δ : ℝ)
:
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 < δ)
:
theorem
MeasureTheory.Integrable.simpleFunc_mul
{X : Type u_6}
{f : X → ℝ}
{m0 : MeasurableSpace X}
{μ : Measure X}
(g : SimpleFunc X ℝ)
(hf : Integrable f μ)
:
Integrable (⇑g * f) μ
theorem
MeasureTheory.Integrable.simpleFunc_mul'
{X : Type u_6}
{f : X → ℝ}
{m m0 : MeasurableSpace X}
{μ : Measure X}
(hm : m ≤ m0)
(g : SimpleFunc X ℝ)
(hf : Integrable f μ)
:
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.