# mathlibdocumentation

measure_theory.integrable_on

# Functions integrable on a set and at a filter #

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 measurable_at_filter {α : Type u_1} {β : Type u_2} (f : α → β) (l : filter α) (μ : . "volume_tac") :
Prop

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

Equations
• μ = ∃ (s : set α) (H : s l),
@[simp]
theorem measurable_at_bot {α : Type u_1} {β : Type u_2} {μ : measure_theory.measure α} {f : α → β} :
theorem measurable_at_filter.eventually {α : Type u_1} {β : Type u_2} {l : filter α} {f : α → β} {μ : measure_theory.measure α} (h : μ) :
∀ᶠ (s : set α) in , (μ.restrict s)
theorem measurable_at_filter.filter_mono {α : Type u_1} {β : Type u_2} {l l' : filter α} {f : α → β} {μ : measure_theory.measure α} (h : μ) (h' : l' l) :
μ
theorem ae_measurable.measurable_at_filter {α : Type u_1} {β : Type u_2} {l : filter α} {f : α → β} {μ : measure_theory.measure α} (h : μ) :
μ
theorem ae_measurable.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) :
μ
theorem measurable.measurable_at_filter {α : Type u_1} {β : Type u_2} {l : filter α} {f : α → β} {μ : measure_theory.measure α} (h : measurable f) :
μ
theorem measure_theory.has_finite_integral_restrict_of_bounded {α : Type u_1} {E : Type u_3} [normed_group E] {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} [normed_group E] (f : α → E) (s : set α) (μ : . "volume_tac") :
Prop

A function is integrable_on a set s if it is almost everywhere 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} [normed_group E] {f : α → E} {s : set α} {μ : measure_theory.measure α} (h : μ) :
@[simp]
theorem measure_theory.integrable_on_empty {α : Type u_1} {E : Type u_3} [normed_group E] {f : α → E} {μ : measure_theory.measure α} :
@[simp]
theorem measure_theory.integrable_on_univ {α : Type u_1} {E : Type u_3} [normed_group E] {f : α → E} {μ : measure_theory.measure α} :
theorem measure_theory.integrable_on_zero {α : Type u_1} {E : Type u_3} [normed_group E] {s : set α} {μ : measure_theory.measure α} :
measure_theory.integrable_on (λ (_x : α), 0) s μ
theorem measure_theory.integrable_on_const {α : Type u_1} {E : Type u_3} [normed_group E] {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} [normed_group E] {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} [normed_group E] {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} [normed_group E] {f : α → E} {s : set α} {μ ν : measure_theory.measure α} (h : ν) (hμ : μ ν) :
theorem measure_theory.integrable_on.mono_set_ae {α : Type u_1} {E : Type u_3} [normed_group E] {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} [normed_group E] {f : α → E} {s t : set α} {μ : measure_theory.measure α} (h : μ) (hst : s =ᵐ[μ] t) :
theorem measure_theory.integrable.integrable_on {α : Type u_1} {E : Type u_3} [normed_group E] {f : α → E} {s : set α} {μ : measure_theory.measure α} (h : μ) :
theorem measure_theory.integrable.integrable_on' {α : Type u_1} {E : Type u_3} [normed_group E] {f : α → E} {s : set α} {μ : measure_theory.measure α} (h : (μ.restrict s)) :
theorem measure_theory.integrable_on.restrict {α : Type u_1} {E : Type u_3} [normed_group E] {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} [normed_group E] {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} [normed_group E] {f : α → E} {s t : set α} {μ : measure_theory.measure α} (h : (s t) μ) :
theorem measure_theory.integrable_on.union {α : Type u_1} {E : Type u_3} [normed_group E] {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} [normed_group E] {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} [normed_group E] {f : α → E} {μ : measure_theory.measure α} {x : α}  :
μ f x = 0 μ {x} <
@[simp]
theorem measure_theory.integrable_on_finite_union {α : Type u_1} {β : Type u_2} {E : Type u_3} [normed_group E] {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} [normed_group E] {f : α → E} {μ : measure_theory.measure α} {s : finset β} {t : β → set α} :
(⋃ (i : β) (H : i s), t i) μ ∀ (i : β), i s (t i) μ
theorem measure_theory.integrable_on.add_measure {α : Type u_1} {E : Type u_3} [normed_group E] {f : α → E} {s : set α} {μ ν : measure_theory.measure α} (hμ : μ) (hν : ν) :
+ ν)
@[simp]
theorem measure_theory.integrable_on_add_measure {α : Type u_1} {E : Type u_3} [normed_group E] {f : α → E} {s : set α} {μ ν : measure_theory.measure α} :
+ ν)
theorem measure_theory.integrable_indicator_iff {α : Type u_1} {E : Type u_3} [normed_group E] {f : α → E} {s : set α} {μ : measure_theory.measure α} (hs : measurable_set s) :
theorem measure_theory.integrable_on.indicator {α : Type u_1} {E : Type u_3} [normed_group E] {f : α → E} {s : set α} {μ : measure_theory.measure α} (h : μ) (hs : measurable_set s) :
theorem measure_theory.integrable.indicator {α : Type u_1} {E : Type u_3} [normed_group E] {f : α → E} {s : set α} {μ : measure_theory.measure α} (h : μ) (hs : measurable_set s) :
theorem measure_theory.integrable_indicator_const_Lp {α : Type u_1} {μ : measure_theory.measure α} {E : Type u_2} [normed_group E] [borel_space E] {p : ℝ≥0∞} {s : set α} (hs : measurable_set s) (hμs : μ s ) (c : E) :
μ
theorem measure_theory.integrable_on_Lp_of_measure_ne_top {α : Type u_1} {μ : measure_theory.measure α} {E : Type u_2} [normed_group E] [borel_space E] {p : ℝ≥0∞} {s : set α} (f : μ)) (hp : 1 p) (hμs : μ s ) :
def measure_theory.integrable_at_filter {α : Type u_1} {E : Type u_3} [normed_group E] (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.lift' powerset.

Equations
• = ∃ (s : set α) (H : s l),
theorem measure_theory.integrable_at_filter.eventually {α : Type u_1} {E : Type u_3} [normed_group E] {f : α → E} {μ : measure_theory.measure α} {l : filter α} (h : μ) :
∀ᶠ (s : set α) in ,
theorem measure_theory.integrable_at_filter.filter_mono {α : Type u_1} {E : Type u_3} [normed_group E] {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} [normed_group E] {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} [normed_group E] {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} [normed_group E] {f : α → E} {μ : measure_theory.measure α} {l : filter α} :
theorem measure_theory.integrable_at_filter.of_inf_ae {α : Type u_1} {E : Type u_3} [normed_group E] {f : α → E} {μ : measure_theory.measure α} {l : filter α} :
μ

Alias of integrable_at_filter.inf_ae_iff.

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

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

Alias of 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} [normed_group E] {f : α → E} {μ : measure_theory.measure α} {l : filter α} (hfm : μ) (hμ : μ.finite_at_filter l) {b : E} (hf : (𝓝 b)) :
theorem filter.tendsto.integrable_at_filter {α : Type u_1} {E : Type u_3} [normed_group E] {f : α → E} {μ : measure_theory.measure α} {l : filter α} (hfm : μ) (hμ : μ.finite_at_filter l) {b : E} (hf : (𝓝 b)) :

Alias of measure.finite_at_filter.integrable_at_filter_of_tendsto.

theorem measure_theory.integrable_add_of_disjoint {α : Type u_1} {E : Type u_3} [normed_group E] {μ : measure_theory.measure α} [borel_space E] {f g : α → E} (h : ) (hf : measurable f) (hg : measurable g) :
theorem is_compact.integrable_on_of_nhds_within {α : Type u_1} {E : Type u_3} [normed_group E] {μ : measure_theory.measure α} {s : set α} (hs : is_compact s) {f : α → E} (hf : ∀ (x : α), x s) :

If a function is integrable at 𝓝[s] x for each point x of a compact set s, then it is integrable on s.

theorem continuous_on.ae_measurable {α : Type u_1} {E : Type u_3} [normed_group E] [borel_space E] {f : α → E} {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.integrable_at_nhds_within {α : Type u_1} {E : Type u_3} [normed_group E] [borel_space E] {μ : measure_theory.measure α} {a : α} {t : set α} {f : α → E} (hft : t) (ht : measurable_set t) (ha : a t) :
theorem continuous_on.integrable_on_compact {α : Type u_1} {E : Type u_3} [normed_group E] [borel_space E] [t2_space α] {μ : measure_theory.measure α} {s : set α} (hs : is_compact s) {f : α → E} (hf : s) :

A function f continuous on a compact set s is integrable on this set with respect to any locally finite measure.

theorem continuous_on.integrable_on_Icc {β : Type u_2} {E : Type u_3} [normed_group E] [borel_space E] {μ : measure_theory.measure β} {a b : β} {f : β → E} (hf : (set.Icc a b)) :
μ
theorem continuous_on.integrable_on_interval {β : Type u_2} {E : Type u_3} [normed_group E] [borel_space E] {μ : measure_theory.measure β} {a b : β} {f : β → E} (hf : b)) :
μ
theorem continuous.integrable_on_compact {α : Type u_1} {E : Type u_3} [normed_group E] [t2_space α] [borel_space E] {μ : measure_theory.measure α} {s : set α} (hs : is_compact s) {f : α → E} (hf : continuous f) :

A continuous function f is integrable on any compact set with respect to any locally finite measure.

theorem continuous.integrable_on_Icc {β : Type u_2} {E : Type u_3} [normed_group E] [borel_space E] {μ : measure_theory.measure β} {a b : β} {f : β → E} (hf : continuous f) :
μ
theorem continuous.integrable_on_interval {β : Type u_2} {E : Type u_3} [normed_group E] [borel_space E] {μ : measure_theory.measure β} {a b : β} {f : β → E} (hf : continuous f) :
μ
theorem continuous.integrable_of_compact_closure_support {α : Type u_1} {E : Type u_3} [normed_group E] [t2_space α] [borel_space E] {μ : measure_theory.measure α} {f : α → E} (hf : continuous f) (hfc : is_compact (closure (function.support f))) :

A continuous function with compact closure of the support is integrable on the whole space.

theorem measure_theory.integrable_on.mul_continuous_on {α : Type u_1} [t2_space α] {μ : measure_theory.measure α} {s : set α} {f g : α → } (hf : μ) (hg : s) (hs : is_compact s) :
measure_theory.integrable_on (λ (x : α), (f x) * g x) s μ
theorem measure_theory.integrable_on.continuous_on_mul {α : Type u_1} [t2_space α] {μ : measure_theory.measure α} {s : set α} {f g : α → } (hf : μ) (hg : s) (hs : is_compact s) :
measure_theory.integrable_on (λ (x : α), (g x) * f x) s μ
theorem integrable_on_compact_of_monotone_on {α : Type u_1} {E : Type u_3} [normed_group E] [borel_space α] [borel_space E] {μ : measure_theory.measure α} {s : set α} (hs : is_compact s) {f : α → E} (hmono : ∀ ⦃x y : α⦄, x sy sx yf x f y) :
theorem integrable_on_compact_of_antimono_on {α : Type u_1} {E : Type u_3} [normed_group E] [borel_space α] [borel_space E] {μ : measure_theory.measure α} {s : set α} (hs : is_compact s) {f : α → E} (hmono : ∀ ⦃x y : α⦄, x sy sx yf y f x) :
theorem integrable_on_compact_of_monotone {α : Type u_1} {E : Type u_3} [normed_group E] [borel_space α] [borel_space E] {μ : measure_theory.measure α} {s : set α} (hs : is_compact s) {f : α → E} (hmono : monotone f) :
theorem monotone.integrable_on_compact {α : Type u_1} {E : Type u_3} [normed_group E] [borel_space α] [borel_space E] {μ : measure_theory.measure α} {s : set α} (hs : is_compact s) {f : α → E} (hmono : monotone f) :

Alias of integrable_on_compact_of_monotone.

theorem integrable_on_compact_of_antimono {α : Type u_1} {E : Type u_3} [normed_group E] [borel_space α] [borel_space E] {μ : measure_theory.measure α} {s : set α} (hs : is_compact s) {f : α → E} (hmono : ∀ ⦃x y : α⦄, x yf y f x) :