Documentation

Mathlib.MeasureTheory.Integral.IntegrableOn

Functions integrable on a set and at a filter #

We define IntegrableOn f s μ := Integrable f (μ.restrict s) and prove theorems like integrableOn_union : IntegrableOn f (s ∪ t) μ ↔ IntegrableOn f s μ ∧ IntegrableOn f t μ.

Next we define a predicate IntegrableAtFilter (f : α → E) (l : Filter α) (μ : Measure α) saying that f is integrable at some set s ∈ l and prove that a measurable function is integrable at l with respect to μ provided that f is bounded above at l ⊓ μ.ae and μ is finite at l.

def StronglyMeasurableAtFilter {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [TopologicalSpace β] (f : αβ) (l : Filter α) (μ : autoParam (MeasureTheory.Measure α) _auto✝) :

A function f is strongly measurable at a filter l w.r.t. a measure μ if it is ae strongly measurable w.r.t. μ.restrict s for some s ∈ l.

Equations
Instances For
    @[simp]
    theorem stronglyMeasurableAt_bot {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [TopologicalSpace β] {μ : MeasureTheory.Measure α} {f : αβ} :
    theorem StronglyMeasurableAtFilter.filter_mono {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [TopologicalSpace β] {l : Filter α} {l' : Filter α} {f : αβ} {μ : MeasureTheory.Measure α} (h : StronglyMeasurableAtFilter f l μ) (h' : l' l) :
    theorem MeasureTheory.hasFiniteIntegral_restrict_of_bounded {α : Type u_1} {E : Type u_3} [MeasurableSpace α] [NormedAddCommGroup E] {f : αE} {s : Set α} {μ : MeasureTheory.Measure α} {C : } (hs : μ s < ) (hf : ∀ᵐ (x : α) ∂MeasureTheory.Measure.restrict μ s, f x C) :
    def MeasureTheory.IntegrableOn {α : Type u_1} {E : Type u_3} [MeasurableSpace α] [NormedAddCommGroup E] (f : αE) (s : Set α) (μ : autoParam (MeasureTheory.Measure α) _auto✝) :

    A function is IntegrableOn a set s if it is almost everywhere strongly measurable on s and if the integral of its pointwise norm over s is less than infinity.

    Equations
    Instances For
      theorem MeasureTheory.integrableOn_zero {α : Type u_1} {E : Type u_3} [MeasurableSpace α] [NormedAddCommGroup E] {s : Set α} {μ : MeasureTheory.Measure α} :
      MeasureTheory.IntegrableOn (fun (x : α) => 0) s μ
      @[simp]
      theorem MeasureTheory.integrableOn_const {α : Type u_1} {E : Type u_3} [MeasurableSpace α] [NormedAddCommGroup E] {s : Set α} {μ : MeasureTheory.Measure α} {C : E} :
      MeasureTheory.IntegrableOn (fun (x : α) => C) s μ C = 0 μ s <
      theorem MeasureTheory.IntegrableOn.mono {α : Type u_1} {E : Type u_3} [MeasurableSpace α] [NormedAddCommGroup E] {f : αE} {s : Set α} {t : Set α} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure α} (h : MeasureTheory.IntegrableOn f t ν) (hs : s t) (hμ : μ ν) :
      theorem MeasureTheory.IntegrableOn.mono_set {α : Type u_1} {E : Type u_3} [MeasurableSpace α] [NormedAddCommGroup E] {f : αE} {s : Set α} {t : Set α} {μ : MeasureTheory.Measure α} (h : MeasureTheory.IntegrableOn f t μ) (hst : s t) :
      theorem MeasureTheory.IntegrableOn.mono_measure {α : Type u_1} {E : Type u_3} [MeasurableSpace α] [NormedAddCommGroup E] {f : αE} {s : Set α} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure α} (h : MeasureTheory.IntegrableOn f s ν) (hμ : μ ν) :
      theorem MeasureTheory.IntegrableOn.congr_fun {α : Type u_1} {E : Type u_3} [MeasurableSpace α] [NormedAddCommGroup E] {f : αE} {g : αE} {s : Set α} {μ : MeasureTheory.Measure α} (h : MeasureTheory.IntegrableOn f s μ) (hst : Set.EqOn f g s) (hs : MeasurableSet s) :
      theorem MeasureTheory.integrableOn_congr_fun {α : Type u_1} {E : Type u_3} [MeasurableSpace α] [NormedAddCommGroup E] {f : αE} {g : αE} {s : Set α} {μ : MeasureTheory.Measure α} (hst : Set.EqOn f g s) (hs : MeasurableSet s) :
      theorem MeasureTheory.Integrable.piecewise {α : Type u_1} {E : Type u_3} [MeasurableSpace α] [NormedAddCommGroup E] {f : αE} {g : αE} {s : Set α} {μ : MeasureTheory.Measure α} [DecidablePred fun (x : α) => x s] (hs : MeasurableSet s) (hf : MeasureTheory.IntegrableOn f s μ) (hg : MeasureTheory.IntegrableOn g s μ) :
      theorem MeasureTheory.IntegrableOn.left_of_union {α : Type u_1} {E : Type u_3} [MeasurableSpace α] [NormedAddCommGroup E] {f : αE} {s : Set α} {t : Set α} {μ : MeasureTheory.Measure α} (h : MeasureTheory.IntegrableOn f (s t) μ) :
      theorem MeasureTheory.IntegrableOn.right_of_union {α : Type u_1} {E : Type u_3} [MeasurableSpace α] [NormedAddCommGroup E] {f : αE} {s : Set α} {t : Set α} {μ : MeasureTheory.Measure α} (h : MeasureTheory.IntegrableOn f (s t) μ) :
      theorem MeasureTheory.IntegrableOn.union {α : Type u_1} {E : Type u_3} [MeasurableSpace α] [NormedAddCommGroup E] {f : αE} {s : Set α} {t : Set α} {μ : MeasureTheory.Measure α} (hs : MeasureTheory.IntegrableOn f s μ) (ht : MeasureTheory.IntegrableOn f t μ) :
      @[simp]
      theorem MeasureTheory.integrableOn_singleton_iff {α : Type u_1} {E : Type u_3} [MeasurableSpace α] [NormedAddCommGroup E] {f : αE} {μ : MeasureTheory.Measure α} {x : α} [MeasurableSingletonClass α] :
      MeasureTheory.IntegrableOn f {x} μ f x = 0 μ {x} <
      @[simp]
      theorem MeasureTheory.integrableOn_finite_biUnion {α : Type u_1} {β : Type u_2} {E : Type u_3} [MeasurableSpace α] [NormedAddCommGroup E] {f : αE} {μ : MeasureTheory.Measure α} {s : Set β} (hs : Set.Finite s) {t : βSet α} :
      MeasureTheory.IntegrableOn f (⋃ i ∈ s, t i) μ is, MeasureTheory.IntegrableOn f (t i) μ
      @[simp]
      theorem MeasureTheory.integrableOn_finset_iUnion {α : Type u_1} {β : Type u_2} {E : Type u_3} [MeasurableSpace α] [NormedAddCommGroup E] {f : αE} {μ : MeasureTheory.Measure α} {s : Finset β} {t : βSet α} :
      MeasureTheory.IntegrableOn f (⋃ i ∈ s, t i) μ is, MeasureTheory.IntegrableOn f (t i) μ
      @[simp]
      theorem MeasureTheory.integrableOn_finite_iUnion {α : Type u_1} {β : Type u_2} {E : Type u_3} [MeasurableSpace α] [NormedAddCommGroup E] {f : αE} {μ : MeasureTheory.Measure α} [Finite β] {t : βSet α} :
      MeasureTheory.IntegrableOn f (⋃ (i : β), t i) μ ∀ (i : β), MeasureTheory.IntegrableOn f (t i) μ
      theorem MeasureTheory.integrableOn_map_equiv {α : Type u_1} {β : Type u_2} {E : Type u_3} [MeasurableSpace α] [NormedAddCommGroup E] [MeasurableSpace β] (e : α ≃ᵐ β) {f : βE} {μ : MeasureTheory.Measure α} {s : Set β} :
      theorem MeasureTheory.MeasurePreserving.integrableOn_image {α : Type u_1} {β : Type u_2} {E : Type u_3} [MeasurableSpace α] [NormedAddCommGroup E] {μ : MeasureTheory.Measure α} [MeasurableSpace β] {e : αβ} {ν : MeasureTheory.Measure β} (h₁ : MeasureTheory.MeasurePreserving e μ ν) (h₂ : MeasurableEmbedding e) {f : βE} {s : Set α} :
      theorem MeasureTheory.IntegrableOn.indicator {α : Type u_1} {E : Type u_3} [MeasurableSpace α] [NormedAddCommGroup E] {f : αE} {s : Set α} {t : Set α} {μ : MeasureTheory.Measure α} (h : MeasureTheory.IntegrableOn f s μ) (ht : MeasurableSet t) :
      theorem MeasureTheory.integrable_indicatorConstLp {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {E : Type u_5} [NormedAddCommGroup E] {p : ENNReal} {s : Set α} (hs : MeasurableSet s) (hμs : μ s ) (c : E) :

      If a function is integrable on a set s and nonzero there, then the measurable hull of s is well behaved: the restriction of the measure to toMeasurable μ s coincides with its restriction to s.

      theorem MeasureTheory.IntegrableOn.of_ae_diff_eq_zero {α : Type u_1} {E : Type u_3} [MeasurableSpace α] [NormedAddCommGroup E] {f : αE} {s : Set α} {t : Set α} {μ : MeasureTheory.Measure α} (hf : MeasureTheory.IntegrableOn f s μ) (ht : MeasureTheory.NullMeasurableSet t μ) (h't : ∀ᵐ (x : α) ∂μ, x t \ sf x = 0) :

      If a function is integrable on a set s, and vanishes on t \ s, then it is integrable on t if t is null-measurable.

      theorem MeasureTheory.IntegrableOn.of_forall_diff_eq_zero {α : Type u_1} {E : Type u_3} [MeasurableSpace α] [NormedAddCommGroup E] {f : αE} {s : Set α} {t : Set α} {μ : MeasureTheory.Measure α} (hf : MeasureTheory.IntegrableOn f s μ) (ht : MeasurableSet t) (h't : xt \ s, f x = 0) :

      If a function is integrable on a set s, and vanishes on t \ s, then it is integrable on t if t is measurable.

      theorem MeasureTheory.IntegrableOn.integrable_of_ae_not_mem_eq_zero {α : Type u_1} {E : Type u_3} [MeasurableSpace α] [NormedAddCommGroup E] {f : αE} {s : Set α} {μ : MeasureTheory.Measure α} (hf : MeasureTheory.IntegrableOn f s μ) (h't : ∀ᵐ (x : α) ∂μ, xsf x = 0) :

      If a function is integrable on a set s and vanishes almost everywhere on its complement, then it is integrable.

      theorem MeasureTheory.IntegrableOn.integrable_of_forall_not_mem_eq_zero {α : Type u_1} {E : Type u_3} [MeasurableSpace α] [NormedAddCommGroup E] {f : αE} {s : Set α} {μ : MeasureTheory.Measure α} (hf : MeasureTheory.IntegrableOn f s μ) (h't : xs, f x = 0) :

      If a function is integrable on a set s and vanishes everywhere on its complement, then it is integrable.

      theorem MeasureTheory.integrableOn_Lp_of_measure_ne_top {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {E : Type u_5} [NormedAddCommGroup E] {p : ENNReal} {s : Set α} (f : (MeasureTheory.Lp E p μ)) (hp : 1 p) (hμs : μ s ) :
      theorem MeasureTheory.Integrable.lintegral_lt_top {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {f : α} (hf : MeasureTheory.Integrable f μ) :
      ∫⁻ (x : α), ENNReal.ofReal (f x)μ <
      theorem MeasureTheory.IntegrableOn.set_lintegral_lt_top {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {f : α} {s : Set α} (hf : MeasureTheory.IntegrableOn f s μ) :
      ∫⁻ (x : α) in s, ENNReal.ofReal (f x)μ <

      We say that a function f is integrable at filter l if it is integrable on some set s ∈ l. Equivalently, it is eventually integrable on s in l.smallSets.

      Equations
      Instances For
        theorem MeasureTheory.IntegrableAtFilter.smul {α : Type u_1} {E : Type u_3} [MeasurableSpace α] [NormedAddCommGroup E] {μ : MeasureTheory.Measure α} {l : Filter α} {𝕜 : Type u_5} [NormedAddCommGroup 𝕜] [SMulZeroClass 𝕜 E] [BoundedSMul 𝕜 E] {f : αE} (hf : MeasureTheory.IntegrableAtFilter f l μ) (c : 𝕜) :
        theorem MeasureTheory.IntegrableAtFilter.norm {α : Type u_1} {E : Type u_3} [MeasurableSpace α] [NormedAddCommGroup E] {f : αE} {μ : MeasureTheory.Measure α} {l : Filter α} (hf : MeasureTheory.IntegrableAtFilter f l μ) :
        MeasureTheory.IntegrableAtFilter (fun (x : α) => f x) l μ
        theorem MeasureTheory.IntegrableAtFilter.filter_mono {α : Type u_1} {E : Type u_3} [MeasurableSpace α] [NormedAddCommGroup E] {f : αE} {μ : MeasureTheory.Measure α} {l : Filter α} {l' : Filter α} (hl : l l') (hl' : MeasureTheory.IntegrableAtFilter f l' μ) :

        If μ is a measure finite at filter l and f is a function such that its norm is bounded above at l, then f is integrable at l.

        theorem MeasureTheory.Measure.integrableOn_of_bounded {α : Type u_1} {E : Type u_3} [MeasurableSpace α] [NormedAddCommGroup E] {f : αE} {s : Set α} {μ : MeasureTheory.Measure α} (s_finite : μ s ) (f_mble : MeasureTheory.AEStronglyMeasurable f μ) {M : } (f_bdd : ∀ᵐ (a : α) ∂MeasureTheory.Measure.restrict μ s, f a M) :

        A function which is continuous on a set s is almost everywhere measurable with respect to μ.restrict s.

        A function which is continuous on a separable set s is almost everywhere strongly measurable with respect to μ.restrict s.

        A function which is continuous on a set s is almost everywhere strongly measurable with respect to μ.restrict s when either the source space or the target space is second-countable.

        A function which is continuous on a compact set s is almost everywhere strongly measurable with respect to μ.restrict s.

        If a function is continuous on an open set s, then it is strongly measurable at the filter 𝓝 x for all x ∈ s if either the source space or the target space is second-countable.

        theorem ContinuousAt.stronglyMeasurableAtFilter {α : Type u_1} {E : Type u_3} [MeasurableSpace α] [NormedAddCommGroup E] [TopologicalSpace α] [OpensMeasurableSpace α] [SecondCountableTopologyEither α E] {f : αE} {s : Set α} {μ : MeasureTheory.Measure α} (hs : IsOpen s) (hf : xs, ContinuousAt f x) (x : α) :

        If a function is continuous on a measurable set s, then it is measurable at the filter 𝓝[s] x for all x.

        Lemmas about adding and removing interval boundaries #

        The primed lemmas take explicit arguments about the measure being finite at the endpoint, while the unprimed ones use [NoAtoms μ].

        theorem integrableOn_Icc_iff_integrableOn_Ioc' {α : Type u_1} {E : Type u_3} [MeasurableSpace α] [NormedAddCommGroup E] [PartialOrder α] [MeasurableSingletonClass α] {f : αE} {μ : MeasureTheory.Measure α} {a : α} {b : α} (ha : μ {a} ) :
        theorem integrableOn_Icc_iff_integrableOn_Ico' {α : Type u_1} {E : Type u_3} [MeasurableSpace α] [NormedAddCommGroup E] [PartialOrder α] [MeasurableSingletonClass α] {f : αE} {μ : MeasureTheory.Measure α} {a : α} {b : α} (hb : μ {b} ) :
        theorem integrableOn_Ico_iff_integrableOn_Ioo' {α : Type u_1} {E : Type u_3} [MeasurableSpace α] [NormedAddCommGroup E] [PartialOrder α] [MeasurableSingletonClass α] {f : αE} {μ : MeasureTheory.Measure α} {a : α} {b : α} (ha : μ {a} ) :
        theorem integrableOn_Ioc_iff_integrableOn_Ioo' {α : Type u_1} {E : Type u_3} [MeasurableSpace α] [NormedAddCommGroup E] [PartialOrder α] [MeasurableSingletonClass α] {f : αE} {μ : MeasureTheory.Measure α} {a : α} {b : α} (hb : μ {b} ) :
        theorem integrableOn_Icc_iff_integrableOn_Ioo' {α : Type u_1} {E : Type u_3} [MeasurableSpace α] [NormedAddCommGroup E] [PartialOrder α] [MeasurableSingletonClass α] {f : αE} {μ : MeasureTheory.Measure α} {a : α} {b : α} (ha : μ {a} ) (hb : μ {b} ) :