# mathlib3documentation

measure_theory.integral.integrable_on

# Functions integrable on a set and at a filter #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

We define integrable_on f s μ := integrable f (μ.restrict s) and prove theorems like integrable_on_union : integrable_on f (s ∪ t) μ ↔ integrable_on f s μ ∧ integrable_on f t μ.

Next we define a predicate integrable_at_filter (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 strongly_measurable_at_filter {α : Type u_1} {β : Type u_2} (f : α β) (l : filter α) (μ : . "volume_tac") :
Prop

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
@[simp]
theorem strongly_measurable_at_bot {α : Type u_1} {β : Type u_2} {μ : measure_theory.measure α} {f : α β} :
@[protected]
theorem strongly_measurable_at_filter.eventually {α : Type u_1} {β : Type u_2} {l : filter α} {f : α β} {μ : measure_theory.measure α} (h : μ) :
∀ᶠ (s : set α) in l.small_sets,
@[protected]
theorem strongly_measurable_at_filter.filter_mono {α : Type u_1} {β : Type u_2} {l l' : filter α} {f : α β} {μ : measure_theory.measure α} (h : μ) (h' : l' l) :
@[protected]
theorem measure_theory.ae_strongly_measurable.strongly_measurable_at_filter {α : Type u_1} {β : Type u_2} {l : filter α} {f : α β} {μ : measure_theory.measure α}  :
theorem ae_strongly_measurable.strongly_measurable_at_filter_of_mem {α : Type u_1} {β : Type u_2} {l : filter α} {f : α β} {μ : measure_theory.measure α} {s : set α} (h : (μ.restrict s)) (hl : s l) :
@[protected]
theorem measure_theory.strongly_measurable.strongly_measurable_at_filter {α : Type u_1} {β : Type u_2} {l : filter α} {f : α β} {μ : measure_theory.measure α}  :
theorem measure_theory.has_finite_integral_restrict_of_bounded {α : Type u_1} {E : Type u_3} {f : α E} {s : set α} {μ : measure_theory.measure α} {C : } (hs : μ s < ) (hf : ∀ᵐ (x : α) μ.restrict s, f x C) :
def measure_theory.integrable_on {α : Type u_1} {E : Type u_3} (f : α E) (s : set α) (μ : . "volume_tac") :
Prop

A function is integrable_on 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
theorem measure_theory.integrable_on.integrable {α : Type u_1} {E : Type u_3} {f : α E} {s : set α} {μ : measure_theory.measure α} (h : μ) :
@[simp]
theorem measure_theory.integrable_on_empty {α : Type u_1} {E : Type u_3} {f : α E} {μ : measure_theory.measure α} :
@[simp]
theorem measure_theory.integrable_on_univ {α : Type u_1} {E : Type u_3} {f : α E} {μ : measure_theory.measure α} :
theorem measure_theory.integrable_on_zero {α : Type u_1} {E : Type u_3} {s : set α} {μ : measure_theory.measure α} :
measure_theory.integrable_on (λ (_x : α), 0) s μ
@[simp]
theorem measure_theory.integrable_on_const {α : Type u_1} {E : Type u_3} {s : set α} {μ : measure_theory.measure α} {C : E} :
measure_theory.integrable_on (λ (_x : α), C) s μ C = 0 μ s <
theorem measure_theory.integrable_on.mono {α : Type u_1} {E : Type u_3} {f : α E} {s t : set α} {μ ν : measure_theory.measure α} (h : ν) (hs : s t) (hμ : μ ν) :
theorem measure_theory.integrable_on.mono_set {α : Type u_1} {E : Type u_3} {f : α E} {s t : set α} {μ : measure_theory.measure α} (h : μ) (hst : s t) :
theorem measure_theory.integrable_on.mono_measure {α : Type u_1} {E : Type u_3} {f : α E} {s : set α} {μ ν : measure_theory.measure α} (h : ν) (hμ : μ ν) :
theorem measure_theory.integrable_on.mono_set_ae {α : Type u_1} {E : Type u_3} {f : α E} {s t : set α} {μ : measure_theory.measure α} (h : μ) (hst : s ≤ᵐ[μ] t) :
theorem measure_theory.integrable_on.congr_set_ae {α : Type u_1} {E : Type u_3} {f : α E} {s t : set α} {μ : measure_theory.measure α} (h : μ) (hst : s =ᵐ[μ] t) :
theorem measure_theory.integrable_on.congr_fun_ae {α : Type u_1} {E : Type u_3} {f g : α E} {s : set α} {μ : measure_theory.measure α} (h : μ) (hst : f =ᵐ[μ.restrict s] g) :
theorem measure_theory.integrable_on_congr_fun_ae {α : Type u_1} {E : Type u_3} {f g : α E} {s : set α} {μ : measure_theory.measure α} (hst : f =ᵐ[μ.restrict s] g) :
theorem measure_theory.integrable_on.congr_fun {α : Type u_1} {E : Type u_3} {f g : α E} {s : set α} {μ : measure_theory.measure α} (h : μ) (hst : g s) (hs : measurable_set s) :
theorem measure_theory.integrable_on_congr_fun {α : Type u_1} {E : Type u_3} {f g : α E} {s : set α} {μ : measure_theory.measure α} (hst : g s) (hs : measurable_set s) :
theorem measure_theory.integrable.integrable_on {α : Type u_1} {E : Type u_3} {f : α E} {s : set α} {μ : measure_theory.measure α} (h : μ) :
theorem measure_theory.integrable_on.restrict {α : Type u_1} {E : Type u_3} {f : α E} {s t : set α} {μ : measure_theory.measure α} (h : μ) (hs : measurable_set s) :
(μ.restrict t)
theorem measure_theory.integrable_on.left_of_union {α : Type u_1} {E : Type u_3} {f : α E} {s t : set α} {μ : measure_theory.measure α} (h : (s t) μ) :
theorem measure_theory.integrable_on.right_of_union {α : Type u_1} {E : Type u_3} {f : α E} {s t : set α} {μ : measure_theory.measure α} (h : (s t) μ) :
theorem measure_theory.integrable_on.union {α : Type u_1} {E : Type u_3} {f : α E} {s t : set α} {μ : measure_theory.measure α} (hs : μ) (ht : μ) :
(s t) μ
@[simp]
theorem measure_theory.integrable_on_union {α : Type u_1} {E : Type u_3} {f : α E} {s t : set α} {μ : measure_theory.measure α} :
(s t) μ
@[simp]
theorem measure_theory.integrable_on_singleton_iff {α : Type u_1} {E : Type u_3} {f : α E} {μ : measure_theory.measure α} {x : α}  :
μ f x = 0 μ {x} <
@[simp]
theorem measure_theory.integrable_on_finite_bUnion {α : Type u_1} {β : Type u_2} {E : Type u_3} {f : α E} {μ : measure_theory.measure α} {s : set β} (hs : s.finite) {t : β set α} :
( (i : β) (H : i s), t i) μ (i : β), i s (t i) μ
@[simp]
theorem measure_theory.integrable_on_finset_Union {α : Type u_1} {β : Type u_2} {E : Type u_3} {f : α E} {μ : measure_theory.measure α} {s : finset β} {t : β set α} :
( (i : β) (H : i s), t i) μ (i : β), i s (t i) μ
@[simp]
theorem measure_theory.integrable_on_finite_Union {α : Type u_1} {β : Type u_2} {E : Type u_3} {f : α E} {μ : measure_theory.measure α} [finite β] {t : β set α} :
( (i : β), t i) μ (i : β), (t i) μ
theorem measure_theory.integrable_on.add_measure {α : Type u_1} {E : Type u_3} {f : α E} {s : set α} {μ ν : measure_theory.measure α} (hμ : μ) (hν : ν) :
+ ν)
@[simp]
theorem measure_theory.integrable_on_add_measure {α : Type u_1} {E : Type u_3} {f : α E} {s : set α} {μ ν : measure_theory.measure α} :
+ ν)
theorem measurable_embedding.integrable_on_map_iff {α : Type u_1} {β : Type u_2} {E : Type u_3} {e : α β} (he : measurable_embedding e) {f : β E} {μ : measure_theory.measure α} {s : set β} :
(e ⁻¹' s) μ
theorem measure_theory.integrable_on_map_equiv {α : Type u_1} {β : Type u_2} {E : Type u_3} (e : α ≃ᵐ β) {f : β E} {μ : measure_theory.measure α} {s : set β} :
(e ⁻¹' s) μ
theorem measure_theory.measure_preserving.integrable_on_comp_preimage {α : Type u_1} {β : Type u_2} {E : Type u_3} {μ : measure_theory.measure α} {e : α β} {ν : . "volume_tac"} (h₁ : ν) (h₂ : measurable_embedding e) {f : β E} {s : set β} :
(e ⁻¹' s) μ
theorem measure_theory.measure_preserving.integrable_on_image {α : Type u_1} {β : Type u_2} {E : Type u_3} {μ : measure_theory.measure α} {e : α β} {ν : . "volume_tac"} (h₁ : ν) (h₂ : measurable_embedding e) {f : β E} {s : set α} :
(e '' s) ν s μ
theorem measure_theory.integrable_indicator_iff {α : Type u_1} {E : Type u_3} {f : α E} {s : set α} {μ : measure_theory.measure α} (hs : measurable_set s) :
theorem measure_theory.integrable_on.integrable_indicator {α : Type u_1} {E : Type u_3} {f : α E} {s : set α} {μ : measure_theory.measure α} (h : μ) (hs : measurable_set s) :
theorem measure_theory.integrable.indicator {α : Type u_1} {E : Type u_3} {f : α E} {s : set α} {μ : measure_theory.measure α} (h : μ) (hs : measurable_set s) :
theorem measure_theory.integrable_on.indicator {α : Type u_1} {E : Type u_3} {f : α E} {s t : set α} {μ : measure_theory.measure α} (h : μ) (ht : measurable_set t) :
μ
theorem measure_theory.integrable_indicator_const_Lp {α : Type u_1} {μ : measure_theory.measure α} {E : Type u_2} {p : ennreal} {s : set α} (hs : measurable_set s) (hμs : μ s ) (c : E) :
μ
theorem measure_theory.integrable_on.restrict_to_measurable {α : Type u_1} {E : Type u_3} {f : α E} {s : set α} {μ : measure_theory.measure α} (hf : μ) (h's : (x : α), x s f x 0) :
= μ.restrict s

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 to_measurable μ s coincides with its restriction to s.

theorem measure_theory.integrable_on.of_ae_diff_eq_zero {α : Type u_1} {E : Type u_3} {f : α E} {s t : set α} {μ : measure_theory.measure α} (hf : μ) (ht : μ) (h't : ∀ᵐ (x : α) μ, x t \ 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 null-measurable.

theorem measure_theory.integrable_on.of_forall_diff_eq_zero {α : Type u_1} {E : Type u_3} {f : α E} {s t : set α} {μ : measure_theory.measure α} (hf : μ) (ht : measurable_set t) (h't : (x : α), x t \ 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 measure_theory.integrable_on.integrable_of_ae_not_mem_eq_zero {α : Type u_1} {E : Type u_3} {f : α E} {s : set α} {μ : measure_theory.measure α} (hf : μ) (h't : ∀ᵐ (x : α) μ, x s f x = 0) :

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

theorem measure_theory.integrable_on.integrable_of_forall_not_mem_eq_zero {α : Type u_1} {E : Type u_3} {f : α E} {s : set α} {μ : measure_theory.measure α} (hf : μ) (h't : (x : α), x s f x = 0) :

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

theorem measure_theory.integrable_on_iff_integrable_of_support_subset {α : Type u_1} {E : Type u_3} {f : α E} {s : set α} {μ : measure_theory.measure α} (h1s : s) :
theorem measure_theory.integrable_on_Lp_of_measure_ne_top {α : Type u_1} {μ : measure_theory.measure α} {E : Type u_2} {p : ennreal} {s : set α} (f : μ)) (hp : 1 p) (hμs : μ s ) :
theorem measure_theory.integrable.lintegral_lt_top {α : Type u_1} {μ : measure_theory.measure α} {f : α } (hf : μ) :
∫⁻ (x : α), ennreal.of_real (f x) μ <
theorem measure_theory.integrable_on.set_lintegral_lt_top {α : Type u_1} {μ : measure_theory.measure α} {f : α } {s : set α} (hf : μ) :
∫⁻ (x : α) in s, ennreal.of_real (f x) μ <
def measure_theory.integrable_at_filter {α : Type u_1} {E : Type u_3} (f : α E) (l : filter α) (μ : . "volume_tac") :
Prop

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.small_sets.

Equations
theorem measure_theory.integrable.integrable_at_filter {α : Type u_1} {E : Type u_3} {f : α E} {μ : measure_theory.measure α} (h : μ) (l : filter α) :
@[protected]
theorem measure_theory.integrable_at_filter.eventually {α : Type u_1} {E : Type u_3} {f : α E} {μ : measure_theory.measure α} {l : filter α} (h : μ) :
∀ᶠ (s : set α) in l.small_sets,
theorem measure_theory.integrable_at_filter.filter_mono {α : Type u_1} {E : Type u_3} {f : α E} {μ : measure_theory.measure α} {l l' : filter α} (hl : l l') (hl' : μ) :
theorem measure_theory.integrable_at_filter.inf_of_left {α : Type u_1} {E : Type u_3} {f : α E} {μ : measure_theory.measure α} {l l' : filter α} (hl : μ) :
(l l') μ
theorem measure_theory.integrable_at_filter.inf_of_right {α : Type u_1} {E : Type u_3} {f : α E} {μ : measure_theory.measure α} {l l' : filter α} (hl : μ) :
(l' l) μ
@[simp]
theorem measure_theory.integrable_at_filter.inf_ae_iff {α : Type u_1} {E : Type u_3} {f : α E} {μ : measure_theory.measure α} {l : filter α} :
theorem measure_theory.integrable_at_filter.of_inf_ae {α : Type u_1} {E : Type u_3} {f : α E} {μ : measure_theory.measure α} {l : filter α} :

Alias of the forward direction of measure_theory.integrable_at_filter.inf_ae_iff.

theorem measure_theory.measure.finite_at_filter.integrable_at_filter {α : Type u_1} {E : Type u_3} {f : α E} {μ : measure_theory.measure α} {l : filter α} (hfm : μ) (hμ : μ.finite_at_filter l) (hf : ) :

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 measure_theory.measure.finite_at_filter.integrable_at_filter_of_tendsto_ae {α : Type u_1} {E : Type u_3} {f : α E} {μ : measure_theory.measure α} {l : filter α} (hfm : μ) (hμ : μ.finite_at_filter l) {b : E} (hf : (l μ.ae) (nhds b)) :
theorem filter.tendsto.integrable_at_filter_ae {α : Type u_1} {E : Type u_3} {f : α E} {μ : measure_theory.measure α} {l : filter α} (hfm : μ) (hμ : μ.finite_at_filter l) {b : E} (hf : (l μ.ae) (nhds b)) :

Alias of measure_theory.measure.finite_at_filter.integrable_at_filter_of_tendsto_ae.

theorem measure_theory.measure.finite_at_filter.integrable_at_filter_of_tendsto {α : Type u_1} {E : Type u_3} {f : α E} {μ : measure_theory.measure α} {l : filter α} (hfm : μ) (hμ : μ.finite_at_filter l) {b : E} (hf : (nhds b)) :
theorem filter.tendsto.integrable_at_filter {α : Type u_1} {E : Type u_3} {f : α E} {μ : measure_theory.measure α} {l : filter α} (hfm : μ) (hμ : μ.finite_at_filter l) {b : E} (hf : (nhds b)) :

Alias of measure_theory.measure.finite_at_filter.integrable_at_filter_of_tendsto.

theorem measure_theory.integrable_add_of_disjoint {α : Type u_1} {E : Type u_3} {μ : measure_theory.measure α} {f g : α E} (h : )  :
theorem continuous_on.ae_measurable {α : Type u_1} {β : Type u_2} [borel_space β] {f : α β} {s : set α} {μ : measure_theory.measure α} (hf : s) (hs : measurable_set s) :
(μ.restrict s)

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

theorem continuous_on.ae_strongly_measurable_of_is_separable {α : Type u_1} {β : Type u_2} {f : α β} {s : set α} {μ : measure_theory.measure α} (hf : s) (hs : measurable_set s) (h's : topological_space.is_separable s) :

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

theorem continuous_on.ae_strongly_measurable {α : Type u_1} {β : Type u_2} [h : β] {f : α β} {s : set α} {μ : measure_theory.measure α} (hf : s) (hs : measurable_set 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.

theorem continuous_on.ae_strongly_measurable_of_is_compact {α : Type u_1} {β : Type u_2} {f : α β} {s : set α} {μ : measure_theory.measure α} (hf : s) (hs : is_compact s) (h's : measurable_set s) :

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

theorem continuous_on.integrable_at_nhds_within_of_is_separable {α : Type u_1} {E : Type u_3} {μ : measure_theory.measure α} {a : α} {t : set α} {f : α E} (hft : t) (ht : measurable_set t) (h't : topological_space.is_separable t) (ha : a t) :
theorem continuous_on.integrable_at_nhds_within {α : Type u_1} {E : Type u_3} {μ : measure_theory.measure α} {a : α} {t : set α} {f : α E} (hft : t) (ht : measurable_set t) (ha : a t) :
theorem continuous.integrable_at_nhds {α : Type u_1} {E : Type u_3} {μ : measure_theory.measure α} {f : α E} (hf : continuous f) (a : α) :
theorem continuous_on.strongly_measurable_at_filter {α : Type u_1} {β : Type u_2} {f : α β} {s : set α} {μ : measure_theory.measure α} (hs : is_open s) (hf : s) (x : α) (H : x 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 continuous_at.strongly_measurable_at_filter {α : Type u_1} {E : Type u_3} {f : α E} {s : set α} {μ : measure_theory.measure α} (hs : is_open s) (hf : (x : α), x s ) (x : α) (H : x s) :
theorem continuous.strongly_measurable_at_filter {α : Type u_1} {β : Type u_2} {f : α β} (hf : continuous f) (μ : measure_theory.measure α) (l : filter α) :
theorem continuous_on.strongly_measurable_at_filter_nhds_within {α : Type u_1} {β : Type u_2} {f : α β} {s : set α} {μ : measure_theory.measure α} (hf : s) (hs : measurable_set s) (x : α) :
μ

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

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

theorem integrable_on_Icc_iff_integrable_on_Ioc' {α : Type u_1} {E : Type u_3} {f : α E} {μ : measure_theory.measure α} {a b : α} (ha : μ {a} ) :
μ μ
theorem integrable_on_Icc_iff_integrable_on_Ico' {α : Type u_1} {E : Type u_3} {f : α E} {μ : measure_theory.measure α} {a b : α} (hb : μ {b} ) :
μ μ
theorem integrable_on_Ico_iff_integrable_on_Ioo' {α : Type u_1} {E : Type u_3} {f : α E} {μ : measure_theory.measure α} {a b : α} (ha : μ {a} ) :
μ μ
theorem integrable_on_Ioc_iff_integrable_on_Ioo' {α : Type u_1} {E : Type u_3} {f : α E} {μ : measure_theory.measure α} {a b : α} (hb : μ {b} ) :
μ μ
theorem integrable_on_Icc_iff_integrable_on_Ioo' {α : Type u_1} {E : Type u_3} {f : α E} {μ : measure_theory.measure α} {a b : α} (ha : μ {a} ) (hb : μ {b} ) :
μ μ
theorem integrable_on_Ici_iff_integrable_on_Ioi' {α : Type u_1} {E : Type u_3} {f : α E} {μ : measure_theory.measure α} {b : α} (hb : μ {b} ) :
theorem integrable_on_Iic_iff_integrable_on_Iio' {α : Type u_1} {E : Type u_3} {f : α E} {μ : measure_theory.measure α} {b : α} (hb : μ {b} ) :
theorem integrable_on_Icc_iff_integrable_on_Ioc {α : Type u_1} {E : Type u_3} {f : α E} {μ : measure_theory.measure α} {a b : α}  :
μ μ
theorem integrable_on_Icc_iff_integrable_on_Ico {α : Type u_1} {E : Type u_3} {f : α E} {μ : measure_theory.measure α} {a b : α}  :
μ μ
theorem integrable_on_Ico_iff_integrable_on_Ioo {α : Type u_1} {E : Type u_3} {f : α E} {μ : measure_theory.measure α} {a b : α}  :
μ μ
theorem integrable_on_Ioc_iff_integrable_on_Ioo {α : Type u_1} {E : Type u_3} {f : α E} {μ : measure_theory.measure α} {a b : α}  :
μ μ
theorem integrable_on_Icc_iff_integrable_on_Ioo {α : Type u_1} {E : Type u_3} {f : α E} {μ : measure_theory.measure α} {a b : α}  :
μ μ
theorem integrable_on_Ici_iff_integrable_on_Ioi {α : Type u_1} {E : Type u_3} {f : α E} {μ : measure_theory.measure α} {b : α}  :
theorem integrable_on_Iic_iff_integrable_on_Iio {α : Type u_1} {E : Type u_3} {f : α E} {μ : measure_theory.measure α} {b : α}  :