mathlib3 documentation

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} [measurable_space α] [topological_space β] (f : α β) (l : filter α) (μ : measure_theory.measure α . "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]
@[protected]
theorem strongly_measurable_at_filter.filter_mono {α : Type u_1} {β : Type u_2} [measurable_space α] [topological_space β] {l l' : filter α} {f : α β} {μ : measure_theory.measure α} (h : strongly_measurable_at_filter f l μ) (h' : l' l) :
theorem measure_theory.has_finite_integral_restrict_of_bounded {α : Type u_1} {E : Type u_3} [measurable_space α] [normed_add_comm_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_add_comm_group E] (f : α E) (s : set α) (μ : measure_theory.measure α . "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_zero {α : Type u_1} {E : Type u_3} [measurable_space α] [normed_add_comm_group E] {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} [measurable_space α] [normed_add_comm_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} [measurable_space α] [normed_add_comm_group 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_add_comm_group 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_add_comm_group E] {f : α E} {s : set α} {μ ν : measure_theory.measure α} (h : measure_theory.integrable_on f s ν) (hμ : μ ν) :
@[simp]
theorem measure_theory.integrable_on_finite_bUnion {α : Type u_1} {β : Type u_2} {E : Type u_3} [measurable_space α] [normed_add_comm_group 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 s measure_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_add_comm_group E] {f : α E} {μ : measure_theory.measure α} {s : finset β} {t : β set α} :
measure_theory.integrable_on f ( (i : β) (H : i s), t i) μ (i : β), i s measure_theory.integrable_on f (t i) μ
@[simp]
theorem measure_theory.integrable_on_finite_Union {α : Type u_1} {β : Type u_2} {E : Type u_3} [measurable_space α] [normed_add_comm_group E] {f : α E} {μ : measure_theory.measure α} [finite β] {t : β set α} :
measure_theory.integrable_on f ( (i : β), t i) μ (i : β), measure_theory.integrable_on f (t i) μ
theorem measure_theory.integrable_on.restrict_to_measurable {α : Type u_1} {E : Type u_3} [measurable_space α] [normed_add_comm_group E] {f : α E} {s : set α} {μ : measure_theory.measure α} (hf : measure_theory.integrable_on f s μ) (h's : (x : α), x s f x 0) :

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} [measurable_space α] [normed_add_comm_group E] {f : α E} {s t : set α} {μ : measure_theory.measure α} (hf : measure_theory.integrable_on f s μ) (ht : measure_theory.null_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 null-measurable.

theorem measure_theory.integrable_on.of_forall_diff_eq_zero {α : Type u_1} {E : Type u_3} [measurable_space α] [normed_add_comm_group E] {f : α E} {s t : set α} {μ : measure_theory.measure α} (hf : measure_theory.integrable_on f s μ) (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.

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

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

def measure_theory.integrable_at_filter {α : Type u_1} {E : Type u_3} [measurable_space α] [normed_add_comm_group 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.small_sets.

Equations

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

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 [has_no_atoms μ].