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})