Documentation

Mathlib.MeasureTheory.VectorMeasure.SetIntegral

Set integral #

In this file we prove properties of ∫ᵛ x in s, f x ∂[B; μ]. Recall that this notation is defined as ∫ᵛ x, f x ∂[B; μ.restrict s].

The API in this file is modelled on the API for the Bochner integral.

source
theorem MeasureTheory.VectorMeasure.IntegrableOn.mono {X : Type u_2} {E : Type u_3} {F : Type u_4} {mX : MeasurableSpace X} [NormedAddCommGroup E] [NormedAddCommGroup F] {μ : VectorMeasure X F} {f : X → E} {s t : Set X} (hs : MeasurableSet s) (hts : t ⊆ s) (h : μ.IntegrableOn f s) :
μ.IntegrableOn f t
source
theorem MeasureTheory.VectorMeasure.IntegrableOn.union {X : Type u_2} {E : Type u_3} {F : Type u_4} {mX : MeasurableSpace X} [NormedAddCommGroup E] [NormedAddCommGroup F] {μ : VectorMeasure X F} {f : X → E} {s t : Set X} (hs : MeasurableSet s) (ht : MeasurableSet t) (hf : μ.IntegrableOn f s) (h'f : μ.IntegrableOn f t) :
μ.IntegrableOn f (s ∪ t)
source
@[simp]
theorem MeasureTheory.VectorMeasure.IntegrableOn.empty {X : Type u_2} {E : Type u_3} {F : Type u_4} {mX : MeasurableSpace X} [NormedAddCommGroup E] [NormedAddCommGroup F] {μ : VectorMeasure X F} {f : X → E} :
μ.IntegrableOn f ∅
source
theorem MeasureTheory.VectorMeasure.IntegrableOn.biUnion_finite {ι : Type u_1} {X : Type u_2} {E : Type u_3} {F : Type u_4} {mX : MeasurableSpace X} [NormedAddCommGroup E] [NormedAddCommGroup F] {μ : VectorMeasure X F} {f : X → E} {s : Set ι} (hs : s.Finite) {t : ι → Set X} (ht : ∀ i ∈ s, MeasurableSet (t i)) (h't : ∀ i ∈ s, μ.IntegrableOn f (t i)) :
μ.IntegrableOn f (⋃ i ∈ s, t i)
source
theorem MeasureTheory.VectorMeasure.IntegrableOn.biUnion_finset {ι : Type u_1} {X : Type u_2} {E : Type u_3} {F : Type u_4} {mX : MeasurableSpace X} [NormedAddCommGroup E] [NormedAddCommGroup F] {μ : VectorMeasure X F} {f : X → E} {s : Finset ι} {t : ι → Set X} (ht : ∀ i ∈ s, MeasurableSet (t i)) (h't : ∀ i ∈ s, μ.IntegrableOn f (t i)) :
μ.IntegrableOn f (⋃ i ∈ s, t i)
source
theorem MeasureTheory.VectorMeasure.IntegrableOn.iUnion_finite {ι : Type u_1} {X : Type u_2} {E : Type u_3} {F : Type u_4} {mX : MeasurableSpace X} [NormedAddCommGroup E] [NormedAddCommGroup F] {μ : VectorMeasure X F} {f : X → E} [Finite ι] {t : ι → Set X} (ht : ∀ (i : ι), MeasurableSet (t i)) (h't : ∀ (i : ι), μ.IntegrableOn f (t i)) :
μ.IntegrableOn f (⋃ (i : ι), t i)
source
@[simp]
theorem MeasureTheory.VectorMeasure.integrableOn_univ {X : Type u_2} {E : Type u_3} {F : Type u_4} {mX : MeasurableSpace X} [NormedAddCommGroup E] [NormedAddCommGroup F] {μ : VectorMeasure X F} {f : X → E} :
μ.IntegrableOn f Set.univ ↔ μ.Integrable f
source
theorem MeasureTheory.VectorMeasure.Integrable.integrableOn {X : Type u_2} {E : Type u_3} {F : Type u_4} {mX : MeasurableSpace X} [NormedAddCommGroup E] [NormedAddCommGroup F] {μ : VectorMeasure X F} {f : X → E} {s : Set X} (h : μ.Integrable f) :
μ.IntegrableOn f s
source
theorem MeasureTheory.VectorMeasure.integrable_indicator_iff {X : Type u_2} {E : Type u_3} {F : Type u_4} {mX : MeasurableSpace X} [NormedAddCommGroup E] [NormedAddCommGroup F] {μ : VectorMeasure X F} {f : X → E} {s : Set X} (hs : MeasurableSet s) :
μ.Integrable (s.indicator f) ↔ μ.IntegrableOn f s
source
theorem MeasureTheory.VectorMeasure.IntegrableOn.integrable_indicator {X : Type u_2} {E : Type u_3} {F : Type u_4} {mX : MeasurableSpace X} [NormedAddCommGroup E] [NormedAddCommGroup F] {μ : VectorMeasure X F} {f : X → E} {s : Set X} (h : μ.IntegrableOn f s) (hs : MeasurableSet s) :
μ.Integrable (s.indicator f)
source
theorem MeasureTheory.VectorMeasure.setIntegral_eq_zero_of_not_measurableSet {X : Type u_2} {E : Type u_3} {F : Type u_4} {G : Type u_5} {mX : MeasurableSpace X} [NormedAddCommGroup E] [NormedAddCommGroup F] [NormedAddCommGroup G] {μ : VectorMeasure X F} {f : X → E} {s : Set X} [NormedSpace ℝ E] [NormedSpace ℝ F] [NormedSpace ℝ G] {B : E →L[ℝ] F →L[ℝ] G} (hs : ¬MeasurableSet s) :
∫ᵛ (x : X) in s, f x ∂[B; μ] = 0
source
theorem MeasureTheory.VectorMeasure.setIntegral_congr_ae {X : Type u_2} {E : Type u_3} {F : Type u_4} {G : Type u_5} {mX : MeasurableSpace X} [NormedAddCommGroup E] [NormedAddCommGroup F] [NormedAddCommGroup G] {μ : VectorMeasure X F} {f g : X → E} {s : Set X} [NormedSpace ℝ E] [NormedSpace ℝ F] [NormedSpace ℝ G] {B : E →L[ℝ] F →L[ℝ] G} (h : ∀ᵐ (x : X) ∂μ.variation, x ∈ s → f x = g x) :
∫ᵛ (x : X) in s, f x ∂[B; μ] = ∫ᵛ (x : X) in s, g x ∂[B; μ]
source
theorem MeasureTheory.VectorMeasure.setIntegral_congr_fun {X : Type u_2} {E : Type u_3} {F : Type u_4} {G : Type u_5} {mX : MeasurableSpace X} [NormedAddCommGroup E] [NormedAddCommGroup F] [NormedAddCommGroup G] {μ : VectorMeasure X F} {f g : X → E} {s : Set X} [NormedSpace ℝ E] [NormedSpace ℝ F] [NormedSpace ℝ G] {B : E →L[ℝ] F →L[ℝ] G} (h : Set.EqOn f g s) :
∫ᵛ (x : X) in s, f x ∂[B; μ] = ∫ᵛ (x : X) in s, g x ∂[B; μ]
source
theorem MeasureTheory.VectorMeasure.setIntegral_union {X : Type u_2} {E : Type u_3} {F : Type u_4} {G : Type u_5} {mX : MeasurableSpace X} [NormedAddCommGroup E] [NormedAddCommGroup F] [NormedAddCommGroup G] {μ : VectorMeasure X F} {f : X → E} {s t : Set X} [NormedSpace ℝ E] [NormedSpace ℝ F] [NormedSpace ℝ G] {B : E →L[ℝ] F →L[ℝ] G} (hst : Disjoint s t) (hs : MeasurableSet s) (ht : MeasurableSet t) (hfs : μ.IntegrableOn f s) (hft : μ.IntegrableOn f t) :
∫ᵛ (x : X) in s ∪ t, f x ∂[B; μ] = ∫ᵛ (x : X) in s, f x ∂[B; μ] + ∫ᵛ (x : X) in t, f x ∂[B; μ]
source
theorem MeasureTheory.VectorMeasure.setIntegral_sdiff {X : Type u_2} {E : Type u_3} {F : Type u_4} {G : Type u_5} {mX : MeasurableSpace X} [NormedAddCommGroup E] [NormedAddCommGroup F] [NormedAddCommGroup G] {μ : VectorMeasure X F} {f : X → E} {s t : Set X} [NormedSpace ℝ E] [NormedSpace ℝ F] [NormedSpace ℝ G] {B : E →L[ℝ] F →L[ℝ] G} (hs : MeasurableSet s) (ht : MeasurableSet t) (hfs : μ.IntegrableOn f s) (hts : t ⊆ s) :
∫ᵛ (x : X) in s \ t, f x ∂[B; μ] = ∫ᵛ (x : X) in s, f x ∂[B; μ] - ∫ᵛ (x : X) in t, f x ∂[B; μ]
source
theorem MeasureTheory.VectorMeasure.setIntegral_inter_add_sdiff {X : Type u_2} {E : Type u_3} {F : Type u_4} {G : Type u_5} {mX : MeasurableSpace X} [NormedAddCommGroup E] [NormedAddCommGroup F] [NormedAddCommGroup G] {μ : VectorMeasure X F} {f : X → E} {s t : Set X} [NormedSpace ℝ E] [NormedSpace ℝ F] [NormedSpace ℝ G] {B : E →L[ℝ] F →L[ℝ] G} (hs : MeasurableSet s) (ht : MeasurableSet t) (hfs : μ.IntegrableOn f s) :
∫ᵛ (x : X) in s ∩ t, f x ∂[B; μ] + ∫ᵛ (x : X) in s \ t, f x ∂[B; μ] = ∫ᵛ (x : X) in s, f x ∂[B; μ]
source
theorem MeasureTheory.VectorMeasure.setIntegral_biUnion_finset {X : Type u_2} {E : Type u_3} {F : Type u_4} {G : Type u_5} {mX : MeasurableSpace X} [NormedAddCommGroup E] [NormedAddCommGroup F] [NormedAddCommGroup G] {μ : VectorMeasure X F} {f : X → E} [NormedSpace ℝ E] [NormedSpace ℝ F] [NormedSpace ℝ G] {B : E →L[ℝ] F →L[ℝ] G} {ι : Type u_7} (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)) :
∫ᵛ (x : X) in ⋃ i ∈ t, s i, f x ∂[B; μ] = ∑ i ∈ t, ∫ᵛ (x : X) in s i, f x ∂[B; μ]
source
theorem MeasureTheory.VectorMeasure.setIntegral_iUnion_fintype {X : Type u_2} {E : Type u_3} {F : Type u_4} {G : Type u_5} {mX : MeasurableSpace X} [NormedAddCommGroup E] [NormedAddCommGroup F] [NormedAddCommGroup G] {μ : VectorMeasure X F} {f : X → E} [NormedSpace ℝ E] [NormedSpace ℝ F] [NormedSpace ℝ G] {B : E →L[ℝ] F →L[ℝ] G} {ι : Type u_7} [Fintype ι] {s : ι → Set X} (hs : ∀ (i : ι), MeasurableSet (s i)) (h's : Pairwise (Function.onFun Disjoint s)) (hf : ∀ (i : ι), μ.IntegrableOn f (s i)) :
∫ᵛ (x : X) in ⋃ (i : ι), s i, f x ∂[B; μ] = ∑ i : ι, ∫ᵛ (x : X) in s i, f x ∂[B; μ]
source
theorem MeasureTheory.VectorMeasure.setIntegral_empty {X : Type u_2} {E : Type u_3} {F : Type u_4} {G : Type u_5} {mX : MeasurableSpace X} [NormedAddCommGroup E] [NormedAddCommGroup F] [NormedAddCommGroup G] {μ : VectorMeasure X F} {f : X → E} [NormedSpace ℝ E] [NormedSpace ℝ F] [NormedSpace ℝ G] {B : E →L[ℝ] F →L[ℝ] G} :
∫ᵛ (x : X) in ∅, f x ∂[B; μ] = 0
source
theorem MeasureTheory.VectorMeasure.setIntegral_univ {X : Type u_2} {E : Type u_3} {F : Type u_4} {G : Type u_5} {mX : MeasurableSpace X} [NormedAddCommGroup E] [NormedAddCommGroup F] [NormedAddCommGroup G] {μ : VectorMeasure X F} {f : X → E} [NormedSpace ℝ E] [NormedSpace ℝ F] [NormedSpace ℝ G] {B : E →L[ℝ] F →L[ℝ] G} :
∫ᵛ (x : X) in Set.univ, f x ∂[B; μ] = ∫ᵛ (x : X), f x ∂[B; μ]
source
theorem MeasureTheory.VectorMeasure.setIntegral_add_compl {X : Type u_2} {E : Type u_3} {F : Type u_4} {G : Type u_5} {mX : MeasurableSpace X} [NormedAddCommGroup E] [NormedAddCommGroup F] [NormedAddCommGroup G] {μ : VectorMeasure X F} {f : X → E} {s : Set X} [NormedSpace ℝ E] [NormedSpace ℝ F] [NormedSpace ℝ G] {B : E →L[ℝ] F →L[ℝ] G} (hs : MeasurableSet s) (hfi : μ.Integrable f) :
∫ᵛ (x : X) in s, f x ∂[B; μ] + ∫ᵛ (x : X) in sᶜ, f x ∂[B; μ] = ∫ᵛ (x : X), f x ∂[B; μ]
source
theorem MeasureTheory.VectorMeasure.setIntegral_compl {X : Type u_2} {E : Type u_3} {F : Type u_4} {G : Type u_5} {mX : MeasurableSpace X} [NormedAddCommGroup E] [NormedAddCommGroup F] [NormedAddCommGroup G] {μ : VectorMeasure X F} {f : X → E} {s : Set X} [NormedSpace ℝ E] [NormedSpace ℝ F] [NormedSpace ℝ G] {B : E →L[ℝ] F →L[ℝ] G} (hs : MeasurableSet s) (hfi : μ.Integrable f) :
∫ᵛ (x : X) in sᶜ, f x ∂[B; μ] = ∫ᵛ (x : X), f x ∂[B; μ] - ∫ᵛ (x : X) in s, f x ∂[B; μ]
source
theorem MeasureTheory.VectorMeasure.integral_indicator {X : Type u_2} {E : Type u_3} {F : Type u_4} {G : Type u_5} {mX : MeasurableSpace X} [NormedAddCommGroup E] [NormedAddCommGroup F] [NormedAddCommGroup G] {μ : VectorMeasure X F} {f : X → E} {s : Set X} [NormedSpace ℝ E] [NormedSpace ℝ F] [NormedSpace ℝ G] {B : E →L[ℝ] F →L[ℝ] G} (hs : MeasurableSet s) :
∫ᵛ (x : X), s.indicator f x ∂[B; μ] = ∫ᵛ (x : X) in s, f x ∂[B; μ]

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 ∂[B; μ] defined as ∫ᵛ x, f x ∂[B; μ.restrict s].

source
theorem MeasureTheory.VectorMeasure.setIntegral_indicator {X : Type u_2} {E : Type u_3} {F : Type u_4} {G : Type u_5} {mX : MeasurableSpace X} [NormedAddCommGroup E] [NormedAddCommGroup F] [NormedAddCommGroup G] {μ : VectorMeasure X F} {f : X → E} {s t : Set X} [NormedSpace ℝ E] [NormedSpace ℝ F] [NormedSpace ℝ G] {B : E →L[ℝ] F →L[ℝ] G} (hs : MeasurableSet s) (ht : MeasurableSet t) :
∫ᵛ (x : X) in s, t.indicator f x ∂[B; μ] = ∫ᵛ (x : X) in s ∩ t, f x ∂[B; μ]
source
theorem MeasureTheory.VectorMeasure.setIntegral_congr_set {X : Type u_2} {E : Type u_3} {F : Type u_4} {G : Type u_5} {mX : MeasurableSpace X} [NormedAddCommGroup E] [NormedAddCommGroup F] [NormedAddCommGroup G] {μ : VectorMeasure X F} {f : X → E} {s t : Set X} [NormedSpace ℝ E] [NormedSpace ℝ F] [NormedSpace ℝ G] {B : E →L[ℝ] F →L[ℝ] G} (hs : MeasurableSet s) (ht : MeasurableSet t) (hst : s =ᵐ[μ.variation] t) :
∫ᵛ (x : X) in s, f x ∂[B; μ] = ∫ᵛ (x : X) in t, f x ∂[B; μ]
source
theorem MeasureTheory.VectorMeasure.integral_piecewise {X : Type u_2} {E : Type u_3} {F : Type u_4} {G : Type u_5} {mX : MeasurableSpace X} [NormedAddCommGroup E] [NormedAddCommGroup F] [NormedAddCommGroup G] {μ : VectorMeasure X F} {f g : X → E} {s : Set X} [NormedSpace ℝ E] [NormedSpace ℝ F] [NormedSpace ℝ G] {B : E →L[ℝ] F →L[ℝ] G} [DecidablePred fun (x : X) => x ∈ s] (hs : MeasurableSet s) (hf : μ.IntegrableOn f s) (hg : μ.IntegrableOn g sᶜ) :
∫ᵛ (x : X), s.piecewise f g x ∂[B; μ] = ∫ᵛ (x : X) in s, f x ∂[B; μ] + ∫ᵛ (x : X) in sᶜ, g x ∂[B; μ]
source
theorem MeasureTheory.VectorMeasure.setIntegral_eq_zero_of_ae_eq_zero {X : Type u_2} {E : Type u_3} {F : Type u_4} {G : Type u_5} {mX : MeasurableSpace X} [NormedAddCommGroup E] [NormedAddCommGroup F] [NormedAddCommGroup G] {μ : VectorMeasure X F} {f : X → E} {t : Set X} [NormedSpace ℝ E] [NormedSpace ℝ F] [NormedSpace ℝ G] {B : E →L[ℝ] F →L[ℝ] G} (ht_eq : ∀ᵐ (x : X) ∂μ.variation, x ∈ t → f x = 0) :
∫ᵛ (x : X) in t, f x ∂[B; μ] = 0
source
theorem MeasureTheory.VectorMeasure.setIntegral_eq_zero_of_forall_eq_zero {X : Type u_2} {E : Type u_3} {F : Type u_4} {G : Type u_5} {mX : MeasurableSpace X} [NormedAddCommGroup E] [NormedAddCommGroup F] [NormedAddCommGroup G] {μ : VectorMeasure X F} {f : X → E} {t : Set X} [NormedSpace ℝ E] [NormedSpace ℝ F] [NormedSpace ℝ G] {B : E →L[ℝ] F →L[ℝ] G} (ht_eq : ∀ x ∈ t, f x = 0) :
∫ᵛ (x : X) in t, f x ∂[B; μ] = 0
source
theorem MeasureTheory.VectorMeasure.frequently_ae_ne_zero_of_setIntegral_ne_zero {X : Type u_2} {E : Type u_3} {F : Type u_4} {G : Type u_5} {mX : MeasurableSpace X} [NormedAddCommGroup E] [NormedAddCommGroup F] [NormedAddCommGroup G] {μ : VectorMeasure X F} {f : X → E} {t : Set X} [NormedSpace ℝ E] [NormedSpace ℝ F] [NormedSpace ℝ G] {B : E →L[ℝ] F →L[ℝ] G} (hU : ∫ᵛ (x : X) in t, f x ∂[B; μ] ≠ 0) :
∃ᵐ (x : X) ∂μ.variation.restrict t, f x ≠ 0
source
theorem MeasureTheory.VectorMeasure.exists_ne_zero_of_setIntegral_ne_zero {X : Type u_2} {E : Type u_3} {F : Type u_4} {G : Type u_5} {mX : MeasurableSpace X} [NormedAddCommGroup E] [NormedAddCommGroup F] [NormedAddCommGroup G] {μ : VectorMeasure X F} {f : X → E} {t : Set X} [NormedSpace ℝ E] [NormedSpace ℝ F] [NormedSpace ℝ G] {B : E →L[ℝ] F →L[ℝ] G} (hU : ∫ᵛ (x : X) in t, f x ∂[B; μ] ≠ 0) :
∃ x ∈ t, f x ≠ 0
source
theorem MeasureTheory.VectorMeasure.setIntegral_of_variation_apply_eq_zero {X : Type u_2} {E : Type u_3} {F : Type u_4} {G : Type u_5} {mX : MeasurableSpace X} [NormedAddCommGroup E] [NormedAddCommGroup F] [NormedAddCommGroup G] {μ : VectorMeasure X F} [NormedSpace ℝ E] [NormedSpace ℝ F] [NormedSpace ℝ G] {B : E →L[ℝ] F →L[ℝ] G} (f : X → E) {s : Set X} (hs : μ.variation s = 0) :
∫ᵛ (x : X) in s, f x ∂[B; μ] = 0
source
theorem MeasureTheory.VectorMeasure.setIntegral_dirac' {X : Type u_2} {E : Type u_3} {F : Type u_4} {G : Type u_5} [NormedAddCommGroup E] [NormedAddCommGroup F] [NormedAddCommGroup G] {f : X → E} [NormedSpace ℝ E] [NormedSpace ℝ F] [NormedSpace ℝ G] {B : E →L[ℝ] F →L[ℝ] G} {mX : MeasurableSpace X} [CompleteSpace G] {a : X} {v : F} (hf : StronglyMeasurable f) {s : Set X} (hs : MeasurableSet s) [Decidable (a ∈ s)] :
∫ᵛ (x : X) in s, f x ∂[B; dirac a v] = if a ∈ s then (B (f a)) v else 0
source
theorem MeasureTheory.VectorMeasure.setIntegral_dirac {X : Type u_2} {E : Type u_3} {F : Type u_4} {G : Type u_5} [NormedAddCommGroup E] [NormedAddCommGroup F] [NormedAddCommGroup G] {f : X → E} [NormedSpace ℝ E] [NormedSpace ℝ F] [NormedSpace ℝ G] {B : E →L[ℝ] F →L[ℝ] G} [MeasurableSpace X] [MeasurableSingletonClass X] [CompleteSpace G] {a : X} {v : F} {s : Set X} (hs : MeasurableSet s) [Decidable (a ∈ s)] :
∫ᵛ (x : X) in s, f x ∂[B; dirac a v] = if a ∈ s then (B (f a)) v else 0
source
theorem MeasureTheory.VectorMeasure.integral_singleton' {X : Type u_2} {E : Type u_3} {F : Type u_4} {G : Type u_5} {mX : MeasurableSpace X} [NormedAddCommGroup E] [NormedAddCommGroup F] [NormedAddCommGroup G] {μ : VectorMeasure X F} {f : X → E} [NormedSpace ℝ E] [NormedSpace ℝ F] [NormedSpace ℝ G] {B : E →L[ℝ] F →L[ℝ] G} [CompleteSpace G] {a : X} (hf : StronglyMeasurable f) :
∫ᵛ (a : X) in {a}, f a ∂[B; μ] = (B (f a)) (μ {a})
source
theorem MeasureTheory.VectorMeasure.integral_singleton {X : Type u_2} {E : Type u_3} {F : Type u_4} {G : Type u_5} {mX : MeasurableSpace X} [NormedAddCommGroup E] [NormedAddCommGroup F] [NormedAddCommGroup G] {μ : VectorMeasure X F} {f : X → E} [NormedSpace ℝ E] [NormedSpace ℝ F] [NormedSpace ℝ G] {B : E →L[ℝ] F →L[ℝ] G} [MeasurableSingletonClass X] {a : X} [CompleteSpace G] :
∫ᵛ (a : X) in {a}, f a ∂[B; μ] = (B (f a)) (μ {a})
source
theorem MeasureTheory.VectorMeasure.setIntegral_union_eq_left_of_ae {X : Type u_2} {E : Type u_3} {F : Type u_4} {G : Type u_5} {mX : MeasurableSpace X} [NormedAddCommGroup E] [NormedAddCommGroup F] [NormedAddCommGroup G] {μ : VectorMeasure X F} {f : X → E} {s t : Set X} [NormedSpace ℝ E] [NormedSpace ℝ F] [NormedSpace ℝ G] {B : E →L[ℝ] F →L[ℝ] G} (hs : MeasurableSet s) (ht : MeasurableSet t) (ht_eq : ∀ᵐ (x : X) ∂μ.variation.restrict t, f x = 0) :
∫ᵛ (x : X) in s ∪ t, f x ∂[B; μ] = ∫ᵛ (x : X) in s, f x ∂[B; μ]
source
theorem MeasureTheory.VectorMeasure.setIntegral_union_eq_left_of_forall {X : Type u_2} {E : Type u_3} {F : Type u_4} {G : Type u_5} {mX : MeasurableSpace X} [NormedAddCommGroup E] [NormedAddCommGroup F] [NormedAddCommGroup G] {μ : VectorMeasure X F} {f : X → E} {s t : Set X} [NormedSpace ℝ E] [NormedSpace ℝ F] [NormedSpace ℝ G] {B : E →L[ℝ] F →L[ℝ] G} (hs : MeasurableSet s) (ht : MeasurableSet t) (ht_eq : ∀ x ∈ t, f x = 0) :
∫ᵛ (x : X) in s ∪ t, f x ∂[B; μ] = ∫ᵛ (x : X) in s, f x ∂[B; μ]
source
theorem MeasureTheory.VectorMeasure.setIntegral_eq_of_subset_of_ae_sdiff_eq_zero {X : Type u_2} {E : Type u_3} {F : Type u_4} {G : Type u_5} {mX : MeasurableSpace X} [NormedAddCommGroup E] [NormedAddCommGroup F] [NormedAddCommGroup G] {μ : VectorMeasure X F} {f : X → E} {s t : Set X} [NormedSpace ℝ E] [NormedSpace ℝ F] [NormedSpace ℝ G] {B : E →L[ℝ] F →L[ℝ] G} (hs : MeasurableSet s) (ht : MeasurableSet t) (hts : s ⊆ t) (h't : ∀ᵐ (x : X) ∂μ.variation.restrict (t \ s), f x = 0) :
∫ᵛ (x : X) in t, f x ∂[B; μ] = ∫ᵛ (x : X) in s, f x ∂[B; μ]
source
theorem MeasureTheory.VectorMeasure.setIntegral_eq_of_subset_of_forall_sdiff_eq_zero {X : Type u_2} {E : Type u_3} {F : Type u_4} {G : Type u_5} {mX : MeasurableSpace X} [NormedAddCommGroup E] [NormedAddCommGroup F] [NormedAddCommGroup G] {μ : VectorMeasure X F} {f : X → E} {s t : Set X} [NormedSpace ℝ E] [NormedSpace ℝ F] [NormedSpace ℝ G] {B : E →L[ℝ] F →L[ℝ] G} (hs : MeasurableSet s) (ht : MeasurableSet t) (hts : s ⊆ t) (h't : ∀ x ∈ t \ s, f x = 0) :
∫ᵛ (x : X) in t, f x ∂[B; μ] = ∫ᵛ (x : X) in s, f x ∂[B; μ]

If a function vanishes on t \ s with s ⊆ t, then its integrals on s and t coincide.

source
theorem MeasureTheory.VectorMeasure.setIntegral_eq_integral_of_ae_compl_eq_zero {X : Type u_2} {E : Type u_3} {F : Type u_4} {G : Type u_5} {mX : MeasurableSpace X} [NormedAddCommGroup E] [NormedAddCommGroup F] [NormedAddCommGroup G] {μ : VectorMeasure X F} {f : X → E} {s : Set X} [NormedSpace ℝ E] [NormedSpace ℝ F] [NormedSpace ℝ G] {B : E →L[ℝ] F →L[ℝ] G} (hs : MeasurableSet s) (h : ∀ᵐ (x : X) ∂μ.variation, x ∉ s → f x = 0) :
∫ᵛ (x : X) in s, f x ∂[B; μ] = ∫ᵛ (x : X), f x ∂[B; μ]

If a function vanishes almost everywhere on sᶜ, then its integral on s coincides with its integral on the whole space.

source
theorem MeasureTheory.VectorMeasure.setIntegral_eq_integral_of_forall_compl_eq_zero {X : Type u_2} {E : Type u_3} {F : Type u_4} {G : Type u_5} {mX : MeasurableSpace X} [NormedAddCommGroup E] [NormedAddCommGroup F] [NormedAddCommGroup G] {μ : VectorMeasure X F} {f : X → E} {s : Set X} [NormedSpace ℝ E] [NormedSpace ℝ F] [NormedSpace ℝ G] {B : E →L[ℝ] F →L[ℝ] G} (hs : MeasurableSet s) (h : ∀ x ∉ s, f x = 0) :
∫ᵛ (x : X) in s, f x ∂[B; μ] = ∫ᵛ (x : X), f x ∂[B; μ]

If a function vanishes on sᶜ, then its integral on s coincides with its integral on the whole space.

source
theorem MeasureTheory.VectorMeasure.setIntegral_const {X : Type u_2} {E : Type u_3} {F : Type u_4} {G : Type u_5} {mX : MeasurableSpace X} [NormedAddCommGroup E] [NormedAddCommGroup F] [NormedAddCommGroup G] {μ : VectorMeasure X F} {s : Set X} [NormedSpace ℝ E] [NormedSpace ℝ F] [NormedSpace ℝ G] {B : E →L[ℝ] F →L[ℝ] G} [CompleteSpace G] [IsFiniteMeasure (μ.variation.restrict s)] (c : E) :
∫ᵛ (x : X) in s, c ∂[B; μ] = (B c) (μ s)
source
@[simp]
theorem MeasureTheory.VectorMeasure.integral_indicator_const {X : Type u_2} {E : Type u_3} {F : Type u_4} {G : Type u_5} {mX : MeasurableSpace X} [NormedAddCommGroup E] [NormedAddCommGroup F] [NormedAddCommGroup G] {μ : VectorMeasure X F} [NormedSpace ℝ E] [NormedSpace ℝ F] [NormedSpace ℝ G] {B : E →L[ℝ] F →L[ℝ] G} [CompleteSpace G] (e : E) ⦃s : Set X⦄ [IsFiniteMeasure (μ.variation.restrict s)] (s_meas : MeasurableSet s) :
∫ᵛ (x : X), s.indicator (fun (x : X) => e) x ∂[B; μ] = (B e) (μ s)
source
theorem MeasureTheory.VectorMeasure.setIntegral_map {X : Type u_2} {E : Type u_3} {F : Type u_4} {G : Type u_5} {mX : MeasurableSpace X} [NormedAddCommGroup E] [NormedAddCommGroup F] [NormedAddCommGroup G] {μ : VectorMeasure X F} [NormedSpace ℝ E] [NormedSpace ℝ F] [NormedSpace ℝ G] {B : E →L[ℝ] F →L[ℝ] G} {β : Type u_7} [MeasurableSpace β] {φ : X → β} (hφ : Measurable φ) {f : β → E} {s : Set β} (hs : MeasurableSet s) (hfm : AEStronglyMeasurable f (Measure.map φ (μ.restrict (φ ⁻¹' s)).variation)) (hfi' : μ.Integrable (f ∘ φ)) :
∫ᵛ (y : β) in s, f y ∂[B; μ.map φ] = ∫ᵛ (x : X) in φ ⁻¹' s, f (φ x) ∂[B; μ]
source
theorem MeasurableEmbedding.setIntegral_map_vectorMeasure {X : Type u_2} {E : Type u_3} {F : Type u_4} {G : Type u_5} {mX : MeasurableSpace X} [NormedAddCommGroup E] [NormedAddCommGroup F] [NormedAddCommGroup G] {μ : MeasureTheory.VectorMeasure X F} [NormedSpace ℝ E] [NormedSpace ℝ F] [NormedSpace ℝ G] {B : E →L[ℝ] F →L[ℝ] G} {β : Type u_7} [MeasurableSpace β] {φ : X → β} {f : β → E} (hφ : MeasurableEmbedding φ) {s : Set β} (hs : MeasurableSet s) :
∫ᵛ (y : β) in s, f y ∂[B; μ.map φ] = ∫ᵛ (x : X) in φ ⁻¹' s, f (φ x) ∂[B; μ]
source
theorem Topology.IsClosedEmbedding.setIntegral_map_vectorMeasure {X : Type u_2} {E : Type u_3} {F : Type u_4} {G : Type u_5} {mX : MeasurableSpace X} [NormedAddCommGroup E] [NormedAddCommGroup F] [NormedAddCommGroup G] {μ : MeasureTheory.VectorMeasure X F} [NormedSpace ℝ E] [NormedSpace ℝ F] [NormedSpace ℝ G] {B : E →L[ℝ] F →L[ℝ] G} [TopologicalSpace X] [BorelSpace X] {β : Type u_7} [MeasurableSpace β] [TopologicalSpace β] [BorelSpace β] {φ : X → β} {f : β → E} {s : Set β} (hs : MeasurableSet s) (hφ : IsClosedEmbedding φ) :
∫ᵛ (y : β) in s, f y ∂[B; μ.map φ] = ∫ᵛ (x : X) in φ ⁻¹' s, f (φ x) ∂[B; μ]
source
theorem MeasureTheory.VectorMeasure.setIntegral_map_equiv {X : Type u_2} {E : Type u_3} {F : Type u_4} {G : Type u_5} {mX : MeasurableSpace X} [NormedAddCommGroup E] [NormedAddCommGroup F] [NormedAddCommGroup G] {μ : VectorMeasure X F} [NormedSpace ℝ E] [NormedSpace ℝ F] [NormedSpace ℝ G] {B : E →L[ℝ] F →L[ℝ] G} {β : Type u_7} [MeasurableSpace β] {e : X ≃ᵐ β} {f : β → E} {s : Set β} (hs : MeasurableSet s) :
∫ᵛ (y : β) in s, f y ∂[B; μ.map ⇑e] = ∫ᵛ (x : X) in ⇑e ⁻¹' s, f (e x) ∂[B; μ]
source
theorem MeasureTheory.VectorMeasure.continuousLinearMap_apply_integral {X : Type u_2} {E : Type u_3} {F : Type u_4} {G : Type u_5} {H : Type u_6} {mX : MeasurableSpace X} [NormedAddCommGroup E] [NormedAddCommGroup F] [NormedAddCommGroup G] [NormedAddCommGroup H] {μ : VectorMeasure X F} {f : X → E} [NormedSpace ℝ E] [NormedSpace ℝ F] [NormedSpace ℝ G] [NormedSpace ℝ H] {B : E →L[ℝ] F →L[ℝ] G} [CompleteSpace G] [CompleteSpace H] {C : G →L[ℝ] H} (hf : Integrable f μ.variation) :
C ∫ᵛ (y : X), f y ∂[B; μ] = ∫ᵛ (y : X), f y ∂[(ContinuousLinearMap.compL ℝ F G H) C ∘SL B; μ]
source
theorem MeasureTheory.VectorMeasure.integral_continuousLinearMap_comp {X : Type u_2} {E : Type u_3} {F : Type u_4} {G : Type u_5} {H : Type u_6} {mX : MeasurableSpace X} [NormedAddCommGroup E] [NormedAddCommGroup F] [NormedAddCommGroup G] [NormedAddCommGroup H] {μ : VectorMeasure X F} [NormedSpace ℝ E] [NormedSpace ℝ F] [NormedSpace ℝ G] [NormedSpace ℝ H] {B : E →L[ℝ] F →L[ℝ] G} {f : X → H} {C : H →L[ℝ] E} (hf : Integrable f μ.variation) :
∫ᵛ (y : X), C (f y) ∂[B; μ] = ∫ᵛ (y : X), f y ∂[B ∘SL C; μ]
source
theorem MeasureTheory.VectorMeasure.enorm_setIntegral_le_of_enorm_le_const_ae {X : Type u_2} {E : Type u_3} {F : Type u_4} {G : Type u_5} {mX : MeasurableSpace X} [NormedAddCommGroup E] [NormedAddCommGroup F] [NormedAddCommGroup G] {μ : VectorMeasure X F} {f : X → E} {s : Set X} [NormedSpace ℝ E] [NormedSpace ℝ F] [NormedSpace ℝ G] {B : E →L[ℝ] F →L[ℝ] G} {C : ENNReal} (hC : ∀ᵐ (x : X) ∂μ.variation.restrict s, ‖f x‖ₑ ≤ C) :
‖∫ᵛ (x : X) in s, f x ∂[B; μ]‖ₑ ≤ C * ‖B‖ₑ * μ.variation s
source
theorem MeasureTheory.VectorMeasure.enorm_setIntegral_le_of_enorm_le_const {X : Type u_2} {E : Type u_3} {F : Type u_4} {G : Type u_5} {mX : MeasurableSpace X} [NormedAddCommGroup E] [NormedAddCommGroup F] [NormedAddCommGroup G] {μ : VectorMeasure X F} {f : X → E} {s : Set X} [NormedSpace ℝ E] [NormedSpace ℝ F] [NormedSpace ℝ G] {B : E →L[ℝ] F →L[ℝ] G} {C : ENNReal} (hC : ∀ x ∈ s, ‖f x‖ₑ ≤ C) :
‖∫ᵛ (x : X) in s, f x ∂[B; μ]‖ₑ ≤ C * ‖B‖ₑ * μ.variation s
source
theorem MeasureTheory.VectorMeasure.norm_setIntegral_le_of_norm_le_const_ae {X : Type u_2} {E : Type u_3} {F : Type u_4} {G : Type u_5} {mX : MeasurableSpace X} [NormedAddCommGroup E] [NormedAddCommGroup F] [NormedAddCommGroup G] {μ : VectorMeasure X F} {f : X → E} {s : Set X} [NormedSpace ℝ E] [NormedSpace ℝ F] [NormedSpace ℝ G] {B : E →L[ℝ] F →L[ℝ] G} {C : ℝ} [h : IsFiniteMeasure (μ.variation.restrict s)] (hC : ∀ᵐ (x : X) ∂μ.variation.restrict s, ‖f x‖ ≤ C) :
‖∫ᵛ (x : X) in s, f x ∂[B; μ]‖ ≤ C * ‖B‖ * μ.variation.real s
source
theorem MeasureTheory.VectorMeasure.norm_setIntegral_le_of_norm_le_const {X : Type u_2} {E : Type u_3} {F : Type u_4} {G : Type u_5} {mX : MeasurableSpace X} [NormedAddCommGroup E] [NormedAddCommGroup F] [NormedAddCommGroup G] {μ : VectorMeasure X F} {f : X → E} {s : Set X} [NormedSpace ℝ E] [NormedSpace ℝ F] [NormedSpace ℝ G] {B : E →L[ℝ] F →L[ℝ] G} {C : ℝ} [h : IsFiniteMeasure (μ.variation.restrict s)] (hC : ∀ x ∈ s, ‖f x‖ ≤ C) :
‖∫ᵛ (x : X) in s, f x ∂[B; μ]‖ ≤ C * ‖B‖ * μ.variation.real s
source
theorem MeasureTheory.VectorMeasure.enorm_setIntegral_le_lintegral_enorm {X : Type u_2} {E : Type u_3} {F : Type u_4} {G : Type u_5} {mX : MeasurableSpace X} [NormedAddCommGroup E] [NormedAddCommGroup F] [NormedAddCommGroup G] {μ : VectorMeasure X F} {f : X → E} {s : Set X} [NormedSpace ℝ E] [NormedSpace ℝ F] [NormedSpace ℝ G] {B : E →L[ℝ] F →L[ℝ] G} :
‖∫ᵛ (x : X) in s, f x ∂[B; μ]‖ₑ ≤ ‖B‖ₑ * ∫⁻ (x : X) in s, ‖f x‖ₑ ∂μ.variation
source
theorem MeasureTheory.VectorMeasure.enorm_setIntegral_le_lintegral_enorm_transpose {X : Type u_2} {E : Type u_3} {F : Type u_4} {G : Type u_5} {mX : MeasurableSpace X} [NormedAddCommGroup E] [NormedAddCommGroup F] [NormedAddCommGroup G] {μ : VectorMeasure X F} {f : X → E} {s : Set X} [NormedSpace ℝ E] [NormedSpace ℝ F] [NormedSpace ℝ G] {B : E →L[ℝ] F →L[ℝ] G} :
‖∫ᵛ (x : X) in s, f x ∂[B; μ]‖ₑ ≤ ∫⁻ (x : X) in s, ‖f x‖ₑ ∂(μ.transpose B).variation
source
theorem MeasureTheory.VectorMeasure.hasSum_setIntegral_iUnion {X : Type u_2} {E : Type u_3} {F : Type u_4} {G : Type u_5} {mX : MeasurableSpace X} [NormedAddCommGroup E] [NormedAddCommGroup F] [NormedAddCommGroup G] {μ : VectorMeasure X F} {f : X → E} [NormedSpace ℝ E] [NormedSpace ℝ F] [NormedSpace ℝ G] {B : E →L[ℝ] F →L[ℝ] G} {ι : Type u_7} [Countable ι] {s : ι → Set X} (hm : ∀ (i : ι), MeasurableSet (s i)) (hd : Pairwise (Function.onFun Disjoint s)) (hfi : μ.IntegrableOn f (⋃ (i : ι), s i)) :
HasSum (fun (n : ι) => ∫ᵛ (x : X) in s n, f x ∂[B; μ]) ∫ᵛ (x : X) in ⋃ (n : ι), s n, f x ∂[B; μ]
source
theorem MeasureTheory.VectorMeasure.integral_iUnion {X : Type u_2} {E : Type u_3} {F : Type u_4} {G : Type u_5} {mX : MeasurableSpace X} [NormedAddCommGroup E] [NormedAddCommGroup F] [NormedAddCommGroup G] {μ : VectorMeasure X F} {f : X → E} [NormedSpace ℝ E] [NormedSpace ℝ F] [NormedSpace ℝ G] {B : E →L[ℝ] F →L[ℝ] G} {ι : Type u_7} [Countable ι] {s : ι → Set X} (hm : ∀ (i : ι), MeasurableSet (s i)) (hd : Pairwise (Function.onFun Disjoint s)) (hfi : μ.IntegrableOn f (⋃ (i : ι), s i)) :
∫ᵛ (x : X) in ⋃ (n : ι), s n, f x ∂[B; μ] = ∑' (n : ι), ∫ᵛ (x : X) in s n, f x ∂[B; μ]
source
@[simp]
theorem MeasureTheory.VectorMeasure.setIntegral_toSignedMeasure {X : Type u_2} {G : Type u_5} {mX : MeasurableSpace X} [NormedAddCommGroup G] [NormedSpace ℝ G] {μ : Measure X} [IsFiniteMeasure μ] {f : X → G} {s : Set X} (hs : MeasurableSet s) :
∫ᵛ (x : X) in s, f x ∂<•μ.toSignedMeasure = ∫ (x : X) in s, f x ∂μ
source
theorem MeasureTheory.VectorMeasure.Integrable.tendsto_setIntegral_nhds_zero {X : Type u_2} {E : Type u_3} {F : Type u_4} {G : Type u_5} {mX : MeasurableSpace X} [NormedAddCommGroup E] [NormedAddCommGroup F] [NormedAddCommGroup G] {μ : VectorMeasure X F} {f : X → E} [NormedSpace ℝ E] [NormedSpace ℝ F] [NormedSpace ℝ G] {B : E →L[ℝ] F →L[ℝ] G} {ι : Type u_7} (hf : μ.Integrable f) {l : Filter ι} {s : ι → Set X} (hs : Filter.Tendsto (⇑μ.variation ∘ s) l (nhds 0)) :
Filter.Tendsto (fun (i : ι) => ∫ᵛ (x : X) in s i, f x ∂[B; μ]) l (nhds 0)

If f is integrable, then ∫ᵛ x in s, f x ∂[B; μ] is absolutely continuous in s: it tends to zero as μ.variation s tends to zero.

source
theorem MeasureTheory.VectorMeasure.tendsto_setIntegral_of_L1 {X : Type u_2} {E : Type u_3} {F : Type u_4} {G : Type u_5} {mX : MeasurableSpace X} [NormedAddCommGroup E] [NormedAddCommGroup F] [NormedAddCommGroup G] {μ : VectorMeasure X F} [NormedSpace ℝ E] [NormedSpace ℝ F] [NormedSpace ℝ G] {B : E →L[ℝ] F →L[ℝ] G} {ι : Type u_7} (f : X → E) (hfi : AEStronglyMeasurable f μ.variation) {F✝ : ι → X → E} {l : Filter ι} (hFi : ∀ᶠ (i : ι) in l, μ.Integrable (F✝ i)) (hF : Filter.Tendsto (fun (i : ι) => ∫⁻ (x : X), ‖F✝ i x - f x‖ₑ ∂μ.variation) l (nhds 0)) (s : Set X) :
Filter.Tendsto (fun (i : ι) => ∫ᵛ (x : X) in s, F✝ i x ∂[B; μ]) l (nhds ∫ᵛ (x : X) in s, f x ∂[B; μ])

If F i → f in L1, then ∫ᵛ x in s, F i x ∂[B; μ] → ∫ᵛ x in s, f x ∂[B; μ].

source
theorem MeasureTheory.VectorMeasure.tendsto_setIntegral_of_L1' {X : Type u_2} {E : Type u_3} {F : Type u_4} {G : Type u_5} {mX : MeasurableSpace X} [NormedAddCommGroup E] [NormedAddCommGroup F] [NormedAddCommGroup G] {μ : VectorMeasure X F} [NormedSpace ℝ E] [NormedSpace ℝ F] [NormedSpace ℝ G] {B : E →L[ℝ] F →L[ℝ] G} {ι : Type u_7} (f : X → E) (hfi : AEStronglyMeasurable f μ.variation) {F✝ : ι → X → E} {l : Filter ι} (hFi : ∀ᶠ (i : ι) in l, μ.Integrable (F✝ i)) (hF : Filter.Tendsto (fun (i : ι) => eLpNorm (F✝ i - f) 1 μ.variation) l (nhds 0)) (s : Set X) :
Filter.Tendsto (fun (i : ι) => ∫ᵛ (x : X) in s, F✝ i x ∂[B; μ]) l (nhds ∫ᵛ (x : X) in s, f x ∂[B; μ])

If F i → f in L1, then ∫ᵛ x in s, F i x ∂[B; μ] → ∫ᵛ x in s, f x ∂[B; μ].