mathlib documentation

measure_theory.integral.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} [measurable_space α] [measurable_space β] (f : α → β) (l : filter α) (μ : measure_theory.measure α . "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
@[simp]
theorem measurable_at_bot {α : Type u_1} {β : Type u_2} [measurable_space α] [measurable_space β] {μ : measure_theory.measure α} {f : α → β} :
theorem measurable_at_filter.eventually {α : Type u_1} {β : Type u_2} [measurable_space α] [measurable_space β] {l : filter α} {f : α → β} {μ : measure_theory.measure α} (h : measurable_at_filter f l μ) :
∀ᶠ (s : set α) in l.lift' set.powerset, ae_measurable f (μ.restrict s)
theorem measurable_at_filter.filter_mono {α : Type u_1} {β : Type u_2} [measurable_space α] [measurable_space β] {l l' : filter α} {f : α → β} {μ : measure_theory.measure α} (h : measurable_at_filter f l μ) (h' : l' l) :
theorem ae_measurable.measurable_at_filter {α : Type u_1} {β : Type u_2} [measurable_space α] [measurable_space β] {l : filter α} {f : α → β} {μ : measure_theory.measure α} (h : ae_measurable f μ) :
theorem ae_measurable.measurable_at_filter_of_mem {α : Type u_1} {β : Type u_2} [measurable_space α] [measurable_space β] {l : filter α} {f : α → β} {μ : measure_theory.measure α} {s : set α} (h : ae_measurable f (μ.restrict s)) (hl : s l) :
theorem measurable.measurable_at_filter {α : Type u_1} {β : Type u_2} [measurable_space α] [measurable_space β] {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} [measurable_space α] [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} [measurable_space α] [normed_group E] [measurable_space E] (f : α → E) (s : set α) (μ : measure_theory.measure α . "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} [measurable_space α] [normed_group E] [measurable_space E] {f : α → E} {s : set α} {μ : measure_theory.measure α} (h : measure_theory.integrable_on f s μ) :
@[simp]
theorem measure_theory.integrable_on_empty {α : Type u_1} {E : Type u_3} [measurable_space α] [normed_group E] [measurable_space E] {f : α → E} {μ : measure_theory.measure α} :
theorem measure_theory.integrable_on_zero {α : Type u_1} {E : Type u_3} [measurable_space α] [normed_group E] [measurable_space 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} [measurable_space α] [normed_group E] [measurable_space 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} [measurable_space α] [normed_group E] [measurable_space E] {f : α → E} {s t : set α} {μ ν : measure_theory.measure α} (h : measure_theory.integrable_on f t ν) (hs : s t) (hμ : μ ν) :
theorem measure_theory.integrable_on.mono_set {α : Type u_1} {E : Type u_3} [measurable_space α] [normed_group E] [measurable_space E] {f : α → E} {s t : set α} {μ : measure_theory.measure α} (h : measure_theory.integrable_on f t μ) (hst : s t) :
theorem measure_theory.integrable_on.mono_measure {α : Type u_1} {E : Type u_3} [measurable_space α] [normed_group E] [measurable_space E] {f : α → E} {s : set α} {μ ν : measure_theory.measure α} (h : measure_theory.integrable_on f s ν) (hμ : μ ν) :
theorem measure_theory.integrable_on.mono_set_ae {α : Type u_1} {E : Type u_3} [measurable_space α] [normed_group E] [measurable_space E] {f : α → E} {s t : set α} {μ : measure_theory.measure α} (h : measure_theory.integrable_on f t μ) (hst : s ≤ᵐ[μ] t) :
theorem measure_theory.integrable_on.congr_set_ae {α : Type u_1} {E : Type u_3} [measurable_space α] [normed_group E] [measurable_space E] {f : α → E} {s t : set α} {μ : measure_theory.measure α} (h : measure_theory.integrable_on f t μ) (hst : s =ᵐ[μ] t) :
theorem measure_theory.integrable.integrable_on {α : Type u_1} {E : Type u_3} [measurable_space α] [normed_group E] [measurable_space E] {f : α → E} {s : set α} {μ : measure_theory.measure α} (h : measure_theory.integrable f μ) :
theorem measure_theory.integrable.integrable_on' {α : Type u_1} {E : Type u_3} [measurable_space α] [normed_group E] [measurable_space E] {f : α → E} {s : set α} {μ : measure_theory.measure α} (h : measure_theory.integrable f (μ.restrict s)) :
theorem measure_theory.integrable_on.restrict {α : Type u_1} {E : Type u_3} [measurable_space α] [normed_group E] [measurable_space E] {f : α → E} {s t : set α} {μ : measure_theory.measure α} (h : measure_theory.integrable_on f s μ) (hs : measurable_set s) :
theorem measure_theory.integrable_on.left_of_union {α : Type u_1} {E : Type u_3} [measurable_space α] [normed_group E] [measurable_space E] {f : α → E} {s t : set α} {μ : measure_theory.measure α} (h : measure_theory.integrable_on f (s t) μ) :
theorem measure_theory.integrable_on.right_of_union {α : Type u_1} {E : Type u_3} [measurable_space α] [normed_group E] [measurable_space E] {f : α → E} {s t : set α} {μ : measure_theory.measure α} (h : measure_theory.integrable_on f (s t) μ) :
theorem measure_theory.integrable_on.union {α : Type u_1} {E : Type u_3} [measurable_space α] [normed_group E] [measurable_space E] {f : α → E} {s t : set α} {μ : measure_theory.measure α} (hs : measure_theory.integrable_on f s μ) (ht : measure_theory.integrable_on f t μ) :
@[simp]
@[simp]
theorem measure_theory.integrable_on_singleton_iff {α : Type u_1} {E : Type u_3} [measurable_space α] [normed_group E] [measurable_space E] {f : α → E} {μ : measure_theory.measure α} {x : α} [measurable_singleton_class α] :
@[simp]
theorem measure_theory.integrable_on_finite_Union {α : Type u_1} {β : Type u_2} {E : Type u_3} [measurable_space α] [normed_group E] [measurable_space E] {f : α → E} {μ : measure_theory.measure α} {s : set β} (hs : s.finite) {t : β → set α} :
measure_theory.integrable_on f (⋃ (i : β) (H : i s), t i) μ ∀ (i : β), i smeasure_theory.integrable_on f (t i) μ
@[simp]
theorem measure_theory.integrable_on_finset_Union {α : Type u_1} {β : Type u_2} {E : Type u_3} [measurable_space α] [normed_group E] [measurable_space E] {f : α → E} {μ : measure_theory.measure α} {s : finset β} {t : β → set α} :
measure_theory.integrable_on f (⋃ (i : β) (H : i s), t i) μ ∀ (i : β), i smeasure_theory.integrable_on f (t i) μ
@[simp]
theorem measure_theory.integrable_on_fintype_Union {α : Type u_1} {β : Type u_2} {E : Type u_3} [measurable_space α] [normed_group E] [measurable_space E] {f : α → E} {μ : measure_theory.measure α} [fintype β] {t : β → set α} :
measure_theory.integrable_on f (⋃ (i : β), t i) μ ∀ (i : β), measure_theory.integrable_on f (t i) μ
theorem measure_theory.integrable_on.add_measure {α : Type u_1} {E : Type u_3} [measurable_space α] [normed_group E] [measurable_space E] {f : α → E} {s : set α} {μ ν : measure_theory.measure α} (hμ : measure_theory.integrable_on f s μ) (hν : measure_theory.integrable_on f s ν) :
@[simp]
theorem measure_theory.integrable_on_map_equiv {α : Type u_1} {β : Type u_2} {E : Type u_3} [measurable_space α] [normed_group E] [measurable_space E] [measurable_space β] (e : α ≃ᵐ β) {f : β → E} {μ : measure_theory.measure α} {s : set β} :
theorem measure_theory.integrable_on.indicator {α : Type u_1} {E : Type u_3} [measurable_space α] [normed_group E] [measurable_space E] {f : α → E} {s : set α} {μ : measure_theory.measure α} (h : measure_theory.integrable_on f s μ) (hs : measurable_set s) :
theorem measure_theory.integrable.indicator {α : Type u_1} {E : Type u_3} [measurable_space α] [normed_group E] [measurable_space E] {f : α → E} {s : set α} {μ : measure_theory.measure α} (h : measure_theory.integrable f μ) (hs : measurable_set s) :
def measure_theory.integrable_at_filter {α : Type u_1} {E : Type u_3} [measurable_space α] [normed_group E] [measurable_space E] (f : α → E) (l : filter α) (μ : measure_theory.measure α . "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
theorem measure_theory.integrable_at_filter.eventually {α : Type u_1} {E : Type u_3} [measurable_space α] [normed_group E] [measurable_space E] {f : α → E} {μ : measure_theory.measure α} {l : filter α} (h : measure_theory.integrable_at_filter f l μ) :
∀ᶠ (s : set α) in l.lift' set.powerset, measure_theory.integrable_on f s μ
theorem measure_theory.integrable_at_filter.filter_mono {α : Type u_1} {E : Type u_3} [measurable_space α] [normed_group E] [measurable_space E] {f : α → E} {μ : measure_theory.measure α} {l l' : filter α} (hl : l l') (hl' : measure_theory.integrable_at_filter f l' μ) :

Alias of integrable_at_filter.inf_ae_iff.

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

Alias of measure.finite_at_filter.integrable_at_filter_of_tendsto_ae.

theorem filter.tendsto.integrable_at_filter {α : Type u_1} {E : Type u_3} [measurable_space α] [normed_group E] [measurable_space E] {f : α → E} {μ : measure_theory.measure α} {l : filter α} [l.is_measurably_generated] (hfm : measurable_at_filter f l μ) (hμ : μ.finite_at_filter l) {b : E} (hf : filter.tendsto f l (𝓝 b)) :

Alias of measure.finite_at_filter.integrable_at_filter_of_tendsto.

theorem is_compact.integrable_on_of_nhds_within {α : Type u_1} {E : Type u_3} [measurable_space α] [measurable_space E] [normed_group E] [topological_space α] {μ : measure_theory.measure α} {s : set α} (hs : is_compact s) {f : α → E} (hf : ∀ (x : α), x smeasure_theory.integrable_at_filter f (𝓝[s] x) μ) :

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} {β : Type u_2} [measurable_space α] [topological_space α] [opens_measurable_space α] [measurable_space β] [topological_space β] [borel_space β] {f : α → β} {s : set α} {μ : measure_theory.measure α} (hf : continuous_on f s) (hs : measurable_set s) :

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

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

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

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

theorem measure_theory.integrable_on.mul_continuous_on_of_subset {α : Type u_1} [measurable_space α] [topological_space α] [opens_measurable_space α] {μ : measure_theory.measure α} {s t : set α} {f g : α → } (hf : measure_theory.integrable_on f s μ) (hg : continuous_on g t) (hs : measurable_set s) (ht : is_compact t) (hst : s t) :
measure_theory.integrable_on (λ (x : α), (f x) * g x) s μ
theorem measure_theory.integrable_on.mul_continuous_on {α : Type u_1} [measurable_space α] [topological_space α] [opens_measurable_space α] {μ : measure_theory.measure α} {s : set α} {f g : α → } [t2_space α] (hf : measure_theory.integrable_on f s μ) (hg : continuous_on g s) (hs : is_compact s) :
measure_theory.integrable_on (λ (x : α), (f x) * g x) s μ
theorem measure_theory.integrable_on.continuous_on_mul_of_subset {α : Type u_1} [measurable_space α] [topological_space α] [opens_measurable_space α] {μ : measure_theory.measure α} {s t : set α} {f g : α → } (hf : measure_theory.integrable_on f s μ) (hg : continuous_on g t) (hs : measurable_set s) (ht : is_compact t) (hst : s t) :
measure_theory.integrable_on (λ (x : α), (g x) * f x) s μ
theorem measure_theory.integrable_on.continuous_on_mul {α : Type u_1} [measurable_space α] [topological_space α] [opens_measurable_space α] {μ : measure_theory.measure α} {s : set α} {f g : α → } [t2_space α] (hf : measure_theory.integrable_on f s μ) (hg : continuous_on g s) (hs : is_compact s) :
measure_theory.integrable_on (λ (x : α), (g x) * f x) s μ