ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>MeasurableSpace α<VAR>TopologicalSpace β<VAR>l : Filter α<VAR>f : α → β<VAR>μ : MeasureTheory.Measure α<VAR>h : StronglyMeasurableAtFilter f l μ<GOAL>∀ᶠ (s : Set α) in l.smallSets, MeasureTheory.AEStronglyMeasurable f (μ.restrict s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>MeasurableSpace α<VAR>TopologicalSpace β<VAR>l l' : Filter α<VAR>f : α → β<VAR>μ : MeasureTheory.Measure α<VAR>h : StronglyMeasurableAtFilter f l μ<VAR>h' : l' ≤ l<GOAL>StronglyMeasurableAtFilter f l' μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>MeasurableSpace α<VAR>TopologicalSpace β<VAR>l : Filter α<VAR>f : α → β<VAR>μ : MeasureTheory.Measure α<VAR>h : MeasureTheory.AEStronglyMeasurable f μ<GOAL>StronglyMeasurableAtFilter f l μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>MeasurableSpace α<VAR>TopologicalSpace β<VAR>l : Filter α<VAR>f : α → β<VAR>μ : MeasureTheory.Measure α<VAR>s : Set α<VAR>h : MeasureTheory.AEStronglyMeasurable f (μ.restrict s)<VAR>hl : s ∈ l<GOAL>StronglyMeasurableAtFilter f l μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>MeasurableSpace α<VAR>TopologicalSpace β<VAR>l : Filter α<VAR>f : α → β<VAR>μ : MeasureTheory.Measure α<VAR>h : MeasureTheory.StronglyMeasurable f<GOAL>StronglyMeasurableAtFilter f l μ
<VAR>α : Type u_1<VAR>E : Type u_3<VAR>MeasurableSpace α<VAR>NormedAddCommGroup E<VAR>f : α → E<VAR>s : Set α<VAR>μ : MeasureTheory.Measure α<VAR>C : ℝ<VAR>hs : μ s < ⊤<VAR>hf : ∀ᵐ (x : α) ∂μ.restrict s, ‖f x‖ ≤ C<GOAL>MeasureTheory.HasFiniteIntegral f (μ.restrict s)
<VAR>α : Type u_1<VAR>E : Type u_3<VAR>MeasurableSpace α<VAR>NormedAddCommGroup E<VAR>f : α → E<VAR>s : Set α<VAR>μ : MeasureTheory.Measure α<VAR>h : MeasureTheory.IntegrableOn f s μ<GOAL>MeasureTheory.Integrable f (μ.restrict s)
<VAR>α : Type u_1<VAR>E : Type u_3<VAR>MeasurableSpace α<VAR>NormedAddCommGroup E<VAR>f : α → E<VAR>μ : MeasureTheory.Measure α<GOAL>MeasureTheory.IntegrableOn f ∅ μ
<VAR>α : Type u_1<VAR>E : Type u_3<VAR>MeasurableSpace α<VAR>NormedAddCommGroup E<VAR>f : α → E<VAR>μ : MeasureTheory.Measure α<GOAL>MeasureTheory.IntegrableOn f Set.univ μ ↔ MeasureTheory.Integrable f μ
<VAR>α : Type u_1<VAR>E : Type u_3<VAR>MeasurableSpace α<VAR>NormedAddCommGroup E<VAR>s : Set α<VAR>μ : MeasureTheory.Measure α<GOAL>MeasureTheory.IntegrableOn (fun x => 0) s μ
<VAR>α : Type u_1<VAR>E : Type u_3<VAR>MeasurableSpace α<VAR>NormedAddCommGroup E<VAR>s : Set α<VAR>μ : MeasureTheory.Measure α<VAR>C : E<GOAL>MeasureTheory.IntegrableOn (fun x => C) s μ ↔ C = 0 ∨ μ s < ⊤
<VAR>α : Type u_1<VAR>E : Type u_3<VAR>MeasurableSpace α<VAR>NormedAddCommGroup E<VAR>f : α → E<VAR>s t : Set α<VAR>μ ν : MeasureTheory.Measure α<VAR>h : MeasureTheory.IntegrableOn f t ν<VAR>hs : s ⊆ t<VAR>hμ : μ ≤ ν<GOAL>MeasureTheory.IntegrableOn f s μ
<VAR>α : Type u_1<VAR>E : Type u_3<VAR>MeasurableSpace α<VAR>NormedAddCommGroup E<VAR>f : α → E<VAR>s t : Set α<VAR>μ : MeasureTheory.Measure α<VAR>h : MeasureTheory.IntegrableOn f t μ<VAR>hst : s ⊆ t<GOAL>MeasureTheory.IntegrableOn f s μ
<VAR>α : Type u_1<VAR>E : Type u_3<VAR>MeasurableSpace α<VAR>NormedAddCommGroup E<VAR>f : α → E<VAR>s : Set α<VAR>μ ν : MeasureTheory.Measure α<VAR>h : MeasureTheory.IntegrableOn f s ν<VAR>hμ : μ ≤ ν<GOAL>MeasureTheory.IntegrableOn f s μ
<VAR>α : Type u_1<VAR>E : Type u_3<VAR>MeasurableSpace α<VAR>NormedAddCommGroup E<VAR>f : α → E<VAR>s t : Set α<VAR>μ : MeasureTheory.Measure α<VAR>h : MeasureTheory.IntegrableOn f t μ<VAR>hst : s ≤ᵐ[μ] t<GOAL>MeasureTheory.IntegrableOn f s μ
<VAR>α : Type u_1<VAR>E : Type u_3<VAR>MeasurableSpace α<VAR>NormedAddCommGroup E<VAR>f : α → E<VAR>s t : Set α<VAR>μ : MeasureTheory.Measure α<VAR>h : MeasureTheory.IntegrableOn f t μ<VAR>hst : s =ᵐ[μ] t<GOAL>MeasureTheory.IntegrableOn f s μ
<VAR>α : Type u_1<VAR>E : Type u_3<VAR>MeasurableSpace α<VAR>NormedAddCommGroup E<VAR>f g : α → E<VAR>s : Set α<VAR>μ : MeasureTheory.Measure α<VAR>h : MeasureTheory.IntegrableOn f s μ<VAR>hst : f =ᵐ[μ.restrict s] g<GOAL>MeasureTheory.IntegrableOn g s μ
<VAR>α : Type u_1<VAR>E : Type u_3<VAR>MeasurableSpace α<VAR>NormedAddCommGroup E<VAR>f g : α → E<VAR>s : Set α<VAR>μ : MeasureTheory.Measure α<VAR>hst : f =ᵐ[μ.restrict s] g<GOAL>MeasureTheory.IntegrableOn f s μ ↔ MeasureTheory.IntegrableOn g s μ
<VAR>α : Type u_1<VAR>E : Type u_3<VAR>MeasurableSpace α<VAR>NormedAddCommGroup E<VAR>f g : α → E<VAR>s : Set α<VAR>μ : MeasureTheory.Measure α<VAR>h : MeasureTheory.IntegrableOn f s μ<VAR>hst : Set.EqOn f g s<VAR>hs : MeasurableSet s<GOAL>MeasureTheory.IntegrableOn g s μ
<VAR>α : Type u_1<VAR>E : Type u_3<VAR>MeasurableSpace α<VAR>NormedAddCommGroup E<VAR>f g : α → E<VAR>s : Set α<VAR>μ : MeasureTheory.Measure α<VAR>hst : Set.EqOn f g s<VAR>hs : MeasurableSet s<GOAL>MeasureTheory.IntegrableOn f s μ ↔ MeasureTheory.IntegrableOn g s μ
<VAR>α : Type u_1<VAR>E : Type u_3<VAR>MeasurableSpace α<VAR>NormedAddCommGroup E<VAR>f : α → E<VAR>s : Set α<VAR>μ : MeasureTheory.Measure α<VAR>h : MeasureTheory.Integrable f μ<GOAL>MeasureTheory.IntegrableOn f s μ
<VAR>α : Type u_1<VAR>E : Type u_3<VAR>MeasurableSpace α<VAR>NormedAddCommGroup E<VAR>f : α → E<VAR>s t : Set α<VAR>μ : MeasureTheory.Measure α<VAR>h : MeasureTheory.IntegrableOn f s μ<VAR>hs : MeasurableSet s<GOAL>MeasureTheory.IntegrableOn f s (μ.restrict t)
<VAR>α : Type u_1<VAR>E : Type u_3<VAR>MeasurableSpace α<VAR>NormedAddCommGroup E<VAR>f : α → E<VAR>s t : Set α<VAR>μ : MeasureTheory.Measure α<VAR>h : MeasureTheory.IntegrableOn f s (μ.restrict t)<GOAL>MeasureTheory.IntegrableOn f (s ∩ t) μ
<VAR>α : Type u_1<VAR>E : Type u_3<VAR>MeasurableSpace α<VAR>NormedAddCommGroup E<VAR>f g : α → E<VAR>s : Set α<VAR>μ : MeasureTheory.Measure α<VAR>DecidablePred fun x => x ∈ s<VAR>hs : MeasurableSet s<VAR>hf : MeasureTheory.IntegrableOn f s μ<VAR>hg : MeasureTheory.IntegrableOn g sᶜ μ<GOAL>MeasureTheory.Integrable (s.piecewise f g) μ
<VAR>α : Type u_1<VAR>E : Type u_3<VAR>MeasurableSpace α<VAR>NormedAddCommGroup E<VAR>f : α → E<VAR>s t : Set α<VAR>μ : MeasureTheory.Measure α<VAR>h : MeasureTheory.IntegrableOn f (s ∪ t) μ<GOAL>MeasureTheory.IntegrableOn f s μ
<VAR>α : Type u_1<VAR>E : Type u_3<VAR>MeasurableSpace α<VAR>NormedAddCommGroup E<VAR>f : α → E<VAR>s t : Set α<VAR>μ : MeasureTheory.Measure α<VAR>h : MeasureTheory.IntegrableOn f (s ∪ t) μ<GOAL>MeasureTheory.IntegrableOn f t μ
<VAR>α : Type u_1<VAR>E : Type u_3<VAR>MeasurableSpace α<VAR>NormedAddCommGroup E<VAR>f : α → E<VAR>s t : Set α<VAR>μ : MeasureTheory.Measure α<VAR>hs : MeasureTheory.IntegrableOn f s μ<VAR>ht : MeasureTheory.IntegrableOn f t μ<GOAL>MeasureTheory.IntegrableOn f (s ∪ t) μ
<VAR>α : Type u_1<VAR>E : Type u_3<VAR>MeasurableSpace α<VAR>NormedAddCommGroup E<VAR>f : α → E<VAR>s t : Set α<VAR>μ : MeasureTheory.Measure α<GOAL>MeasureTheory.IntegrableOn f (s ∪ t) μ ↔ MeasureTheory.IntegrableOn f s μ ∧ MeasureTheory.IntegrableOn f t μ
<VAR>α : Type u_1<VAR>E : Type u_3<VAR>MeasurableSpace α<VAR>NormedAddCommGroup E<VAR>f : α → E<VAR>μ : MeasureTheory.Measure α<VAR>x : α<VAR>MeasurableSingletonClass α<GOAL>MeasureTheory.IntegrableOn f {x} μ ↔ f x = 0 ∨ μ {x} < ⊤
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>MeasurableSpace α<VAR>NormedAddCommGroup E<VAR>f : α → E<VAR>μ : MeasureTheory.Measure α<VAR>s : Set β<VAR>hs : s.Finite<VAR>t : β → Set α<GOAL>MeasureTheory.IntegrableOn f (⋃ i ∈ s, t i) μ ↔ ∀ i ∈ s, MeasureTheory.IntegrableOn f (t i) μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>MeasurableSpace α<VAR>NormedAddCommGroup E<VAR>f : α → E<VAR>μ : MeasureTheory.Measure α<VAR>s : Finset β<VAR>t : β → Set α<GOAL>MeasureTheory.IntegrableOn f (⋃ i ∈ s, t i) μ ↔ ∀ i ∈ s, MeasureTheory.IntegrableOn f (t i) μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>MeasurableSpace α<VAR>NormedAddCommGroup E<VAR>f : α → E<VAR>μ : MeasureTheory.Measure α<VAR>Finite β<VAR>t : β → Set α<GOAL>MeasureTheory.IntegrableOn f (⋃ i, t i) μ ↔ ∀ (i : β), MeasureTheory.IntegrableOn f (t i) μ
<VAR>α : Type u_1<VAR>E : Type u_3<VAR>MeasurableSpace α<VAR>NormedAddCommGroup E<VAR>f : α → E<VAR>s : Set α<VAR>μ ν : MeasureTheory.Measure α<VAR>hμ : MeasureTheory.IntegrableOn f s μ<VAR>hν : MeasureTheory.IntegrableOn f s ν<GOAL>MeasureTheory.IntegrableOn f s (μ + ν)
<VAR>α : Type u_1<VAR>E : Type u_3<VAR>MeasurableSpace α<VAR>NormedAddCommGroup E<VAR>f : α → E<VAR>s : Set α<VAR>μ ν : MeasureTheory.Measure α<GOAL>MeasureTheory.IntegrableOn f s (μ + ν) ↔ MeasureTheory.IntegrableOn f s μ ∧ MeasureTheory.IntegrableOn f s ν
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>MeasurableSpace α<VAR>NormedAddCommGroup E<VAR>MeasurableSpace β<VAR>e : α → β<VAR>he : MeasurableEmbedding e<VAR>f : β → E<VAR>μ : MeasureTheory.Measure α<VAR>s : Set β<GOAL>MeasureTheory.IntegrableOn f s (MeasureTheory.Measure.map e μ) ↔ MeasureTheory.IntegrableOn (f ∘ e) (e ⁻¹' s) μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>MeasurableSpace α<VAR>NormedAddCommGroup E<VAR>MeasurableSpace β<VAR>e : α → β<VAR>he : MeasurableEmbedding e<VAR>f : β → E<VAR>μ : MeasureTheory.Measure β<VAR>s : Set β<VAR>hs : s ⊆ Set.range e<GOAL>MeasureTheory.IntegrableOn f s μ ↔ MeasureTheory.IntegrableOn (f ∘ e) (e ⁻¹' s) (MeasureTheory.Measure.comap e μ)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>MeasurableSpace α<VAR>NormedAddCommGroup E<VAR>MeasurableSpace β<VAR>e : α ≃ᵐ β<VAR>f : β → E<VAR>μ : MeasureTheory.Measure α<VAR>s : Set β<GOAL>MeasureTheory.IntegrableOn f s (MeasureTheory.Measure.map (⇑e) μ) ↔ MeasureTheory.IntegrableOn (f ∘ ⇑e) (⇑e ⁻¹' s) μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>MeasurableSpace α<VAR>NormedAddCommGroup E<VAR>μ : MeasureTheory.Measure α<VAR>MeasurableSpace β<VAR>e : α → β<VAR>ν : MeasureTheory.Measure β<VAR>h₁ : MeasureTheory.MeasurePreserving e μ ν<VAR>h₂ : MeasurableEmbedding e<VAR>f : β → E<VAR>s : Set β<GOAL>MeasureTheory.IntegrableOn (f ∘ e) (e ⁻¹' s) μ ↔ MeasureTheory.IntegrableOn f s ν
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>MeasurableSpace α<VAR>NormedAddCommGroup E<VAR>μ : MeasureTheory.Measure α<VAR>MeasurableSpace β<VAR>e : α → β<VAR>ν : MeasureTheory.Measure β<VAR>h₁ : MeasureTheory.MeasurePreserving e μ ν<VAR>h₂ : MeasurableEmbedding e<VAR>f : β → E<VAR>s : Set α<GOAL>MeasureTheory.IntegrableOn f (e '' s) ν ↔ MeasureTheory.IntegrableOn (f ∘ e) s μ
<VAR>α : Type u_1<VAR>E : Type u_3<VAR>MeasurableSpace α<VAR>NormedAddCommGroup E<VAR>f : α → E<VAR>s : Set α<VAR>μ : MeasureTheory.Measure α<VAR>hs : MeasurableSet s<GOAL>MeasureTheory.Integrable (s.indicator f) μ ↔ MeasureTheory.IntegrableOn f s μ
<VAR>α : Type u_1<VAR>E : Type u_3<VAR>MeasurableSpace α<VAR>NormedAddCommGroup E<VAR>f : α → E<VAR>s : Set α<VAR>μ : MeasureTheory.Measure α<VAR>h : MeasureTheory.IntegrableOn f s μ<VAR>hs : MeasurableSet s<GOAL>MeasureTheory.Integrable (s.indicator f) μ
<VAR>α : Type u_1<VAR>E : Type u_3<VAR>MeasurableSpace α<VAR>NormedAddCommGroup E<VAR>f : α → E<VAR>s : Set α<VAR>μ : MeasureTheory.Measure α<VAR>h : MeasureTheory.Integrable f μ<VAR>hs : MeasurableSet s<GOAL>MeasureTheory.Integrable (s.indicator f) μ
<VAR>α : Type u_1<VAR>E : Type u_3<VAR>MeasurableSpace α<VAR>NormedAddCommGroup E<VAR>f : α → E<VAR>s t : Set α<VAR>μ : MeasureTheory.Measure α<VAR>h : MeasureTheory.IntegrableOn f s μ<VAR>ht : MeasurableSet t<GOAL>MeasureTheory.IntegrableOn (t.indicator f) s μ
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>E : Type u_5<VAR>NormedAddCommGroup E<VAR>p : ℝ≥0∞<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>hμs : μ s ≠ ⊤<VAR>c : E<GOAL>MeasureTheory.Integrable (↑↑(MeasureTheory.indicatorConstLp p hs hμs c)) μ
<VAR>α : Type u_1<VAR>E : Type u_3<VAR>MeasurableSpace α<VAR>NormedAddCommGroup E<VAR>f : α → E<VAR>s : Set α<VAR>μ : MeasureTheory.Measure α<VAR>hf : MeasureTheory.IntegrableOn f s μ<VAR>h's : ∀ x ∈ s, f x ≠ 0<GOAL>μ.restrict (MeasureTheory.toMeasurable μ s) = μ.restrict s
<VAR>α : Type u_1<VAR>E : Type u_3<VAR>MeasurableSpace α<VAR>NormedAddCommGroup E<VAR>f : α → E<VAR>s t : Set α<VAR>μ : MeasureTheory.Measure α<VAR>hf : MeasureTheory.IntegrableOn f s μ<VAR>ht : MeasureTheory.NullMeasurableSet t μ<VAR>h't : ∀ᵐ (x : α) ∂μ, x ∈ t \ s → f x = 0<GOAL>MeasureTheory.IntegrableOn f t μ
<VAR>α : Type u_1<VAR>E : Type u_3<VAR>MeasurableSpace α<VAR>NormedAddCommGroup E<VAR>f : α → E<VAR>s t : Set α<VAR>μ : MeasureTheory.Measure α<VAR>hf : MeasureTheory.IntegrableOn f s μ<VAR>ht : MeasurableSet t<VAR>h't : ∀ x ∈ t \ s, f x = 0<GOAL>MeasureTheory.IntegrableOn f t μ
<VAR>α : Type u_1<VAR>E : Type u_3<VAR>MeasurableSpace α<VAR>NormedAddCommGroup E<VAR>f : α → E<VAR>s : Set α<VAR>μ : MeasureTheory.Measure α<VAR>hf : MeasureTheory.IntegrableOn f s μ<VAR>h't : ∀ᵐ (x : α) ∂μ, x ∉ s → f x = 0<GOAL>MeasureTheory.Integrable f μ
<VAR>α : Type u_1<VAR>E : Type u_3<VAR>MeasurableSpace α<VAR>NormedAddCommGroup E<VAR>f : α → E<VAR>s : Set α<VAR>μ : MeasureTheory.Measure α<VAR>hf : MeasureTheory.IntegrableOn f s μ<VAR>h't : ∀ x ∉ s, f x = 0<GOAL>MeasureTheory.Integrable f μ
<VAR>α : Type u_1<VAR>E : Type u_3<VAR>MeasurableSpace α<VAR>NormedAddCommGroup E<VAR>f : α → E<VAR>s : Set α<VAR>μ : MeasureTheory.Measure α<VAR>h1s : Function.support f ⊆ s<GOAL>MeasureTheory.IntegrableOn f s μ ↔ MeasureTheory.Integrable f μ
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>E : Type u_5<VAR>NormedAddCommGroup E<VAR>p : ℝ≥0∞<VAR>s : Set α<VAR>f : ↥(MeasureTheory.Lp E p μ)<VAR>hp : 1 ≤ p<VAR>hμs : μ s ≠ ⊤<GOAL>MeasureTheory.IntegrableOn (↑↑f) s μ
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f : α → ℝ<VAR>hf : MeasureTheory.Integrable f μ<GOAL>∫⁻ (x : α), ENNReal.ofReal (f x) ∂μ < ⊤
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f : α → ℝ<VAR>s : Set α<VAR>hf : MeasureTheory.IntegrableOn f s μ<GOAL>∫⁻ (x : α) in s, ENNReal.ofReal (f x) ∂μ < ⊤
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>MeasurableSpace α<VAR>NormedAddCommGroup E<VAR>μ : MeasureTheory.Measure α<VAR>l : Filter α<VAR>MeasurableSpace β<VAR>e : α → β<VAR>he : MeasurableEmbedding e<VAR>f : β → E<GOAL>MeasureTheory.IntegrableAtFilter f (Filter.map e l) (MeasureTheory.Measure.map e μ) ↔ MeasureTheory.IntegrableAtFilter (f ∘ e) l μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>MeasurableSpace α<VAR>NormedAddCommGroup E<VAR>l : Filter α<VAR>MeasurableSpace β<VAR>e : α → β<VAR>he : MeasurableEmbedding e<VAR>f : β → E<VAR>μ : MeasureTheory.Measure β<GOAL>MeasureTheory.IntegrableAtFilter f (Filter.map e l) μ ↔ MeasureTheory.IntegrableAtFilter (f ∘ e) l (MeasureTheory.Measure.comap e μ)
<VAR>α : Type u_1<VAR>E : Type u_3<VAR>MeasurableSpace α<VAR>NormedAddCommGroup E<VAR>f : α → E<VAR>μ : MeasureTheory.Measure α<VAR>h : MeasureTheory.Integrable f μ<VAR>l : Filter α<GOAL>MeasureTheory.IntegrableAtFilter f l μ
<VAR>α : Type u_1<VAR>E : Type u_3<VAR>MeasurableSpace α<VAR>NormedAddCommGroup E<VAR>f : α → E<VAR>μ : MeasureTheory.Measure α<VAR>l : Filter α<VAR>h : MeasureTheory.IntegrableAtFilter f l μ<GOAL>∀ᶠ (s : Set α) in l.smallSets, MeasureTheory.IntegrableOn f s μ
<VAR>α : Type u_1<VAR>E : Type u_3<VAR>MeasurableSpace α<VAR>NormedAddCommGroup E<VAR>μ : MeasureTheory.Measure α<VAR>l : Filter α<VAR>f g : α → E<VAR>hf : MeasureTheory.IntegrableAtFilter f l μ<VAR>hg : MeasureTheory.IntegrableAtFilter g l μ<GOAL>MeasureTheory.IntegrableAtFilter (f + g) l μ
<VAR>α : Type u_1<VAR>E : Type u_3<VAR>MeasurableSpace α<VAR>NormedAddCommGroup E<VAR>μ : MeasureTheory.Measure α<VAR>l : Filter α<VAR>f : α → E<VAR>hf : MeasureTheory.IntegrableAtFilter f l μ<GOAL>MeasureTheory.IntegrableAtFilter (-f) l μ
<VAR>α : Type u_1<VAR>E : Type u_3<VAR>MeasurableSpace α<VAR>NormedAddCommGroup E<VAR>μ : MeasureTheory.Measure α<VAR>l : Filter α<VAR>f g : α → E<VAR>hf : MeasureTheory.IntegrableAtFilter f l μ<VAR>hg : MeasureTheory.IntegrableAtFilter g l μ<GOAL>MeasureTheory.IntegrableAtFilter (f - g) l μ
<VAR>α : Type u_1<VAR>E : Type u_3<VAR>MeasurableSpace α<VAR>NormedAddCommGroup E<VAR>μ : MeasureTheory.Measure α<VAR>l : Filter α<VAR>𝕜 : Type u_5<VAR>NormedAddCommGroup 𝕜<VAR>SMulZeroClass 𝕜 E<VAR>BoundedSMul 𝕜 E<VAR>f : α → E<VAR>hf : MeasureTheory.IntegrableAtFilter f l μ<VAR>c : 𝕜<GOAL>MeasureTheory.IntegrableAtFilter (c • f) l μ
<VAR>α : Type u_1<VAR>E : Type u_3<VAR>MeasurableSpace α<VAR>NormedAddCommGroup E<VAR>f : α → E<VAR>μ : MeasureTheory.Measure α<VAR>l : Filter α<VAR>hf : MeasureTheory.IntegrableAtFilter f l μ<GOAL>MeasureTheory.IntegrableAtFilter (fun x => ‖f x‖) l μ
<VAR>α : Type u_1<VAR>E : Type u_3<VAR>MeasurableSpace α<VAR>NormedAddCommGroup E<VAR>f : α → E<VAR>μ : MeasureTheory.Measure α<VAR>l l' : Filter α<VAR>hl : l ≤ l'<VAR>hl' : MeasureTheory.IntegrableAtFilter f l' μ<GOAL>MeasureTheory.IntegrableAtFilter f l μ
<VAR>α : Type u_1<VAR>E : Type u_3<VAR>MeasurableSpace α<VAR>NormedAddCommGroup E<VAR>f : α → E<VAR>μ : MeasureTheory.Measure α<VAR>l l' : Filter α<VAR>hl : MeasureTheory.IntegrableAtFilter f l μ<GOAL>MeasureTheory.IntegrableAtFilter f (l ⊓ l') μ
<VAR>α : Type u_1<VAR>E : Type u_3<VAR>MeasurableSpace α<VAR>NormedAddCommGroup E<VAR>f : α → E<VAR>μ : MeasureTheory.Measure α<VAR>l l' : Filter α<VAR>hl : MeasureTheory.IntegrableAtFilter f l μ<GOAL>MeasureTheory.IntegrableAtFilter f (l' ⊓ l) μ
<VAR>α : Type u_1<VAR>E : Type u_3<VAR>MeasurableSpace α<VAR>NormedAddCommGroup E<VAR>f : α → E<VAR>μ : MeasureTheory.Measure α<VAR>l : Filter α<GOAL>MeasureTheory.IntegrableAtFilter f (l ⊓ MeasureTheory.ae μ) μ ↔ MeasureTheory.IntegrableAtFilter f l μ
<VAR>α : Type u_1<VAR>E : Type u_3<VAR>MeasurableSpace α<VAR>NormedAddCommGroup E<VAR>f : α → E<VAR>μ : MeasureTheory.Measure α<GOAL>MeasureTheory.IntegrableAtFilter f ⊤ μ ↔ MeasureTheory.Integrable f μ
<VAR>α : Type u_1<VAR>E : Type u_3<VAR>MeasurableSpace α<VAR>NormedAddCommGroup E<VAR>f : α → E<VAR>μ : MeasureTheory.Measure α<VAR>l l' : Filter α<GOAL>MeasureTheory.IntegrableAtFilter f (l ⊔ l') μ ↔ MeasureTheory.IntegrableAtFilter f l μ ∧ MeasureTheory.IntegrableAtFilter f l' μ
<VAR>α : Type u_1<VAR>E : Type u_3<VAR>MeasurableSpace α<VAR>NormedAddCommGroup E<VAR>f : α → E<VAR>μ : MeasureTheory.Measure α<VAR>l : Filter α<VAR>l.IsMeasurablyGenerated<VAR>hfm : StronglyMeasurableAtFilter f l μ<VAR>hμ : μ.FiniteAtFilter l<VAR>hf : Filter.IsBoundedUnder (fun x x_1 => x ≤ x_1) l (norm ∘ f)<GOAL>MeasureTheory.IntegrableAtFilter f l μ
<VAR>α : Type u_1<VAR>E : Type u_3<VAR>MeasurableSpace α<VAR>NormedAddCommGroup E<VAR>f : α → E<VAR>μ : MeasureTheory.Measure α<VAR>l : Filter α<VAR>l.IsMeasurablyGenerated<VAR>hfm : StronglyMeasurableAtFilter f l μ<VAR>hμ : μ.FiniteAtFilter l<VAR>b : E<VAR>hf : Filter.Tendsto f (l ⊓ MeasureTheory.ae μ) (𝓝 b)<GOAL>MeasureTheory.IntegrableAtFilter f l μ
<VAR>α : Type u_1<VAR>E : Type u_3<VAR>MeasurableSpace α<VAR>NormedAddCommGroup E<VAR>f : α → E<VAR>μ : MeasureTheory.Measure α<VAR>l : Filter α<VAR>l.IsMeasurablyGenerated<VAR>hfm : StronglyMeasurableAtFilter f l μ<VAR>hμ : μ.FiniteAtFilter l<VAR>b : E<VAR>hf : Filter.Tendsto f l (𝓝 b)<GOAL>MeasureTheory.IntegrableAtFilter f l μ
<VAR>α : Type u_1<VAR>E : Type u_3<VAR>MeasurableSpace α<VAR>NormedAddCommGroup E<VAR>f : α → E<VAR>s : Set α<VAR>μ : MeasureTheory.Measure α<VAR>s_finite : μ s ≠ ⊤<VAR>f_mble : MeasureTheory.AEStronglyMeasurable f μ<VAR>M : ℝ<VAR>f_bdd : ∀ᵐ (a : α) ∂μ.restrict s, ‖f a‖ ≤ M<GOAL>MeasureTheory.IntegrableOn f s μ
<VAR>α : Type u_1<VAR>E : Type u_3<VAR>MeasurableSpace α<VAR>NormedAddCommGroup E<VAR>μ : MeasureTheory.Measure α<VAR>f g : α → E<VAR>h : Disjoint (Function.support f) (Function.support g)<VAR>hf : MeasureTheory.StronglyMeasurable f<VAR>hg : MeasureTheory.StronglyMeasurable g<GOAL>MeasureTheory.Integrable (f + g) μ ↔ MeasureTheory.Integrable f μ ∧ MeasureTheory.Integrable g μ
<VAR>α : Type u_1<VAR>E : Type u_3<VAR>MeasurableSpace α<VAR>NormedAddCommGroup E<VAR>f : α → E<VAR>μ : MeasureTheory.Measure α<VAR>l : Filter α<VAR>h : MeasureTheory.IntegrableAtFilter f l μ<VAR>h' : ∀ s ∈ l, μ s = ⊤<VAR>a : E<VAR>hf : Filter.Tendsto f l (𝓝 a)<GOAL>a = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>MeasurableSpace α<VAR>TopologicalSpace α<VAR>OpensMeasurableSpace α<VAR>MeasurableSpace β<VAR>TopologicalSpace β<VAR>BorelSpace β<VAR>f : α → β<VAR>s : Set α<VAR>μ : MeasureTheory.Measure α<VAR>hf : ContinuousOn f s<VAR>hs : MeasurableSet s<GOAL>AEMeasurable f (μ.restrict s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>MeasurableSpace α<VAR>TopologicalSpace α<VAR>TopologicalSpace.PseudoMetrizableSpace α<VAR>OpensMeasurableSpace α<VAR>TopologicalSpace β<VAR>TopologicalSpace.PseudoMetrizableSpace β<VAR>f : α → β<VAR>s : Set α<VAR>μ : MeasureTheory.Measure α<VAR>hf : ContinuousOn f s<VAR>hs : MeasurableSet s<VAR>h's : TopologicalSpace.IsSeparable s<GOAL>MeasureTheory.AEStronglyMeasurable f (μ.restrict s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>MeasurableSpace α<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>h : SecondCountableTopologyEither α β<VAR>OpensMeasurableSpace α<VAR>TopologicalSpace.PseudoMetrizableSpace β<VAR>f : α → β<VAR>s : Set α<VAR>μ : MeasureTheory.Measure α<VAR>hf : ContinuousOn f s<VAR>hs : MeasurableSet s<GOAL>MeasureTheory.AEStronglyMeasurable f (μ.restrict s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>MeasurableSpace α<VAR>TopologicalSpace α<VAR>OpensMeasurableSpace α<VAR>TopologicalSpace β<VAR>TopologicalSpace.PseudoMetrizableSpace β<VAR>f : α → β<VAR>s : Set α<VAR>μ : MeasureTheory.Measure α<VAR>hf : ContinuousOn f s<VAR>hs : IsCompact s<VAR>h's : MeasurableSet s<GOAL>MeasureTheory.AEStronglyMeasurable f (μ.restrict s)
<VAR>α : Type u_1<VAR>E : Type u_3<VAR>MeasurableSpace α<VAR>NormedAddCommGroup E<VAR>TopologicalSpace α<VAR>TopologicalSpace.PseudoMetrizableSpace α<VAR>OpensMeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>MeasureTheory.IsLocallyFiniteMeasure μ<VAR>a : α<VAR>t : Set α<VAR>f : α → E<VAR>hft : ContinuousOn f t<VAR>ht : MeasurableSet t<VAR>h't : TopologicalSpace.IsSeparable t<VAR>ha : a ∈ t<GOAL>MeasureTheory.IntegrableAtFilter f (𝓝[t] a) μ
<VAR>α : Type u_1<VAR>E : Type u_3<VAR>MeasurableSpace α<VAR>NormedAddCommGroup E<VAR>TopologicalSpace α<VAR>SecondCountableTopologyEither α E<VAR>OpensMeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>MeasureTheory.IsLocallyFiniteMeasure μ<VAR>a : α<VAR>t : Set α<VAR>f : α → E<VAR>hft : ContinuousOn f t<VAR>ht : MeasurableSet t<VAR>ha : a ∈ t<GOAL>MeasureTheory.IntegrableAtFilter f (𝓝[t] a) μ
<VAR>α : Type u_1<VAR>E : Type u_3<VAR>MeasurableSpace α<VAR>NormedAddCommGroup E<VAR>TopologicalSpace α<VAR>SecondCountableTopologyEither α E<VAR>OpensMeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>MeasureTheory.IsLocallyFiniteMeasure μ<VAR>f : α → E<VAR>hf : Continuous f<VAR>a : α<GOAL>MeasureTheory.IntegrableAtFilter f (𝓝 a) μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>MeasurableSpace α<VAR>TopologicalSpace α<VAR>OpensMeasurableSpace α<VAR>TopologicalSpace β<VAR>TopologicalSpace.PseudoMetrizableSpace β<VAR>SecondCountableTopologyEither α β<VAR>f : α → β<VAR>s : Set α<VAR>μ : MeasureTheory.Measure α<VAR>hs : IsOpen s<VAR>hf : ContinuousOn f s<VAR>x : α<GOAL>x ∈ s → StronglyMeasurableAtFilter f (𝓝 x) μ
<VAR>α : Type u_1<VAR>E : Type u_3<VAR>MeasurableSpace α<VAR>NormedAddCommGroup E<VAR>TopologicalSpace α<VAR>OpensMeasurableSpace α<VAR>SecondCountableTopologyEither α E<VAR>f : α → E<VAR>s : Set α<VAR>μ : MeasureTheory.Measure α<VAR>hs : IsOpen s<VAR>hf : ∀ x ∈ s, ContinuousAt f x<VAR>x : α<GOAL>x ∈ s → StronglyMeasurableAtFilter f (𝓝 x) μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>MeasurableSpace α<VAR>TopologicalSpace α<VAR>OpensMeasurableSpace α<VAR>TopologicalSpace β<VAR>TopologicalSpace.PseudoMetrizableSpace β<VAR>SecondCountableTopologyEither α β<VAR>f : α → β<VAR>hf : Continuous f<VAR>μ : MeasureTheory.Measure α<VAR>l : Filter α<GOAL>StronglyMeasurableAtFilter f l μ
<VAR>α : Type u_5<VAR>β : Type u_6<VAR>MeasurableSpace α<VAR>TopologicalSpace α<VAR>OpensMeasurableSpace α<VAR>TopologicalSpace β<VAR>TopologicalSpace.PseudoMetrizableSpace β<VAR>SecondCountableTopologyEither α β<VAR>f : α → β<VAR>s : Set α<VAR>μ : MeasureTheory.Measure α<VAR>hf : ContinuousOn f s<VAR>hs : MeasurableSet s<VAR>x : α<GOAL>StronglyMeasurableAtFilter f (𝓝[s] x) μ
<VAR>α : Type u_1<VAR>E : Type u_3<VAR>MeasurableSpace α<VAR>NormedAddCommGroup E<VAR>PartialOrder α<VAR>MeasurableSingletonClass α<VAR>f : α → E<VAR>μ : MeasureTheory.Measure α<VAR>a b : α<VAR>ha : μ {a} ≠ ⊤<GOAL>MeasureTheory.IntegrableOn f (Set.Icc a b) μ ↔ MeasureTheory.IntegrableOn f (Set.Ioc a b) μ