Functions integrable on a set and at a filter #
We define IntegrableOn f s μ := Integrable f (μ.restrict s) and prove theorems like
integrableOn_union : IntegrableOn f (s ∪ t) μ ↔ IntegrableOn f s μ ∧ IntegrableOn f t μ.
Next we define a predicate IntegrableAtFilter (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
StronglyMeasurableAtFilter
{α : Type u_1}
{β : Type u_2}
[MeasurableSpace α]
[TopologicalSpace β]
(f : α → β)
(l : Filter α)
(μ : autoParam (MeasureTheory.Measure α) _auto✝)
:
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
- StronglyMeasurableAtFilter f l = ∃ s ∈ l, MeasureTheory.AEStronglyMeasurable f (MeasureTheory.Measure.restrict μ s)
Instances For
@[simp]
theorem
stronglyMeasurableAt_bot
{α : Type u_1}
{β : Type u_2}
[MeasurableSpace α]
[TopologicalSpace β]
{μ : MeasureTheory.Measure α}
{f : α → β}
:
theorem
StronglyMeasurableAtFilter.eventually
{α : Type u_1}
{β : Type u_2}
[MeasurableSpace α]
[TopologicalSpace β]
{l : Filter α}
{f : α → β}
{μ : MeasureTheory.Measure α}
(h : StronglyMeasurableAtFilter f l)
:
∀ᶠ (s : Set α) in Filter.smallSets l, MeasureTheory.AEStronglyMeasurable f (MeasureTheory.Measure.restrict μ s)
theorem
StronglyMeasurableAtFilter.filter_mono
{α : Type u_1}
{β : Type u_2}
[MeasurableSpace α]
[TopologicalSpace β]
{l : Filter α}
{l' : Filter α}
{f : α → β}
{μ : MeasureTheory.Measure α}
(h : StronglyMeasurableAtFilter f l)
(h' : l' ≤ l)
:
theorem
MeasureTheory.AEStronglyMeasurable.stronglyMeasurableAtFilter
{α : Type u_1}
{β : Type u_2}
[MeasurableSpace α]
[TopologicalSpace β]
{l : Filter α}
{f : α → β}
{μ : MeasureTheory.Measure α}
(h : MeasureTheory.AEStronglyMeasurable f μ)
:
theorem
AeStronglyMeasurable.stronglyMeasurableAtFilter_of_mem
{α : Type u_1}
{β : Type u_2}
[MeasurableSpace α]
[TopologicalSpace β]
{l : Filter α}
{f : α → β}
{μ : MeasureTheory.Measure α}
{s : Set α}
(h : MeasureTheory.AEStronglyMeasurable f (MeasureTheory.Measure.restrict μ s))
(hl : s ∈ l)
:
theorem
MeasureTheory.StronglyMeasurable.stronglyMeasurableAtFilter
{α : Type u_1}
{β : Type u_2}
[MeasurableSpace α]
[TopologicalSpace β]
{l : Filter α}
{f : α → β}
{μ : MeasureTheory.Measure α}
(h : MeasureTheory.StronglyMeasurable f)
:
theorem
MeasureTheory.hasFiniteIntegral_restrict_of_bounded
{α : Type u_1}
{E : Type u_3}
[MeasurableSpace α]
[NormedAddCommGroup E]
{f : α → E}
{s : Set α}
{μ : MeasureTheory.Measure α}
{C : ℝ}
(hs : ↑↑μ s < ⊤)
(hf : ∀ᵐ (x : α) ∂MeasureTheory.Measure.restrict μ s, ‖f x‖ ≤ C)
:
def
MeasureTheory.IntegrableOn
{α : Type u_1}
{E : Type u_3}
[MeasurableSpace α]
[NormedAddCommGroup E]
(f : α → E)
(s : Set α)
(μ : autoParam (MeasureTheory.Measure α) _auto✝)
:
A function is IntegrableOn 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
Instances For
theorem
MeasureTheory.integrableOn_def
{α : Type u_1}
{E : Type u_3}
[MeasurableSpace α]
[NormedAddCommGroup E]
(f : α → E)
(s : Set α)
(μ : MeasureTheory.Measure α)
:
theorem
MeasureTheory.IntegrableOn.integrable
{α : Type u_1}
{E : Type u_3}
[MeasurableSpace α]
[NormedAddCommGroup E]
{f : α → E}
{s : Set α}
{μ : MeasureTheory.Measure α}
(h : MeasureTheory.IntegrableOn f s)
:
@[simp]
theorem
MeasureTheory.integrableOn_empty
{α : Type u_1}
{E : Type u_3}
[MeasurableSpace α]
[NormedAddCommGroup E]
{f : α → E}
{μ : MeasureTheory.Measure α}
:
@[simp]
theorem
MeasureTheory.integrableOn_univ
{α : Type u_1}
{E : Type u_3}
[MeasurableSpace α]
[NormedAddCommGroup E]
{f : α → E}
{μ : MeasureTheory.Measure α}
:
MeasureTheory.IntegrableOn f Set.univ ↔ MeasureTheory.Integrable f
theorem
MeasureTheory.integrableOn_zero
{α : Type u_1}
{E : Type u_3}
[MeasurableSpace α]
[NormedAddCommGroup E]
{s : Set α}
{μ : MeasureTheory.Measure α}
:
MeasureTheory.IntegrableOn (fun (x : α) => 0) s
@[simp]
theorem
MeasureTheory.integrableOn_const
{α : Type u_1}
{E : Type u_3}
[MeasurableSpace α]
[NormedAddCommGroup E]
{s : Set α}
{μ : MeasureTheory.Measure α}
{C : E}
:
theorem
MeasureTheory.IntegrableOn.mono
{α : Type u_1}
{E : Type u_3}
[MeasurableSpace α]
[NormedAddCommGroup E]
{f : α → E}
{s : Set α}
{t : Set α}
{μ : MeasureTheory.Measure α}
{ν : MeasureTheory.Measure α}
(h : MeasureTheory.IntegrableOn f t)
(hs : s ⊆ t)
(hμ : μ ≤ ν)
:
theorem
MeasureTheory.IntegrableOn.mono_set
{α : Type u_1}
{E : Type u_3}
[MeasurableSpace α]
[NormedAddCommGroup E]
{f : α → E}
{s : Set α}
{t : Set α}
{μ : MeasureTheory.Measure α}
(h : MeasureTheory.IntegrableOn f t)
(hst : s ⊆ t)
:
theorem
MeasureTheory.IntegrableOn.mono_measure
{α : Type u_1}
{E : Type u_3}
[MeasurableSpace α]
[NormedAddCommGroup E]
{f : α → E}
{s : Set α}
{μ : MeasureTheory.Measure α}
{ν : MeasureTheory.Measure α}
(h : MeasureTheory.IntegrableOn f s)
(hμ : μ ≤ ν)
:
theorem
MeasureTheory.IntegrableOn.mono_set_ae
{α : Type u_1}
{E : Type u_3}
[MeasurableSpace α]
[NormedAddCommGroup E]
{f : α → E}
{s : Set α}
{t : Set α}
{μ : MeasureTheory.Measure α}
(h : MeasureTheory.IntegrableOn f t)
(hst : s ≤ᶠ[MeasureTheory.Measure.ae μ] t)
:
theorem
MeasureTheory.IntegrableOn.congr_set_ae
{α : Type u_1}
{E : Type u_3}
[MeasurableSpace α]
[NormedAddCommGroup E]
{f : α → E}
{s : Set α}
{t : Set α}
{μ : MeasureTheory.Measure α}
(h : MeasureTheory.IntegrableOn f t)
(hst : s =ᶠ[MeasureTheory.Measure.ae μ] t)
:
theorem
MeasureTheory.IntegrableOn.congr_fun_ae
{α : Type u_1}
{E : Type u_3}
[MeasurableSpace α]
[NormedAddCommGroup E]
{f : α → E}
{g : α → E}
{s : Set α}
{μ : MeasureTheory.Measure α}
(h : MeasureTheory.IntegrableOn f s)
(hst : f =ᶠ[MeasureTheory.Measure.ae (MeasureTheory.Measure.restrict μ s)] g)
:
theorem
MeasureTheory.integrableOn_congr_fun_ae
{α : Type u_1}
{E : Type u_3}
[MeasurableSpace α]
[NormedAddCommGroup E]
{f : α → E}
{g : α → E}
{s : Set α}
{μ : MeasureTheory.Measure α}
(hst : f =ᶠ[MeasureTheory.Measure.ae (MeasureTheory.Measure.restrict μ s)] g)
:
theorem
MeasureTheory.IntegrableOn.congr_fun
{α : Type u_1}
{E : Type u_3}
[MeasurableSpace α]
[NormedAddCommGroup E]
{f : α → E}
{g : α → E}
{s : Set α}
{μ : MeasureTheory.Measure α}
(h : MeasureTheory.IntegrableOn f s)
(hst : Set.EqOn f g s)
(hs : MeasurableSet s)
:
theorem
MeasureTheory.integrableOn_congr_fun
{α : Type u_1}
{E : Type u_3}
[MeasurableSpace α]
[NormedAddCommGroup E]
{f : α → E}
{g : α → E}
{s : Set α}
{μ : MeasureTheory.Measure α}
(hst : Set.EqOn f g s)
(hs : MeasurableSet s)
:
theorem
MeasureTheory.Integrable.integrableOn
{α : Type u_1}
{E : Type u_3}
[MeasurableSpace α]
[NormedAddCommGroup E]
{f : α → E}
{s : Set α}
{μ : MeasureTheory.Measure α}
(h : MeasureTheory.Integrable f)
:
theorem
MeasureTheory.IntegrableOn.restrict
{α : Type u_1}
{E : Type u_3}
[MeasurableSpace α]
[NormedAddCommGroup E]
{f : α → E}
{s : Set α}
{t : Set α}
{μ : MeasureTheory.Measure α}
(h : MeasureTheory.IntegrableOn f s)
(hs : MeasurableSet s)
:
theorem
MeasureTheory.IntegrableOn.inter_of_restrict
{α : Type u_1}
{E : Type u_3}
[MeasurableSpace α]
[NormedAddCommGroup E]
{f : α → E}
{s : Set α}
{t : Set α}
{μ : MeasureTheory.Measure α}
(h : MeasureTheory.IntegrableOn f s)
:
MeasureTheory.IntegrableOn f (s ∩ t)
theorem
MeasureTheory.Integrable.piecewise
{α : Type u_1}
{E : Type u_3}
[MeasurableSpace α]
[NormedAddCommGroup E]
{f : α → E}
{g : α → E}
{s : Set α}
{μ : MeasureTheory.Measure α}
[DecidablePred fun (x : α) => x ∈ s]
(hs : MeasurableSet s)
(hf : MeasureTheory.IntegrableOn f s)
(hg : MeasureTheory.IntegrableOn g sᶜ)
:
theorem
MeasureTheory.IntegrableOn.left_of_union
{α : Type u_1}
{E : Type u_3}
[MeasurableSpace α]
[NormedAddCommGroup E]
{f : α → E}
{s : Set α}
{t : Set α}
{μ : MeasureTheory.Measure α}
(h : MeasureTheory.IntegrableOn f (s ∪ t))
:
theorem
MeasureTheory.IntegrableOn.right_of_union
{α : Type u_1}
{E : Type u_3}
[MeasurableSpace α]
[NormedAddCommGroup E]
{f : α → E}
{s : Set α}
{t : Set α}
{μ : MeasureTheory.Measure α}
(h : MeasureTheory.IntegrableOn f (s ∪ t))
:
theorem
MeasureTheory.IntegrableOn.union
{α : Type u_1}
{E : Type u_3}
[MeasurableSpace α]
[NormedAddCommGroup E]
{f : α → E}
{s : Set α}
{t : Set α}
{μ : MeasureTheory.Measure α}
(hs : MeasureTheory.IntegrableOn f s)
(ht : MeasureTheory.IntegrableOn f t)
:
MeasureTheory.IntegrableOn f (s ∪ t)
@[simp]
theorem
MeasureTheory.integrableOn_union
{α : Type u_1}
{E : Type u_3}
[MeasurableSpace α]
[NormedAddCommGroup E]
{f : α → E}
{s : Set α}
{t : Set α}
{μ : MeasureTheory.Measure α}
:
MeasureTheory.IntegrableOn f (s ∪ t) ↔ MeasureTheory.IntegrableOn f s ∧ MeasureTheory.IntegrableOn f t
@[simp]
theorem
MeasureTheory.integrableOn_singleton_iff
{α : Type u_1}
{E : Type u_3}
[MeasurableSpace α]
[NormedAddCommGroup E]
{f : α → E}
{μ : MeasureTheory.Measure α}
{x : α}
[MeasurableSingletonClass α]
:
@[simp]
theorem
MeasureTheory.integrableOn_finite_biUnion
{α : Type u_1}
{β : Type u_2}
{E : Type u_3}
[MeasurableSpace α]
[NormedAddCommGroup E]
{f : α → E}
{μ : MeasureTheory.Measure α}
{s : Set β}
(hs : Set.Finite s)
{t : β → Set α}
:
MeasureTheory.IntegrableOn f (⋃ i ∈ s, t i) ↔ ∀ i ∈ s, MeasureTheory.IntegrableOn f (t i)
@[simp]
theorem
MeasureTheory.integrableOn_finset_iUnion
{α : Type u_1}
{β : Type u_2}
{E : Type u_3}
[MeasurableSpace α]
[NormedAddCommGroup E]
{f : α → E}
{μ : MeasureTheory.Measure α}
{s : Finset β}
{t : β → Set α}
:
MeasureTheory.IntegrableOn f (⋃ i ∈ s, t i) ↔ ∀ i ∈ s, MeasureTheory.IntegrableOn f (t i)
@[simp]
theorem
MeasureTheory.integrableOn_finite_iUnion
{α : Type u_1}
{β : Type u_2}
{E : Type u_3}
[MeasurableSpace α]
[NormedAddCommGroup E]
{f : α → E}
{μ : MeasureTheory.Measure α}
[Finite β]
{t : β → Set α}
:
MeasureTheory.IntegrableOn f (⋃ (i : β), t i) ↔ ∀ (i : β), MeasureTheory.IntegrableOn f (t i)
theorem
MeasureTheory.IntegrableOn.add_measure
{α : Type u_1}
{E : Type u_3}
[MeasurableSpace α]
[NormedAddCommGroup E]
{f : α → E}
{s : Set α}
{μ : MeasureTheory.Measure α}
{ν : MeasureTheory.Measure α}
(hμ : MeasureTheory.IntegrableOn f s)
(hν : MeasureTheory.IntegrableOn f s)
:
@[simp]
theorem
MeasureTheory.integrableOn_add_measure
{α : Type u_1}
{E : Type u_3}
[MeasurableSpace α]
[NormedAddCommGroup E]
{f : α → E}
{s : Set α}
{μ : MeasureTheory.Measure α}
{ν : MeasureTheory.Measure α}
:
theorem
MeasurableEmbedding.integrableOn_map_iff
{α : Type u_1}
{β : Type u_2}
{E : Type u_3}
[MeasurableSpace α]
[NormedAddCommGroup E]
[MeasurableSpace β]
{e : α → β}
(he : MeasurableEmbedding e)
{f : β → E}
{μ : MeasureTheory.Measure α}
{s : Set β}
:
MeasureTheory.IntegrableOn f s ↔ MeasureTheory.IntegrableOn (f ∘ e) (e ⁻¹' s)
theorem
MeasurableEmbedding.integrableOn_iff_comap
{α : Type u_1}
{β : Type u_2}
{E : Type u_3}
[MeasurableSpace α]
[NormedAddCommGroup E]
[MeasurableSpace β]
{e : α → β}
(he : MeasurableEmbedding e)
{f : β → E}
{μ : MeasureTheory.Measure β}
{s : Set β}
(hs : s ⊆ Set.range e)
:
MeasureTheory.IntegrableOn f s ↔ MeasureTheory.IntegrableOn (f ∘ e) (e ⁻¹' s)
theorem
MeasureTheory.integrableOn_map_equiv
{α : Type u_1}
{β : Type u_2}
{E : Type u_3}
[MeasurableSpace α]
[NormedAddCommGroup E]
[MeasurableSpace β]
(e : α ≃ᵐ β)
{f : β → E}
{μ : MeasureTheory.Measure α}
{s : Set β}
:
MeasureTheory.IntegrableOn f s ↔ MeasureTheory.IntegrableOn (f ∘ ⇑e) (⇑e ⁻¹' s)
theorem
MeasureTheory.MeasurePreserving.integrableOn_comp_preimage
{α : Type u_1}
{β : Type u_2}
{E : Type u_3}
[MeasurableSpace α]
[NormedAddCommGroup E]
{μ : MeasureTheory.Measure α}
[MeasurableSpace β]
{e : α → β}
{ν : MeasureTheory.Measure β}
(h₁ : MeasureTheory.MeasurePreserving e)
(h₂ : MeasurableEmbedding e)
{f : β → E}
{s : Set β}
:
MeasureTheory.IntegrableOn (f ∘ e) (e ⁻¹' s) ↔ MeasureTheory.IntegrableOn f s
theorem
MeasureTheory.MeasurePreserving.integrableOn_image
{α : Type u_1}
{β : Type u_2}
{E : Type u_3}
[MeasurableSpace α]
[NormedAddCommGroup E]
{μ : MeasureTheory.Measure α}
[MeasurableSpace β]
{e : α → β}
{ν : MeasureTheory.Measure β}
(h₁ : MeasureTheory.MeasurePreserving e)
(h₂ : MeasurableEmbedding e)
{f : β → E}
{s : Set α}
:
MeasureTheory.IntegrableOn f (e '' s) ↔ MeasureTheory.IntegrableOn (f ∘ e) s
theorem
MeasureTheory.integrable_indicator_iff
{α : Type u_1}
{E : Type u_3}
[MeasurableSpace α]
[NormedAddCommGroup E]
{f : α → E}
{s : Set α}
{μ : MeasureTheory.Measure α}
(hs : MeasurableSet s)
:
theorem
MeasureTheory.IntegrableOn.integrable_indicator
{α : Type u_1}
{E : Type u_3}
[MeasurableSpace α]
[NormedAddCommGroup E]
{f : α → E}
{s : Set α}
{μ : MeasureTheory.Measure α}
(h : MeasureTheory.IntegrableOn f s)
(hs : MeasurableSet s)
:
theorem
MeasureTheory.Integrable.indicator
{α : Type u_1}
{E : Type u_3}
[MeasurableSpace α]
[NormedAddCommGroup E]
{f : α → E}
{s : Set α}
{μ : MeasureTheory.Measure α}
(h : MeasureTheory.Integrable f)
(hs : MeasurableSet s)
:
theorem
MeasureTheory.IntegrableOn.indicator
{α : Type u_1}
{E : Type u_3}
[MeasurableSpace α]
[NormedAddCommGroup E]
{f : α → E}
{s : Set α}
{t : Set α}
{μ : MeasureTheory.Measure α}
(h : MeasureTheory.IntegrableOn f s)
(ht : MeasurableSet t)
:
theorem
MeasureTheory.integrable_indicatorConstLp
{α : Type u_1}
[MeasurableSpace α]
{μ : MeasureTheory.Measure α}
{E : Type u_5}
[NormedAddCommGroup E]
{p : ENNReal}
{s : Set α}
(hs : MeasurableSet s)
(hμs : ↑↑μ s ≠ ⊤)
(c : E)
:
MeasureTheory.Integrable ↑↑(MeasureTheory.indicatorConstLp p hs hμs c)
theorem
MeasureTheory.IntegrableOn.restrict_toMeasurable
{α : Type u_1}
{E : Type u_3}
[MeasurableSpace α]
[NormedAddCommGroup E]
{f : α → E}
{s : Set α}
{μ : MeasureTheory.Measure α}
(hf : MeasureTheory.IntegrableOn f s)
(h's : ∀ 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 toMeasurable μ s coincides with its restriction
to s.
theorem
MeasureTheory.IntegrableOn.of_ae_diff_eq_zero
{α : Type u_1}
{E : Type u_3}
[MeasurableSpace α]
[NormedAddCommGroup E]
{f : α → E}
{s : Set α}
{t : Set α}
{μ : MeasureTheory.Measure α}
(hf : MeasureTheory.IntegrableOn f s)
(ht : MeasureTheory.NullMeasurableSet 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
MeasureTheory.IntegrableOn.of_forall_diff_eq_zero
{α : Type u_1}
{E : Type u_3}
[MeasurableSpace α]
[NormedAddCommGroup E]
{f : α → E}
{s : Set α}
{t : Set α}
{μ : MeasureTheory.Measure α}
(hf : MeasureTheory.IntegrableOn f s)
(ht : MeasurableSet t)
(h't : ∀ 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
MeasureTheory.IntegrableOn.integrable_of_ae_not_mem_eq_zero
{α : Type u_1}
{E : Type u_3}
[MeasurableSpace α]
[NormedAddCommGroup E]
{f : α → E}
{s : Set α}
{μ : MeasureTheory.Measure α}
(hf : MeasureTheory.IntegrableOn 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
MeasureTheory.IntegrableOn.integrable_of_forall_not_mem_eq_zero
{α : Type u_1}
{E : Type u_3}
[MeasurableSpace α]
[NormedAddCommGroup E]
{f : α → E}
{s : Set α}
{μ : MeasureTheory.Measure α}
(hf : MeasureTheory.IntegrableOn f s)
(h't : ∀ 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
MeasureTheory.integrableOn_iff_integrable_of_support_subset
{α : Type u_1}
{E : Type u_3}
[MeasurableSpace α]
[NormedAddCommGroup E]
{f : α → E}
{s : Set α}
{μ : MeasureTheory.Measure α}
(h1s : Function.support f ⊆ s)
:
theorem
MeasureTheory.integrableOn_Lp_of_measure_ne_top
{α : Type u_1}
[MeasurableSpace α]
{μ : MeasureTheory.Measure α}
{E : Type u_5}
[NormedAddCommGroup E]
{p : ENNReal}
{s : Set α}
(f : ↥(MeasureTheory.Lp E p))
(hp : 1 ≤ p)
(hμs : ↑↑μ s ≠ ⊤)
:
MeasureTheory.IntegrableOn (↑↑f) s
theorem
MeasureTheory.Integrable.lintegral_lt_top
{α : Type u_1}
[MeasurableSpace α]
{μ : MeasureTheory.Measure α}
{f : α → ℝ}
(hf : MeasureTheory.Integrable f)
:
∫⁻ (x : α), ENNReal.ofReal (f x) ∂μ < ⊤
theorem
MeasureTheory.IntegrableOn.set_lintegral_lt_top
{α : Type u_1}
[MeasurableSpace α]
{μ : MeasureTheory.Measure α}
{f : α → ℝ}
{s : Set α}
(hf : MeasureTheory.IntegrableOn f s)
:
∫⁻ (x : α) in s, ENNReal.ofReal (f x) ∂μ < ⊤
def
MeasureTheory.IntegrableAtFilter
{α : Type u_1}
{E : Type u_3}
[MeasurableSpace α]
[NormedAddCommGroup E]
(f : α → E)
(l : Filter α)
(μ : autoParam (MeasureTheory.Measure α) _auto✝)
:
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.smallSets.
Equations
- MeasureTheory.IntegrableAtFilter f l = ∃ s ∈ l, MeasureTheory.IntegrableOn f s
Instances For
theorem
MeasurableEmbedding.integrableAtFilter_map_iff
{α : Type u_1}
{β : Type u_2}
{E : Type u_3}
[MeasurableSpace α]
[NormedAddCommGroup E]
{μ : MeasureTheory.Measure α}
{l : Filter α}
[MeasurableSpace β]
{e : α → β}
(he : MeasurableEmbedding e)
{f : β → E}
:
MeasureTheory.IntegrableAtFilter f (Filter.map e l) ↔ MeasureTheory.IntegrableAtFilter (f ∘ e) l
theorem
MeasurableEmbedding.integrableAtFilter_iff_comap
{α : Type u_1}
{β : Type u_2}
{E : Type u_3}
[MeasurableSpace α]
[NormedAddCommGroup E]
{l : Filter α}
[MeasurableSpace β]
{e : α → β}
(he : MeasurableEmbedding e)
{f : β → E}
{μ : MeasureTheory.Measure β}
:
MeasureTheory.IntegrableAtFilter f (Filter.map e l) ↔ MeasureTheory.IntegrableAtFilter (f ∘ e) l
theorem
MeasureTheory.Integrable.integrableAtFilter
{α : Type u_1}
{E : Type u_3}
[MeasurableSpace α]
[NormedAddCommGroup E]
{f : α → E}
{μ : MeasureTheory.Measure α}
(h : MeasureTheory.Integrable f)
(l : Filter α)
:
theorem
MeasureTheory.IntegrableAtFilter.eventually
{α : Type u_1}
{E : Type u_3}
[MeasurableSpace α]
[NormedAddCommGroup E]
{f : α → E}
{μ : MeasureTheory.Measure α}
{l : Filter α}
(h : MeasureTheory.IntegrableAtFilter f l)
:
∀ᶠ (s : Set α) in Filter.smallSets l, MeasureTheory.IntegrableOn f s
theorem
MeasureTheory.IntegrableAtFilter.add
{α : Type u_1}
{E : Type u_3}
[MeasurableSpace α]
[NormedAddCommGroup E]
{μ : MeasureTheory.Measure α}
{l : Filter α}
{f : α → E}
{g : α → E}
(hf : MeasureTheory.IntegrableAtFilter f l)
(hg : MeasureTheory.IntegrableAtFilter g l)
:
MeasureTheory.IntegrableAtFilter (f + g) l
theorem
MeasureTheory.IntegrableAtFilter.neg
{α : Type u_1}
{E : Type u_3}
[MeasurableSpace α]
[NormedAddCommGroup E]
{μ : MeasureTheory.Measure α}
{l : Filter α}
{f : α → E}
(hf : MeasureTheory.IntegrableAtFilter f l)
:
theorem
MeasureTheory.IntegrableAtFilter.sub
{α : Type u_1}
{E : Type u_3}
[MeasurableSpace α]
[NormedAddCommGroup E]
{μ : MeasureTheory.Measure α}
{l : Filter α}
{f : α → E}
{g : α → E}
(hf : MeasureTheory.IntegrableAtFilter f l)
(hg : MeasureTheory.IntegrableAtFilter g l)
:
MeasureTheory.IntegrableAtFilter (f - g) l
theorem
MeasureTheory.IntegrableAtFilter.smul
{α : Type u_1}
{E : Type u_3}
[MeasurableSpace α]
[NormedAddCommGroup E]
{μ : MeasureTheory.Measure α}
{l : Filter α}
{𝕜 : Type u_5}
[NormedAddCommGroup 𝕜]
[SMulZeroClass 𝕜 E]
[BoundedSMul 𝕜 E]
{f : α → E}
(hf : MeasureTheory.IntegrableAtFilter f l)
(c : 𝕜)
:
MeasureTheory.IntegrableAtFilter (c • f) l
theorem
MeasureTheory.IntegrableAtFilter.norm
{α : Type u_1}
{E : Type u_3}
[MeasurableSpace α]
[NormedAddCommGroup E]
{f : α → E}
{μ : MeasureTheory.Measure α}
{l : Filter α}
(hf : MeasureTheory.IntegrableAtFilter f l)
:
MeasureTheory.IntegrableAtFilter (fun (x : α) => ‖f x‖) l
theorem
MeasureTheory.IntegrableAtFilter.filter_mono
{α : Type u_1}
{E : Type u_3}
[MeasurableSpace α]
[NormedAddCommGroup E]
{f : α → E}
{μ : MeasureTheory.Measure α}
{l : Filter α}
{l' : Filter α}
(hl : l ≤ l')
(hl' : MeasureTheory.IntegrableAtFilter f l')
:
theorem
MeasureTheory.IntegrableAtFilter.inf_of_left
{α : Type u_1}
{E : Type u_3}
[MeasurableSpace α]
[NormedAddCommGroup E]
{f : α → E}
{μ : MeasureTheory.Measure α}
{l : Filter α}
{l' : Filter α}
(hl : MeasureTheory.IntegrableAtFilter f l)
:
MeasureTheory.IntegrableAtFilter f (l ⊓ l')
theorem
MeasureTheory.IntegrableAtFilter.inf_of_right
{α : Type u_1}
{E : Type u_3}
[MeasurableSpace α]
[NormedAddCommGroup E]
{f : α → E}
{μ : MeasureTheory.Measure α}
{l : Filter α}
{l' : Filter α}
(hl : MeasureTheory.IntegrableAtFilter f l)
:
MeasureTheory.IntegrableAtFilter f (l' ⊓ l)
@[simp]
theorem
MeasureTheory.IntegrableAtFilter.inf_ae_iff
{α : Type u_1}
{E : Type u_3}
[MeasurableSpace α]
[NormedAddCommGroup E]
{f : α → E}
{μ : MeasureTheory.Measure α}
{l : Filter α}
:
theorem
MeasureTheory.IntegrableAtFilter.of_inf_ae
{α : Type u_1}
{E : Type u_3}
[MeasurableSpace α]
[NormedAddCommGroup E]
{f : α → E}
{μ : MeasureTheory.Measure α}
{l : Filter α}
:
Alias of the forward direction of MeasureTheory.IntegrableAtFilter.inf_ae_iff.
@[simp]
theorem
MeasureTheory.integrableAtFilter_top
{α : Type u_1}
{E : Type u_3}
[MeasurableSpace α]
[NormedAddCommGroup E]
{f : α → E}
{μ : MeasureTheory.Measure α}
:
theorem
MeasureTheory.Measure.FiniteAtFilter.integrableAtFilter
{α : Type u_1}
{E : Type u_3}
[MeasurableSpace α]
[NormedAddCommGroup E]
{f : α → E}
{μ : MeasureTheory.Measure α}
{l : Filter α}
[Filter.IsMeasurablyGenerated l]
(hfm : StronglyMeasurableAtFilter f l)
(hμ : MeasureTheory.Measure.FiniteAtFilter μ l)
(hf : Filter.IsBoundedUnder (fun (x x_1 : ℝ) => x ≤ x_1) l (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
MeasureTheory.Measure.FiniteAtFilter.integrableAtFilter_of_tendsto_ae
{α : Type u_1}
{E : Type u_3}
[MeasurableSpace α]
[NormedAddCommGroup E]
{f : α → E}
{μ : MeasureTheory.Measure α}
{l : Filter α}
[Filter.IsMeasurablyGenerated l]
(hfm : StronglyMeasurableAtFilter f l)
(hμ : MeasureTheory.Measure.FiniteAtFilter μ l)
{b : E}
(hf : Filter.Tendsto f (l ⊓ MeasureTheory.Measure.ae μ) (nhds b))
:
theorem
Filter.Tendsto.integrableAtFilter_ae
{α : Type u_1}
{E : Type u_3}
[MeasurableSpace α]
[NormedAddCommGroup E]
{f : α → E}
{μ : MeasureTheory.Measure α}
{l : Filter α}
[Filter.IsMeasurablyGenerated l]
(hfm : StronglyMeasurableAtFilter f l)
(hμ : MeasureTheory.Measure.FiniteAtFilter μ l)
{b : E}
(hf : Filter.Tendsto f (l ⊓ MeasureTheory.Measure.ae μ) (nhds b))
:
Alias of MeasureTheory.Measure.FiniteAtFilter.integrableAtFilter_of_tendsto_ae.
theorem
MeasureTheory.Measure.FiniteAtFilter.integrableAtFilter_of_tendsto
{α : Type u_1}
{E : Type u_3}
[MeasurableSpace α]
[NormedAddCommGroup E]
{f : α → E}
{μ : MeasureTheory.Measure α}
{l : Filter α}
[Filter.IsMeasurablyGenerated l]
(hfm : StronglyMeasurableAtFilter f l)
(hμ : MeasureTheory.Measure.FiniteAtFilter μ l)
{b : E}
(hf : Filter.Tendsto f l (nhds b))
:
theorem
Filter.Tendsto.integrableAtFilter
{α : Type u_1}
{E : Type u_3}
[MeasurableSpace α]
[NormedAddCommGroup E]
{f : α → E}
{μ : MeasureTheory.Measure α}
{l : Filter α}
[Filter.IsMeasurablyGenerated l]
(hfm : StronglyMeasurableAtFilter f l)
(hμ : MeasureTheory.Measure.FiniteAtFilter μ l)
{b : E}
(hf : Filter.Tendsto f l (nhds b))
:
Alias of MeasureTheory.Measure.FiniteAtFilter.integrableAtFilter_of_tendsto.
theorem
MeasureTheory.integrable_add_of_disjoint
{α : Type u_1}
{E : Type u_3}
[MeasurableSpace α]
[NormedAddCommGroup E]
{μ : MeasureTheory.Measure α}
{f : α → E}
{g : α → E}
(h : Disjoint (Function.support f) (Function.support g))
(hf : MeasureTheory.StronglyMeasurable f)
(hg : MeasureTheory.StronglyMeasurable g)
:
theorem
ContinuousOn.aemeasurable
{α : Type u_1}
{β : Type u_2}
[MeasurableSpace α]
[TopologicalSpace α]
[OpensMeasurableSpace α]
[MeasurableSpace β]
[TopologicalSpace β]
[BorelSpace β]
{f : α → β}
{s : Set α}
{μ : MeasureTheory.Measure α}
(hf : ContinuousOn f s)
(hs : MeasurableSet s)
:
A function which is continuous on a set s is almost everywhere measurable with respect to
μ.restrict s.
theorem
ContinuousOn.aestronglyMeasurable_of_isSeparable
{α : Type u_1}
{β : Type u_2}
[MeasurableSpace α]
[TopologicalSpace α]
[TopologicalSpace.PseudoMetrizableSpace α]
[OpensMeasurableSpace α]
[TopologicalSpace β]
[TopologicalSpace.PseudoMetrizableSpace β]
{f : α → β}
{s : Set α}
{μ : MeasureTheory.Measure α}
(hf : ContinuousOn f s)
(hs : MeasurableSet s)
(h's : TopologicalSpace.IsSeparable s)
:
A function which is continuous on a separable set s is almost everywhere strongly measurable
with respect to μ.restrict s.
theorem
ContinuousOn.aestronglyMeasurable
{α : Type u_1}
{β : Type u_2}
[MeasurableSpace α]
[TopologicalSpace α]
[TopologicalSpace β]
[h : SecondCountableTopologyEither α β]
[OpensMeasurableSpace α]
[TopologicalSpace.PseudoMetrizableSpace β]
{f : α → β}
{s : Set α}
{μ : MeasureTheory.Measure α}
(hf : ContinuousOn f s)
(hs : MeasurableSet 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
ContinuousOn.aestronglyMeasurable_of_isCompact
{α : Type u_1}
{β : Type u_2}
[MeasurableSpace α]
[TopologicalSpace α]
[OpensMeasurableSpace α]
[TopologicalSpace β]
[TopologicalSpace.PseudoMetrizableSpace β]
{f : α → β}
{s : Set α}
{μ : MeasureTheory.Measure α}
(hf : ContinuousOn f s)
(hs : IsCompact s)
(h's : MeasurableSet s)
:
A function which is continuous on a compact set s is almost everywhere strongly measurable
with respect to μ.restrict s.
theorem
ContinuousOn.integrableAt_nhdsWithin_of_isSeparable
{α : Type u_1}
{E : Type u_3}
[MeasurableSpace α]
[NormedAddCommGroup E]
[TopologicalSpace α]
[TopologicalSpace.PseudoMetrizableSpace α]
[OpensMeasurableSpace α]
{μ : MeasureTheory.Measure α}
[MeasureTheory.IsLocallyFiniteMeasure μ]
{a : α}
{t : Set α}
{f : α → E}
(hft : ContinuousOn f t)
(ht : MeasurableSet t)
(h't : TopologicalSpace.IsSeparable t)
(ha : a ∈ t)
:
theorem
ContinuousOn.integrableAt_nhdsWithin
{α : Type u_1}
{E : Type u_3}
[MeasurableSpace α]
[NormedAddCommGroup E]
[TopologicalSpace α]
[SecondCountableTopologyEither α E]
[OpensMeasurableSpace α]
{μ : MeasureTheory.Measure α}
[MeasureTheory.IsLocallyFiniteMeasure μ]
{a : α}
{t : Set α}
{f : α → E}
(hft : ContinuousOn f t)
(ht : MeasurableSet t)
(ha : a ∈ t)
:
theorem
Continuous.integrableAt_nhds
{α : Type u_1}
{E : Type u_3}
[MeasurableSpace α]
[NormedAddCommGroup E]
[TopologicalSpace α]
[SecondCountableTopologyEither α E]
[OpensMeasurableSpace α]
{μ : MeasureTheory.Measure α}
[MeasureTheory.IsLocallyFiniteMeasure μ]
{f : α → E}
(hf : Continuous f)
(a : α)
:
theorem
ContinuousOn.stronglyMeasurableAtFilter
{α : Type u_1}
{β : Type u_2}
[MeasurableSpace α]
[TopologicalSpace α]
[OpensMeasurableSpace α]
[TopologicalSpace β]
[TopologicalSpace.PseudoMetrizableSpace β]
[SecondCountableTopologyEither α β]
{f : α → β}
{s : Set α}
{μ : MeasureTheory.Measure α}
(hs : IsOpen s)
(hf : ContinuousOn f s)
(x : α)
:
x ∈ s → StronglyMeasurableAtFilter 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
ContinuousAt.stronglyMeasurableAtFilter
{α : Type u_1}
{E : Type u_3}
[MeasurableSpace α]
[NormedAddCommGroup E]
[TopologicalSpace α]
[OpensMeasurableSpace α]
[SecondCountableTopologyEither α E]
{f : α → E}
{s : Set α}
{μ : MeasureTheory.Measure α}
(hs : IsOpen s)
(hf : ∀ x ∈ s, ContinuousAt f x)
(x : α)
:
x ∈ s → StronglyMeasurableAtFilter f (nhds x)
theorem
Continuous.stronglyMeasurableAtFilter
{α : Type u_1}
{β : Type u_2}
[MeasurableSpace α]
[TopologicalSpace α]
[OpensMeasurableSpace α]
[TopologicalSpace β]
[TopologicalSpace.PseudoMetrizableSpace β]
[SecondCountableTopologyEither α β]
{f : α → β}
(hf : Continuous f)
(μ : MeasureTheory.Measure α)
(l : Filter α)
:
theorem
ContinuousOn.stronglyMeasurableAtFilter_nhdsWithin
{α : Type u_5}
{β : Type u_6}
[MeasurableSpace α]
[TopologicalSpace α]
[OpensMeasurableSpace α]
[TopologicalSpace β]
[TopologicalSpace.PseudoMetrizableSpace β]
[SecondCountableTopologyEither α β]
{f : α → β}
{s : Set α}
{μ : MeasureTheory.Measure α}
(hf : ContinuousOn f s)
(hs : MeasurableSet s)
(x : α)
:
StronglyMeasurableAtFilter f (nhdsWithin 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 [NoAtoms μ].
theorem
integrableOn_Icc_iff_integrableOn_Ioc'
{α : Type u_1}
{E : Type u_3}
[MeasurableSpace α]
[NormedAddCommGroup E]
[PartialOrder α]
[MeasurableSingletonClass α]
{f : α → E}
{μ : MeasureTheory.Measure α}
{a : α}
{b : α}
(ha : ↑↑μ {a} ≠ ⊤)
:
MeasureTheory.IntegrableOn f (Set.Icc a b) ↔ MeasureTheory.IntegrableOn f (Set.Ioc a b)
theorem
integrableOn_Icc_iff_integrableOn_Ico'
{α : Type u_1}
{E : Type u_3}
[MeasurableSpace α]
[NormedAddCommGroup E]
[PartialOrder α]
[MeasurableSingletonClass α]
{f : α → E}
{μ : MeasureTheory.Measure α}
{a : α}
{b : α}
(hb : ↑↑μ {b} ≠ ⊤)
:
MeasureTheory.IntegrableOn f (Set.Icc a b) ↔ MeasureTheory.IntegrableOn f (Set.Ico a b)
theorem
integrableOn_Ico_iff_integrableOn_Ioo'
{α : Type u_1}
{E : Type u_3}
[MeasurableSpace α]
[NormedAddCommGroup E]
[PartialOrder α]
[MeasurableSingletonClass α]
{f : α → E}
{μ : MeasureTheory.Measure α}
{a : α}
{b : α}
(ha : ↑↑μ {a} ≠ ⊤)
:
MeasureTheory.IntegrableOn f (Set.Ico a b) ↔ MeasureTheory.IntegrableOn f (Set.Ioo a b)
theorem
integrableOn_Ioc_iff_integrableOn_Ioo'
{α : Type u_1}
{E : Type u_3}
[MeasurableSpace α]
[NormedAddCommGroup E]
[PartialOrder α]
[MeasurableSingletonClass α]
{f : α → E}
{μ : MeasureTheory.Measure α}
{a : α}
{b : α}
(hb : ↑↑μ {b} ≠ ⊤)
:
MeasureTheory.IntegrableOn f (Set.Ioc a b) ↔ MeasureTheory.IntegrableOn f (Set.Ioo a b)
theorem
integrableOn_Icc_iff_integrableOn_Ioo'
{α : Type u_1}
{E : Type u_3}
[MeasurableSpace α]
[NormedAddCommGroup E]
[PartialOrder α]
[MeasurableSingletonClass α]
{f : α → E}
{μ : MeasureTheory.Measure α}
{a : α}
{b : α}
(ha : ↑↑μ {a} ≠ ⊤)
(hb : ↑↑μ {b} ≠ ⊤)
:
MeasureTheory.IntegrableOn f (Set.Icc a b) ↔ MeasureTheory.IntegrableOn f (Set.Ioo a b)
theorem
integrableOn_Ici_iff_integrableOn_Ioi'
{α : Type u_1}
{E : Type u_3}
[MeasurableSpace α]
[NormedAddCommGroup E]
[PartialOrder α]
[MeasurableSingletonClass α]
{f : α → E}
{μ : MeasureTheory.Measure α}
{b : α}
(hb : ↑↑μ {b} ≠ ⊤)
:
theorem
integrableOn_Iic_iff_integrableOn_Iio'
{α : Type u_1}
{E : Type u_3}
[MeasurableSpace α]
[NormedAddCommGroup E]
[PartialOrder α]
[MeasurableSingletonClass α]
{f : α → E}
{μ : MeasureTheory.Measure α}
{b : α}
(hb : ↑↑μ {b} ≠ ⊤)
:
theorem
integrableOn_Icc_iff_integrableOn_Ioc
{α : Type u_1}
{E : Type u_3}
[MeasurableSpace α]
[NormedAddCommGroup E]
[PartialOrder α]
[MeasurableSingletonClass α]
{f : α → E}
{μ : MeasureTheory.Measure α}
{a : α}
{b : α}
[MeasureTheory.NoAtoms μ]
:
MeasureTheory.IntegrableOn f (Set.Icc a b) ↔ MeasureTheory.IntegrableOn f (Set.Ioc a b)
theorem
integrableOn_Icc_iff_integrableOn_Ico
{α : Type u_1}
{E : Type u_3}
[MeasurableSpace α]
[NormedAddCommGroup E]
[PartialOrder α]
[MeasurableSingletonClass α]
{f : α → E}
{μ : MeasureTheory.Measure α}
{a : α}
{b : α}
[MeasureTheory.NoAtoms μ]
:
MeasureTheory.IntegrableOn f (Set.Icc a b) ↔ MeasureTheory.IntegrableOn f (Set.Ico a b)
theorem
integrableOn_Ico_iff_integrableOn_Ioo
{α : Type u_1}
{E : Type u_3}
[MeasurableSpace α]
[NormedAddCommGroup E]
[PartialOrder α]
[MeasurableSingletonClass α]
{f : α → E}
{μ : MeasureTheory.Measure α}
{a : α}
{b : α}
[MeasureTheory.NoAtoms μ]
:
MeasureTheory.IntegrableOn f (Set.Ico a b) ↔ MeasureTheory.IntegrableOn f (Set.Ioo a b)
theorem
integrableOn_Ioc_iff_integrableOn_Ioo
{α : Type u_1}
{E : Type u_3}
[MeasurableSpace α]
[NormedAddCommGroup E]
[PartialOrder α]
[MeasurableSingletonClass α]
{f : α → E}
{μ : MeasureTheory.Measure α}
{a : α}
{b : α}
[MeasureTheory.NoAtoms μ]
:
MeasureTheory.IntegrableOn f (Set.Ioc a b) ↔ MeasureTheory.IntegrableOn f (Set.Ioo a b)
theorem
integrableOn_Icc_iff_integrableOn_Ioo
{α : Type u_1}
{E : Type u_3}
[MeasurableSpace α]
[NormedAddCommGroup E]
[PartialOrder α]
[MeasurableSingletonClass α]
{f : α → E}
{μ : MeasureTheory.Measure α}
{a : α}
{b : α}
[MeasureTheory.NoAtoms μ]
:
MeasureTheory.IntegrableOn f (Set.Icc a b) ↔ MeasureTheory.IntegrableOn f (Set.Ioo a b)
theorem
integrableOn_Ici_iff_integrableOn_Ioi
{α : Type u_1}
{E : Type u_3}
[MeasurableSpace α]
[NormedAddCommGroup E]
[PartialOrder α]
[MeasurableSingletonClass α]
{f : α → E}
{μ : MeasureTheory.Measure α}
{b : α}
[MeasureTheory.NoAtoms μ]
:
theorem
integrableOn_Iic_iff_integrableOn_Iio
{α : Type u_1}
{E : Type u_3}
[MeasurableSpace α]
[NormedAddCommGroup E]
[PartialOrder α]
[MeasurableSingletonClass α]
{f : α → E}
{μ : MeasureTheory.Measure α}
{b : α}
[MeasureTheory.NoAtoms μ]
: