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
- strongly_measurable_at_filter f l μ = ∃ (s : set α) (H : s ∈ l), measure_theory.ae_strongly_measurable f (measure_theory.measure.restrict μ s)
@[simp]
theorem
strongly_measurable_at_bot
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
[topological_space β]
{μ : measure_theory.measure α}
{f : α → β} :
@[protected]
theorem
strongly_measurable_at_filter.eventually
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
[topological_space β]
{l : filter α}
{f : α → β}
{μ : measure_theory.measure α}
(h : strongly_measurable_at_filter f l μ) :
∀ᶠ (s : set α) in l.small_sets, measure_theory.ae_strongly_measurable f (μ.restrict s)
@[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) :
@[protected]
theorem
measure_theory.ae_strongly_measurable.strongly_measurable_at_filter
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
[topological_space β]
{l : filter α}
{f : α → β}
{μ : measure_theory.measure α}
(h : measure_theory.ae_strongly_measurable f μ) :
theorem
ae_strongly_measurable.strongly_measurable_at_filter_of_mem
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
[topological_space β]
{l : filter α}
{f : α → β}
{μ : measure_theory.measure α}
{s : set α}
(h : measure_theory.ae_strongly_measurable f (μ.restrict s))
(hl : s ∈ l) :
@[protected]
theorem
measure_theory.strongly_measurable.strongly_measurable_at_filter
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
[topological_space β]
{l : filter α}
{f : α → β}
{μ : measure_theory.measure α}
(h : measure_theory.strongly_measurable f) :
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.integrable
{α : 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 μ) :
measure_theory.integrable f (μ.restrict s)
@[simp]
theorem
measure_theory.integrable_on_empty
{α : Type u_1}
{E : Type u_3}
[measurable_space α]
[normed_add_comm_group E]
{f : α → E}
{μ : measure_theory.measure α} :
@[simp]
theorem
measure_theory.integrable_on_univ
{α : Type u_1}
{E : Type u_3}
[measurable_space α]
[normed_add_comm_group E]
{f : α → E}
{μ : measure_theory.measure α} :
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} :
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μ : μ ≤ ν) :
theorem
measure_theory.integrable_on.mono_set_ae
{α : 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.congr_set_ae
{α : 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.congr_fun_ae
{α : Type u_1}
{E : Type u_3}
[measurable_space α]
[normed_add_comm_group E]
{f g : α → E}
{s : set α}
{μ : measure_theory.measure α}
(h : measure_theory.integrable_on f s μ)
(hst : f =ᵐ[μ.restrict s] g) :
theorem
measure_theory.integrable_on_congr_fun_ae
{α : Type u_1}
{E : Type u_3}
[measurable_space α]
[normed_add_comm_group E]
{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}
[measurable_space α]
[normed_add_comm_group E]
{f g : α → E}
{s : set α}
{μ : measure_theory.measure α}
(h : measure_theory.integrable_on f s μ)
(hst : set.eq_on f g s)
(hs : measurable_set s) :
theorem
measure_theory.integrable_on_congr_fun
{α : Type u_1}
{E : Type u_3}
[measurable_space α]
[normed_add_comm_group E]
{f g : α → E}
{s : set α}
{μ : measure_theory.measure α}
(hst : set.eq_on f g s)
(hs : measurable_set s) :
theorem
measure_theory.integrable.integrable_on
{α : 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 f μ) :
theorem
measure_theory.integrable_on.restrict
{α : 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 s μ)
(hs : measurable_set s) :
measure_theory.integrable_on f s (μ.restrict t)
theorem
measure_theory.integrable_on.left_of_union
{α : 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 (s ∪ t) μ) :
theorem
measure_theory.integrable_on.right_of_union
{α : 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 (s ∪ t) μ) :
theorem
measure_theory.integrable_on.union
{α : Type u_1}
{E : Type u_3}
[measurable_space α]
[normed_add_comm_group E]
{f : α → E}
{s t : set α}
{μ : measure_theory.measure α}
(hs : measure_theory.integrable_on f s μ)
(ht : measure_theory.integrable_on f t μ) :
measure_theory.integrable_on f (s ∪ t) μ
@[simp]
theorem
measure_theory.integrable_on_union
{α : Type u_1}
{E : Type u_3}
[measurable_space α]
[normed_add_comm_group E]
{f : α → E}
{s t : set α}
{μ : measure_theory.measure α} :
measure_theory.integrable_on f (s ∪ t) μ ↔ measure_theory.integrable_on f s μ ∧ measure_theory.integrable_on f t μ
@[simp]
theorem
measure_theory.integrable_on_singleton_iff
{α : Type u_1}
{E : Type u_3}
[measurable_space α]
[normed_add_comm_group E]
{f : α → E}
{μ : measure_theory.measure α}
{x : α}
[measurable_singleton_class α] :
@[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.add_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ν : measure_theory.integrable_on f s ν) :
measure_theory.integrable_on f s (μ + ν)
@[simp]
theorem
measure_theory.integrable_on_add_measure
{α : Type u_1}
{E : Type u_3}
[measurable_space α]
[normed_add_comm_group E]
{f : α → E}
{s : set α}
{μ ν : measure_theory.measure α} :
measure_theory.integrable_on f s (μ + ν) ↔ measure_theory.integrable_on f s μ ∧ measure_theory.integrable_on f s ν
theorem
measurable_embedding.integrable_on_map_iff
{α : Type u_1}
{β : Type u_2}
{E : Type u_3}
[measurable_space α]
[normed_add_comm_group E]
[measurable_space β]
{e : α → β}
(he : measurable_embedding e)
{f : β → E}
{μ : measure_theory.measure α}
{s : set β} :
measure_theory.integrable_on f s (measure_theory.measure.map e μ) ↔ measure_theory.integrable_on (f ∘ e) (e ⁻¹' s) μ
theorem
measure_theory.integrable_on_map_equiv
{α : Type u_1}
{β : Type u_2}
{E : Type u_3}
[measurable_space α]
[normed_add_comm_group E]
[measurable_space β]
(e : α ≃ᵐ β)
{f : β → E}
{μ : measure_theory.measure α}
{s : set β} :
measure_theory.integrable_on f s (measure_theory.measure.map ⇑e μ) ↔ measure_theory.integrable_on (f ∘ ⇑e) (⇑e ⁻¹' s) μ
theorem
measure_theory.measure_preserving.integrable_on_comp_preimage
{α : Type u_1}
{β : Type u_2}
{E : Type u_3}
[measurable_space α]
[normed_add_comm_group E]
{μ : measure_theory.measure α}
[measurable_space β]
{e : α → β}
{ν : measure_theory.measure β . "volume_tac"}
(h₁ : measure_theory.measure_preserving e μ ν)
(h₂ : measurable_embedding e)
{f : β → E}
{s : set β} :
measure_theory.integrable_on (f ∘ e) (e ⁻¹' s) μ ↔ measure_theory.integrable_on f s ν
theorem
measure_theory.measure_preserving.integrable_on_image
{α : Type u_1}
{β : Type u_2}
{E : Type u_3}
[measurable_space α]
[normed_add_comm_group E]
{μ : measure_theory.measure α}
[measurable_space β]
{e : α → β}
{ν : measure_theory.measure β . "volume_tac"}
(h₁ : measure_theory.measure_preserving e μ ν)
(h₂ : measurable_embedding e)
{f : β → E}
{s : set α} :
measure_theory.integrable_on f (e '' s) ν ↔ measure_theory.integrable_on (f ∘ e) s μ
theorem
measure_theory.integrable_indicator_iff
{α : Type u_1}
{E : Type u_3}
[measurable_space α]
[normed_add_comm_group E]
{f : α → E}
{s : set α}
{μ : measure_theory.measure α}
(hs : measurable_set s) :
measure_theory.integrable (s.indicator f) μ ↔ measure_theory.integrable_on f s μ
theorem
measure_theory.integrable_on.integrable_indicator
{α : 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 μ)
(hs : measurable_set s) :
measure_theory.integrable (s.indicator f) μ
theorem
measure_theory.integrable.indicator
{α : 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 f μ)
(hs : measurable_set s) :
measure_theory.integrable (s.indicator f) μ
theorem
measure_theory.integrable_on.indicator
{α : 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 s μ)
(ht : measurable_set t) :
measure_theory.integrable_on (t.indicator f) s μ
theorem
measure_theory.integrable_indicator_const_Lp
{α : Type u_1}
[measurable_space α]
{μ : measure_theory.measure α}
{E : Type u_2}
[normed_add_comm_group E]
{p : ennreal}
{s : set α}
(hs : measurable_set s)
(hμs : ⇑μ s ≠ ⊤)
(c : E) :
measure_theory.integrable ⇑(measure_theory.indicator_const_Lp p hs hμs c) μ
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) :
μ.restrict (measure_theory.to_measurable μ s) = μ.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}
[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.
theorem
measure_theory.integrable_on.integrable_of_ae_not_mem_eq_zero
{α : 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'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}
[measurable_space α]
[normed_add_comm_group E]
{f : α → E}
{s : set α}
{μ : measure_theory.measure α}
(hf : measure_theory.integrable_on f s μ)
(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}
[measurable_space α]
[normed_add_comm_group E]
{f : α → E}
{s : set α}
{μ : measure_theory.measure α}
(h1s : function.support f ⊆ s) :
theorem
measure_theory.integrable_on_Lp_of_measure_ne_top
{α : Type u_1}
[measurable_space α]
{μ : measure_theory.measure α}
{E : Type u_2}
[normed_add_comm_group E]
{p : ennreal}
{s : set α}
(f : ↥(measure_theory.Lp E p μ))
(hp : 1 ≤ p)
(hμs : ⇑μ s ≠ ⊤) :
theorem
measure_theory.integrable.lintegral_lt_top
{α : Type u_1}
[measurable_space α]
{μ : measure_theory.measure α}
{f : α → ℝ}
(hf : measure_theory.integrable f μ) :
theorem
measure_theory.integrable_on.set_lintegral_lt_top
{α : Type u_1}
[measurable_space α]
{μ : measure_theory.measure α}
{f : α → ℝ}
{s : set α}
(hf : measure_theory.integrable_on f s μ) :
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
- measure_theory.integrable_at_filter f l μ = ∃ (s : set α) (H : s ∈ l), measure_theory.integrable_on f s μ
theorem
measure_theory.integrable.integrable_at_filter
{α : Type u_1}
{E : Type u_3}
[measurable_space α]
[normed_add_comm_group E]
{f : α → E}
{μ : measure_theory.measure α}
(h : measure_theory.integrable f μ)
(l : filter α) :
@[protected]
theorem
measure_theory.integrable_at_filter.eventually
{α : Type u_1}
{E : Type u_3}
[measurable_space α]
[normed_add_comm_group E]
{f : α → E}
{μ : measure_theory.measure α}
{l : filter α}
(h : measure_theory.integrable_at_filter f l μ) :
∀ᶠ (s : set α) in l.small_sets, measure_theory.integrable_on f s μ
theorem
measure_theory.integrable_at_filter.filter_mono
{α : Type u_1}
{E : Type u_3}
[measurable_space α]
[normed_add_comm_group E]
{f : α → E}
{μ : measure_theory.measure α}
{l l' : filter α}
(hl : l ≤ l')
(hl' : measure_theory.integrable_at_filter f l' μ) :
theorem
measure_theory.integrable_at_filter.inf_of_left
{α : Type u_1}
{E : Type u_3}
[measurable_space α]
[normed_add_comm_group E]
{f : α → E}
{μ : measure_theory.measure α}
{l l' : filter α}
(hl : measure_theory.integrable_at_filter f l μ) :
measure_theory.integrable_at_filter f (l ⊓ l') μ
theorem
measure_theory.integrable_at_filter.inf_of_right
{α : Type u_1}
{E : Type u_3}
[measurable_space α]
[normed_add_comm_group E]
{f : α → E}
{μ : measure_theory.measure α}
{l l' : filter α}
(hl : measure_theory.integrable_at_filter f l μ) :
measure_theory.integrable_at_filter f (l' ⊓ l) μ
@[simp]
theorem
measure_theory.integrable_at_filter.inf_ae_iff
{α : Type u_1}
{E : Type u_3}
[measurable_space α]
[normed_add_comm_group E]
{f : α → E}
{μ : measure_theory.measure α}
{l : filter α} :
measure_theory.integrable_at_filter f (l ⊓ μ.ae) μ ↔ measure_theory.integrable_at_filter f l μ
theorem
measure_theory.integrable_at_filter.of_inf_ae
{α : Type u_1}
{E : Type u_3}
[measurable_space α]
[normed_add_comm_group E]
{f : α → E}
{μ : measure_theory.measure α}
{l : filter α} :
measure_theory.integrable_at_filter f (l ⊓ μ.ae) μ → measure_theory.integrable_at_filter f l μ
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}
[measurable_space α]
[normed_add_comm_group E]
{f : α → E}
{μ : measure_theory.measure α}
{l : filter α}
[l.is_measurably_generated]
(hfm : strongly_measurable_at_filter f l μ)
(hμ : μ.finite_at_filter l)
(hf : filter.is_bounded_under has_le.le l (has_norm.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}
[measurable_space α]
[normed_add_comm_group E]
{f : α → E}
{μ : measure_theory.measure α}
{l : filter α}
[l.is_measurably_generated]
(hfm : strongly_measurable_at_filter f l μ)
(hμ : μ.finite_at_filter l)
{b : E}
(hf : filter.tendsto f (l ⊓ μ.ae) (nhds b)) :
theorem
filter.tendsto.integrable_at_filter_ae
{α : Type u_1}
{E : Type u_3}
[measurable_space α]
[normed_add_comm_group E]
{f : α → E}
{μ : measure_theory.measure α}
{l : filter α}
[l.is_measurably_generated]
(hfm : strongly_measurable_at_filter f l μ)
(hμ : μ.finite_at_filter l)
{b : E}
(hf : filter.tendsto f (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}
[measurable_space α]
[normed_add_comm_group E]
{f : α → E}
{μ : measure_theory.measure α}
{l : filter α}
[l.is_measurably_generated]
(hfm : strongly_measurable_at_filter f l μ)
(hμ : μ.finite_at_filter l)
{b : E}
(hf : filter.tendsto f l (nhds b)) :
theorem
filter.tendsto.integrable_at_filter
{α : Type u_1}
{E : Type u_3}
[measurable_space α]
[normed_add_comm_group E]
{f : α → E}
{μ : measure_theory.measure α}
{l : filter α}
[l.is_measurably_generated]
(hfm : strongly_measurable_at_filter f l μ)
(hμ : μ.finite_at_filter l)
{b : E}
(hf : filter.tendsto f l (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}
[measurable_space α]
[normed_add_comm_group E]
{μ : measure_theory.measure α}
{f g : α → E}
(h : disjoint (function.support f) (function.support g))
(hf : measure_theory.strongly_measurable f)
(hg : measure_theory.strongly_measurable g) :
measure_theory.integrable (f + g) μ ↔ measure_theory.integrable f μ ∧ measure_theory.integrable g μ
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) :
ae_measurable f (μ.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}
[measurable_space α]
[topological_space α]
[topological_space.pseudo_metrizable_space α]
[opens_measurable_space α]
[topological_space β]
[topological_space.pseudo_metrizable_space β]
{f : α → β}
{s : set α}
{μ : measure_theory.measure α}
(hf : continuous_on f 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}
[measurable_space α]
[topological_space α]
[topological_space β]
[h : second_countable_topology_either α β]
[opens_measurable_space α]
[topological_space.pseudo_metrizable_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 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}
[measurable_space α]
[topological_space α]
[opens_measurable_space α]
[topological_space β]
[topological_space.pseudo_metrizable_space β]
{f : α → β}
{s : set α}
{μ : measure_theory.measure α}
(hf : continuous_on f 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}
[measurable_space α]
[normed_add_comm_group E]
[topological_space α]
[topological_space.pseudo_metrizable_space α]
[opens_measurable_space α]
{μ : measure_theory.measure α}
[measure_theory.is_locally_finite_measure μ]
{a : α}
{t : set α}
{f : α → E}
(hft : continuous_on f 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}
[measurable_space α]
[normed_add_comm_group E]
[topological_space α]
[second_countable_topology_either α E]
[opens_measurable_space α]
{μ : measure_theory.measure α}
[measure_theory.is_locally_finite_measure μ]
{a : α}
{t : set α}
{f : α → E}
(hft : continuous_on f t)
(ht : measurable_set t)
(ha : a ∈ t) :
theorem
continuous.integrable_at_nhds
{α : Type u_1}
{E : Type u_3}
[measurable_space α]
[normed_add_comm_group E]
[topological_space α]
[second_countable_topology_either α E]
[opens_measurable_space α]
{μ : measure_theory.measure α}
[measure_theory.is_locally_finite_measure μ]
{f : α → E}
(hf : continuous f)
(a : α) :
theorem
continuous_on.strongly_measurable_at_filter
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
[topological_space α]
[opens_measurable_space α]
[topological_space β]
[topological_space.pseudo_metrizable_space β]
[second_countable_topology_either α β]
{f : α → β}
{s : set α}
{μ : measure_theory.measure α}
(hs : is_open s)
(hf : continuous_on f s)
(x : α)
(H : x ∈ s) :
strongly_measurable_at_filter f (nhds x) μ
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}
[measurable_space α]
[normed_add_comm_group E]
[topological_space α]
[opens_measurable_space α]
[second_countable_topology_either α E]
{f : α → E}
{s : set α}
{μ : measure_theory.measure α}
(hs : is_open s)
(hf : ∀ (x : α), x ∈ s → continuous_at f x)
(x : α)
(H : x ∈ s) :
strongly_measurable_at_filter f (nhds x) μ
theorem
continuous.strongly_measurable_at_filter
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
[topological_space α]
[opens_measurable_space α]
[topological_space β]
[topological_space.pseudo_metrizable_space β]
[second_countable_topology_either α β]
{f : α → β}
(hf : continuous f)
(μ : measure_theory.measure α)
(l : filter α) :
theorem
continuous_on.strongly_measurable_at_filter_nhds_within
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
[topological_space α]
[opens_measurable_space α]
[topological_space β]
[topological_space.pseudo_metrizable_space β]
[second_countable_topology_either α β]
{f : α → β}
{s : set α}
{μ : measure_theory.measure α}
(hf : continuous_on f s)
(hs : measurable_set s)
(x : α) :
strongly_measurable_at_filter f (nhds_within x s) μ
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 μ].
theorem
integrable_on_Icc_iff_integrable_on_Ioc'
{α : Type u_1}
{E : Type u_3}
[measurable_space α]
[normed_add_comm_group E]
[partial_order α]
[measurable_singleton_class α]
{f : α → E}
{μ : measure_theory.measure α}
{a b : α}
(ha : ⇑μ {a} ≠ ⊤) :
measure_theory.integrable_on f (set.Icc a b) μ ↔ measure_theory.integrable_on f (set.Ioc a b) μ
theorem
integrable_on_Icc_iff_integrable_on_Ico'
{α : Type u_1}
{E : Type u_3}
[measurable_space α]
[normed_add_comm_group E]
[partial_order α]
[measurable_singleton_class α]
{f : α → E}
{μ : measure_theory.measure α}
{a b : α}
(hb : ⇑μ {b} ≠ ⊤) :
measure_theory.integrable_on f (set.Icc a b) μ ↔ measure_theory.integrable_on f (set.Ico a b) μ
theorem
integrable_on_Ico_iff_integrable_on_Ioo'
{α : Type u_1}
{E : Type u_3}
[measurable_space α]
[normed_add_comm_group E]
[partial_order α]
[measurable_singleton_class α]
{f : α → E}
{μ : measure_theory.measure α}
{a b : α}
(ha : ⇑μ {a} ≠ ⊤) :
measure_theory.integrable_on f (set.Ico a b) μ ↔ measure_theory.integrable_on f (set.Ioo a b) μ
theorem
integrable_on_Ioc_iff_integrable_on_Ioo'
{α : Type u_1}
{E : Type u_3}
[measurable_space α]
[normed_add_comm_group E]
[partial_order α]
[measurable_singleton_class α]
{f : α → E}
{μ : measure_theory.measure α}
{a b : α}
(hb : ⇑μ {b} ≠ ⊤) :
measure_theory.integrable_on f (set.Ioc a b) μ ↔ measure_theory.integrable_on f (set.Ioo a b) μ
theorem
integrable_on_Icc_iff_integrable_on_Ioo'
{α : Type u_1}
{E : Type u_3}
[measurable_space α]
[normed_add_comm_group E]
[partial_order α]
[measurable_singleton_class α]
{f : α → E}
{μ : measure_theory.measure α}
{a b : α}
(ha : ⇑μ {a} ≠ ⊤)
(hb : ⇑μ {b} ≠ ⊤) :
measure_theory.integrable_on f (set.Icc a b) μ ↔ measure_theory.integrable_on f (set.Ioo a b) μ
theorem
integrable_on_Ici_iff_integrable_on_Ioi'
{α : Type u_1}
{E : Type u_3}
[measurable_space α]
[normed_add_comm_group E]
[partial_order α]
[measurable_singleton_class α]
{f : α → E}
{μ : measure_theory.measure α}
{b : α}
(hb : ⇑μ {b} ≠ ⊤) :
measure_theory.integrable_on f (set.Ici b) μ ↔ measure_theory.integrable_on f (set.Ioi b) μ
theorem
integrable_on_Iic_iff_integrable_on_Iio'
{α : Type u_1}
{E : Type u_3}
[measurable_space α]
[normed_add_comm_group E]
[partial_order α]
[measurable_singleton_class α]
{f : α → E}
{μ : measure_theory.measure α}
{b : α}
(hb : ⇑μ {b} ≠ ⊤) :
measure_theory.integrable_on f (set.Iic b) μ ↔ measure_theory.integrable_on f (set.Iio b) μ
theorem
integrable_on_Icc_iff_integrable_on_Ioc
{α : Type u_1}
{E : Type u_3}
[measurable_space α]
[normed_add_comm_group E]
[partial_order α]
[measurable_singleton_class α]
{f : α → E}
{μ : measure_theory.measure α}
{a b : α}
[measure_theory.has_no_atoms μ] :
measure_theory.integrable_on f (set.Icc a b) μ ↔ measure_theory.integrable_on f (set.Ioc a b) μ
theorem
integrable_on_Icc_iff_integrable_on_Ico
{α : Type u_1}
{E : Type u_3}
[measurable_space α]
[normed_add_comm_group E]
[partial_order α]
[measurable_singleton_class α]
{f : α → E}
{μ : measure_theory.measure α}
{a b : α}
[measure_theory.has_no_atoms μ] :
measure_theory.integrable_on f (set.Icc a b) μ ↔ measure_theory.integrable_on f (set.Ico a b) μ
theorem
integrable_on_Ico_iff_integrable_on_Ioo
{α : Type u_1}
{E : Type u_3}
[measurable_space α]
[normed_add_comm_group E]
[partial_order α]
[measurable_singleton_class α]
{f : α → E}
{μ : measure_theory.measure α}
{a b : α}
[measure_theory.has_no_atoms μ] :
measure_theory.integrable_on f (set.Ico a b) μ ↔ measure_theory.integrable_on f (set.Ioo a b) μ
theorem
integrable_on_Ioc_iff_integrable_on_Ioo
{α : Type u_1}
{E : Type u_3}
[measurable_space α]
[normed_add_comm_group E]
[partial_order α]
[measurable_singleton_class α]
{f : α → E}
{μ : measure_theory.measure α}
{a b : α}
[measure_theory.has_no_atoms μ] :
measure_theory.integrable_on f (set.Ioc a b) μ ↔ measure_theory.integrable_on f (set.Ioo a b) μ
theorem
integrable_on_Icc_iff_integrable_on_Ioo
{α : Type u_1}
{E : Type u_3}
[measurable_space α]
[normed_add_comm_group E]
[partial_order α]
[measurable_singleton_class α]
{f : α → E}
{μ : measure_theory.measure α}
{a b : α}
[measure_theory.has_no_atoms μ] :
measure_theory.integrable_on f (set.Icc a b) μ ↔ measure_theory.integrable_on f (set.Ioo a b) μ
theorem
integrable_on_Ici_iff_integrable_on_Ioi
{α : Type u_1}
{E : Type u_3}
[measurable_space α]
[normed_add_comm_group E]
[partial_order α]
[measurable_singleton_class α]
{f : α → E}
{μ : measure_theory.measure α}
{b : α}
[measure_theory.has_no_atoms μ] :
measure_theory.integrable_on f (set.Ici b) μ ↔ measure_theory.integrable_on f (set.Ioi b) μ
theorem
integrable_on_Iic_iff_integrable_on_Iio
{α : Type u_1}
{E : Type u_3}
[measurable_space α]
[normed_add_comm_group E]
[partial_order α]
[measurable_singleton_class α]
{f : α → E}
{μ : measure_theory.measure α}
{b : α}
[measure_theory.has_no_atoms μ] :
measure_theory.integrable_on f (set.Iic b) μ ↔ measure_theory.integrable_on f (set.Iio b) μ