ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>X : Type u_1<VAR>E : Type u_3<VAR>F : Type u_4<VAR>MeasurableSpace X<VAR>TopologicalSpace X<VAR>NormedAddCommGroup E<VAR>NormedAddCommGroup F<VAR>f : X → E<VAR>μ : MeasureTheory.Measure X<VAR>hf : MeasureTheory.LocallyIntegrable f μ<VAR>g : X → F<VAR>hg : MeasureTheory.AEStronglyMeasurable g μ<VAR>h : ∀ᵐ (x : X) ∂μ, ‖g x‖ ≤ ‖f x‖<GOAL>MeasureTheory.LocallyIntegrable g μ
<VAR>X : Type u_1<VAR>E : Type u_3<VAR>MeasurableSpace X<VAR>TopologicalSpace X<VAR>NormedAddCommGroup E<VAR>f : X → E<VAR>μ : MeasureTheory.Measure X<VAR>s : Set X<VAR>OpensMeasurableSpace X<VAR>hf : MeasureTheory.LocallyIntegrable f (μ.restrict s)<GOAL>MeasureTheory.LocallyIntegrableOn f s μ
<VAR>X : Type u_1<VAR>E : Type u_3<VAR>MeasurableSpace X<VAR>TopologicalSpace X<VAR>NormedAddCommGroup E<VAR>f : X → E<VAR>μ : MeasureTheory.Measure X<VAR>s : Set X<VAR>OpensMeasurableSpace X<VAR>hs : IsClosed s<GOAL>MeasureTheory.LocallyIntegrableOn f s μ ↔ MeasureTheory.LocallyIntegrable f (μ.restrict s)
<VAR>X : Type u_1<VAR>E : Type u_3<VAR>MeasurableSpace X<VAR>TopologicalSpace X<VAR>NormedAddCommGroup E<VAR>f : X → E<VAR>μ : MeasureTheory.Measure X<VAR>k : Set X<VAR>hf : MeasureTheory.LocallyIntegrable f μ<VAR>hk : IsCompact k<GOAL>MeasureTheory.IntegrableOn f k μ
<VAR>X : Type u_1<VAR>E : Type u_3<VAR>MeasurableSpace X<VAR>TopologicalSpace X<VAR>NormedAddCommGroup E<VAR>f : X → E<VAR>μ : MeasureTheory.Measure X<VAR>hf : MeasureTheory.LocallyIntegrable f μ<VAR>k : Set X<VAR>hk : IsCompact k<GOAL>∃ u, IsOpen u ∧ k ⊆ u ∧ MeasureTheory.IntegrableOn f u μ
<VAR>X : Type u_1<VAR>E : Type u_3<VAR>MeasurableSpace X<VAR>TopologicalSpace X<VAR>NormedAddCommGroup E<VAR>f : X → E<VAR>μ : MeasureTheory.Measure X<VAR>LocallyCompactSpace X<GOAL>MeasureTheory.LocallyIntegrable f μ ↔ ∀ (k : Set X), IsCompact k → MeasureTheory.IntegrableOn f k μ
<VAR>X : Type u_1<VAR>E : Type u_3<VAR>MeasurableSpace X<VAR>TopologicalSpace X<VAR>NormedAddCommGroup E<VAR>f : X → E<VAR>μ : MeasureTheory.Measure X<VAR>SecondCountableTopology X<VAR>hf : MeasureTheory.LocallyIntegrable f μ<GOAL>MeasureTheory.AEStronglyMeasurable f μ
<VAR>X : Type u_1<VAR>E : Type u_3<VAR>MeasurableSpace X<VAR>TopologicalSpace X<VAR>NormedAddCommGroup E<VAR>f : X → E<VAR>μ : MeasureTheory.Measure X<VAR>SecondCountableTopology X<VAR>hf : MeasureTheory.LocallyIntegrable f μ<GOAL>∃ u, (∀ (n : ℕ), IsOpen (u n)) ∧ ⋃ n, u n = Set.univ ∧ ∀ (n : ℕ), MeasureTheory.IntegrableOn f (u n) μ
<VAR>X : Type u_1<VAR>E : Type u_3<VAR>MeasurableSpace X<VAR>TopologicalSpace X<VAR>NormedAddCommGroup E<VAR>μ : MeasureTheory.Measure X<VAR>MeasureTheory.IsLocallyFiniteMeasure μ<VAR>f : X → E<VAR>p : ℝ≥0∞<VAR>hf : MeasureTheory.Memℒp f p μ<VAR>hp : 1 ≤ p<GOAL>MeasureTheory.LocallyIntegrable f μ
<VAR>X : Type u_1<VAR>E : Type u_3<VAR>MeasurableSpace X<VAR>TopologicalSpace X<VAR>NormedAddCommGroup E<VAR>μ : MeasureTheory.Measure X<VAR>MeasureTheory.IsLocallyFiniteMeasure μ<VAR>c : E<GOAL>MeasureTheory.LocallyIntegrable (fun x => c) μ
<VAR>X : Type u_1<VAR>E : Type u_3<VAR>MeasurableSpace X<VAR>TopologicalSpace X<VAR>NormedAddCommGroup E<VAR>μ : MeasureTheory.Measure X<VAR>s : Set X<VAR>MeasureTheory.IsLocallyFiniteMeasure μ<VAR>c : E<GOAL>MeasureTheory.LocallyIntegrableOn (fun x => c) s μ
<VAR>X : Type u_1<VAR>E : Type u_3<VAR>MeasurableSpace X<VAR>TopologicalSpace X<VAR>NormedAddCommGroup E<VAR>μ : MeasureTheory.Measure X<GOAL>MeasureTheory.LocallyIntegrable (fun x => 0) μ
<VAR>X : Type u_1<VAR>E : Type u_3<VAR>MeasurableSpace X<VAR>TopologicalSpace X<VAR>NormedAddCommGroup E<VAR>μ : MeasureTheory.Measure X<VAR>s : Set X<GOAL>MeasureTheory.LocallyIntegrableOn (fun x => 0) s μ
<VAR>X : Type u_1<VAR>E : Type u_3<VAR>MeasurableSpace X<VAR>TopologicalSpace X<VAR>NormedAddCommGroup E<VAR>f : X → E<VAR>μ : MeasureTheory.Measure X<VAR>hf : MeasureTheory.LocallyIntegrable f μ<VAR>s : Set X<VAR>hs : MeasurableSet s<GOAL>MeasureTheory.LocallyIntegrable (s.indicator f) μ
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>E : Type u_3<VAR>MeasurableSpace X<VAR>TopologicalSpace X<VAR>MeasurableSpace Y<VAR>TopologicalSpace Y<VAR>NormedAddCommGroup E<VAR>BorelSpace X<VAR>BorelSpace Y<VAR>e : X ≃ₜ Y<VAR>f : Y → E<VAR>μ : MeasureTheory.Measure X<GOAL>MeasureTheory.LocallyIntegrable f (MeasureTheory.Measure.map (⇑e) μ) ↔ MeasureTheory.LocallyIntegrable (f ∘ ⇑e) μ
<VAR>X : Type u_1<VAR>E : Type u_3<VAR>MeasurableSpace X<VAR>TopologicalSpace X<VAR>NormedAddCommGroup E<VAR>f g : X → E<VAR>μ : MeasureTheory.Measure X<VAR>hf : MeasureTheory.LocallyIntegrable f μ<VAR>hg : MeasureTheory.LocallyIntegrable g μ<GOAL>MeasureTheory.LocallyIntegrable (f + g) μ
<VAR>X : Type u_1<VAR>E : Type u_3<VAR>MeasurableSpace X<VAR>TopologicalSpace X<VAR>NormedAddCommGroup E<VAR>f g : X → E<VAR>μ : MeasureTheory.Measure X<VAR>hf : MeasureTheory.LocallyIntegrable f μ<VAR>hg : MeasureTheory.LocallyIntegrable g μ<GOAL>MeasureTheory.LocallyIntegrable (f - g) μ
<VAR>X : Type u_1<VAR>E : Type u_3<VAR>MeasurableSpace X<VAR>TopologicalSpace X<VAR>NormedAddCommGroup E<VAR>f : X → E<VAR>μ : MeasureTheory.Measure X<VAR>hf : MeasureTheory.LocallyIntegrable f μ<GOAL>MeasureTheory.LocallyIntegrable (-f) μ
<VAR>X : Type u_1<VAR>E : Type u_3<VAR>MeasurableSpace X<VAR>TopologicalSpace X<VAR>NormedAddCommGroup E<VAR>f : X → E<VAR>μ : MeasureTheory.Measure X<VAR>𝕜 : Type u_6<VAR>NormedAddCommGroup 𝕜<VAR>SMulZeroClass 𝕜 E<VAR>BoundedSMul 𝕜 E<VAR>hf : MeasureTheory.LocallyIntegrable f μ<VAR>c : 𝕜<GOAL>MeasureTheory.LocallyIntegrable (c • f) μ
<VAR>X : Type u_1<VAR>E : Type u_3<VAR>MeasurableSpace X<VAR>TopologicalSpace X<VAR>NormedAddCommGroup E<VAR>μ : MeasureTheory.Measure X<VAR>ι : Type u_6<VAR>s : Finset ι<VAR>f : ι → X → E<VAR>hf : ∀ i ∈ s, MeasureTheory.LocallyIntegrable (f i) μ<GOAL>MeasureTheory.LocallyIntegrable (∑ i ∈ s, f i) μ
<VAR>X : Type u_1<VAR>E : Type u_3<VAR>MeasurableSpace X<VAR>TopologicalSpace X<VAR>NormedAddCommGroup E<VAR>μ : MeasureTheory.Measure X<VAR>ι : Type u_6<VAR>s : Finset ι<VAR>f : ι → X → E<VAR>hf : ∀ i ∈ s, MeasureTheory.LocallyIntegrable (f i) μ<GOAL>MeasureTheory.LocallyIntegrable (fun a => ∑ i ∈ s, f i a) μ
<VAR>X : Type u_1<VAR>E : Type u_3<VAR>MeasurableSpace X<VAR>TopologicalSpace X<VAR>NormedAddCommGroup E<VAR>f : X → E<VAR>μ : MeasureTheory.Measure X<VAR>NormedSpace ℝ E<VAR>OpensMeasurableSpace X<VAR>T2Space X<VAR>hf : MeasureTheory.LocallyIntegrable f μ<VAR>g : X → ℝ<VAR>hg : Continuous g<VAR>h'g : HasCompactSupport g<GOAL>MeasureTheory.Integrable (fun x => g x • f x) μ
<VAR>X : Type u_1<VAR>E : Type u_3<VAR>MeasurableSpace X<VAR>TopologicalSpace X<VAR>NormedAddCommGroup E<VAR>μ : MeasureTheory.Measure X<VAR>NormedSpace ℝ E<VAR>OpensMeasurableSpace X<VAR>T2Space X<VAR>f : X → ℝ<VAR>hf : MeasureTheory.LocallyIntegrable f μ<VAR>g : X → E<VAR>hg : Continuous g<VAR>h'g : HasCompactSupport g<GOAL>MeasureTheory.Integrable (fun x => f x • g x) μ
<VAR>X : Type u_1<VAR>E : Type u_3<VAR>MeasurableSpace X<VAR>TopologicalSpace X<VAR>NormedAddCommGroup E<VAR>f : X → E<VAR>μ : MeasureTheory.Measure X<GOAL>MeasureTheory.Integrable f μ ↔ MeasureTheory.IntegrableAtFilter f (Filter.cocompact X) μ ∧ MeasureTheory.LocallyIntegrable f μ
<VAR>X : Type u_1<VAR>E : Type u_3<VAR>MeasurableSpace X<VAR>TopologicalSpace X<VAR>NormedAddCommGroup E<VAR>f : X → E<VAR>μ : MeasureTheory.Measure X<VAR>LinearOrder X<VAR>CompactIccSpace X<GOAL>MeasureTheory.Integrable f μ ↔ (MeasureTheory.IntegrableAtFilter f Filter.atBot μ ∧ MeasureTheory.IntegrableAtFilter f Filter.atTop μ) ∧ MeasureTheory.LocallyIntegrable f μ
<VAR>X : Type u_1<VAR>E : Type u_3<VAR>MeasurableSpace X<VAR>TopologicalSpace X<VAR>NormedAddCommGroup E<VAR>f : X → E<VAR>μ : MeasureTheory.Measure X<VAR>LinearOrder X<VAR>OrderTop X<VAR>CompactIccSpace X<GOAL>MeasureTheory.Integrable f μ ↔ MeasureTheory.IntegrableAtFilter f Filter.atBot μ ∧ MeasureTheory.LocallyIntegrable f μ
<VAR>X : Type u_1<VAR>E : Type u_3<VAR>MeasurableSpace X<VAR>TopologicalSpace X<VAR>NormedAddCommGroup E<VAR>f : X → E<VAR>μ : MeasureTheory.Measure X<VAR>LinearOrder X<VAR>OrderBot X<VAR>CompactIccSpace X<GOAL>MeasureTheory.Integrable f μ ↔ MeasureTheory.IntegrableAtFilter f Filter.atTop μ ∧ MeasureTheory.LocallyIntegrable f μ
<VAR>X : Type u_1<VAR>E : Type u_3<VAR>MeasurableSpace X<VAR>TopologicalSpace X<VAR>NormedAddCommGroup E<VAR>f : X → E<VAR>μ : MeasureTheory.Measure X<VAR>a : X<VAR>LinearOrder X<VAR>CompactIccSpace X<GOAL>MeasureTheory.IntegrableOn f (Set.Iic a) μ ↔ MeasureTheory.IntegrableAtFilter f Filter.atBot μ ∧ MeasureTheory.LocallyIntegrableOn f (Set.Iic a) μ
<VAR>X : Type u_1<VAR>E : Type u_3<VAR>MeasurableSpace X<VAR>TopologicalSpace X<VAR>NormedAddCommGroup E<VAR>f : X → E<VAR>μ : MeasureTheory.Measure X<VAR>a : X<VAR>LinearOrder X<VAR>CompactIccSpace X<GOAL>MeasureTheory.IntegrableOn f (Set.Ici a) μ ↔ MeasureTheory.IntegrableAtFilter f Filter.atTop μ ∧ MeasureTheory.LocallyIntegrableOn f (Set.Ici a) μ
<VAR>X : Type u_1<VAR>E : Type u_3<VAR>MeasurableSpace X<VAR>TopologicalSpace X<VAR>NormedAddCommGroup E<VAR>f : X → E<VAR>μ : MeasureTheory.Measure X<VAR>a : X<VAR>LinearOrder X<VAR>CompactIccSpace X<VAR>NoMinOrder X<VAR>OrderTopology X<GOAL>MeasureTheory.IntegrableOn f (Set.Iio a) μ ↔ MeasureTheory.IntegrableAtFilter f Filter.atBot μ ∧ MeasureTheory.IntegrableAtFilter f (𝓝[<] a) μ ∧ MeasureTheory.LocallyIntegrableOn f (Set.Iio a) μ
<VAR>X : Type u_1<VAR>E : Type u_3<VAR>MeasurableSpace X<VAR>TopologicalSpace X<VAR>NormedAddCommGroup E<VAR>f : X → E<VAR>μ : MeasureTheory.Measure X<VAR>a : X<VAR>LinearOrder X<VAR>CompactIccSpace X<VAR>NoMaxOrder X<VAR>OrderTopology X<GOAL>MeasureTheory.IntegrableOn f (Set.Ioi a) μ ↔ MeasureTheory.IntegrableAtFilter f Filter.atTop μ ∧ MeasureTheory.IntegrableAtFilter f (𝓝[>] a) μ ∧ MeasureTheory.LocallyIntegrableOn f (Set.Ioi a) μ
<VAR>X : Type u_1<VAR>E : Type u_3<VAR>MeasurableSpace X<VAR>TopologicalSpace X<VAR>NormedAddCommGroup E<VAR>f : X → E<VAR>μ : MeasureTheory.Measure X<VAR>OpensMeasurableSpace X<VAR>MeasureTheory.IsLocallyFiniteMeasure μ<VAR>SecondCountableTopologyEither X E<VAR>hf : Continuous f<GOAL>MeasureTheory.LocallyIntegrable f μ
<VAR>X : Type u_1<VAR>E : Type u_3<VAR>MeasurableSpace X<VAR>TopologicalSpace X<VAR>NormedAddCommGroup E<VAR>f : X → E<VAR>μ : MeasureTheory.Measure X<VAR>OpensMeasurableSpace X<VAR>K : Set X<VAR>MeasureTheory.IsLocallyFiniteMeasure μ<VAR>SecondCountableTopologyEither X E<VAR>hf : ContinuousOn f K<VAR>hK : MeasurableSet K<GOAL>MeasureTheory.LocallyIntegrableOn f K μ
<VAR>X : Type u_1<VAR>E : Type u_3<VAR>MeasurableSpace X<VAR>TopologicalSpace X<VAR>NormedAddCommGroup E<VAR>f : X → E<VAR>μ : MeasureTheory.Measure X<VAR>OpensMeasurableSpace X<VAR>K : Set X<VAR>MeasureTheory.IsFiniteMeasureOnCompacts μ<VAR>hK : IsCompact K<VAR>h'K : MeasurableSet K<VAR>hf : ContinuousOn f K<GOAL>MeasureTheory.IntegrableOn f K μ
<VAR>X : Type u_1<VAR>E : Type u_3<VAR>MeasurableSpace X<VAR>TopologicalSpace X<VAR>NormedAddCommGroup E<VAR>f : X → E<VAR>μ : MeasureTheory.Measure X<VAR>OpensMeasurableSpace X<VAR>K : Set X<VAR>MeasureTheory.IsFiniteMeasureOnCompacts μ<VAR>T2Space X<VAR>hK : IsCompact K<VAR>hf : ContinuousOn f K<GOAL>MeasureTheory.IntegrableOn f K μ
<VAR>X : Type u_1<VAR>E : Type u_3<VAR>MeasurableSpace X<VAR>TopologicalSpace X<VAR>NormedAddCommGroup E<VAR>f : X → E<VAR>μ : MeasureTheory.Measure X<VAR>OpensMeasurableSpace X<VAR>a b : X<VAR>MeasureTheory.IsFiniteMeasureOnCompacts μ<VAR>Preorder X<VAR>CompactIccSpace X<VAR>T2Space X<VAR>hf : ContinuousOn f (Set.Icc a b)<GOAL>MeasureTheory.IntegrableOn f (Set.Icc a b) μ
<VAR>X : Type u_1<VAR>E : Type u_3<VAR>MeasurableSpace X<VAR>TopologicalSpace X<VAR>NormedAddCommGroup E<VAR>f : X → E<VAR>μ : MeasureTheory.Measure X<VAR>OpensMeasurableSpace X<VAR>a b : X<VAR>MeasureTheory.IsFiniteMeasureOnCompacts μ<VAR>Preorder X<VAR>CompactIccSpace X<VAR>T2Space X<VAR>hf : Continuous f<GOAL>MeasureTheory.IntegrableOn f (Set.Icc a b) μ
<VAR>X : Type u_1<VAR>E : Type u_3<VAR>MeasurableSpace X<VAR>TopologicalSpace X<VAR>NormedAddCommGroup E<VAR>f : X → E<VAR>μ : MeasureTheory.Measure X<VAR>OpensMeasurableSpace X<VAR>a b : X<VAR>MeasureTheory.IsFiniteMeasureOnCompacts μ<VAR>Preorder X<VAR>CompactIccSpace X<VAR>T2Space X<VAR>hf : Continuous f<GOAL>MeasureTheory.IntegrableOn f (Set.Ioc a b) μ
<VAR>X : Type u_1<VAR>E : Type u_3<VAR>MeasurableSpace X<VAR>TopologicalSpace X<VAR>NormedAddCommGroup E<VAR>f : X → E<VAR>μ : MeasureTheory.Measure X<VAR>OpensMeasurableSpace X<VAR>a b : X<VAR>MeasureTheory.IsFiniteMeasureOnCompacts μ<VAR>LinearOrder X<VAR>CompactIccSpace X<VAR>T2Space X<VAR>hf : ContinuousOn f [[a, b]]<GOAL>MeasureTheory.IntegrableOn f [[a, b]] μ
<VAR>X : Type u_1<VAR>E : Type u_3<VAR>MeasurableSpace X<VAR>TopologicalSpace X<VAR>NormedAddCommGroup E<VAR>f : X → E<VAR>μ : MeasureTheory.Measure X<VAR>OpensMeasurableSpace X<VAR>a b : X<VAR>MeasureTheory.IsFiniteMeasureOnCompacts μ<VAR>LinearOrder X<VAR>CompactIccSpace X<VAR>T2Space X<VAR>hf : Continuous f<GOAL>MeasureTheory.IntegrableOn f [[a, b]] μ
<VAR>X : Type u_1<VAR>E : Type u_3<VAR>MeasurableSpace X<VAR>TopologicalSpace X<VAR>NormedAddCommGroup E<VAR>f : X → E<VAR>μ : MeasureTheory.Measure X<VAR>OpensMeasurableSpace X<VAR>a b : X<VAR>MeasureTheory.IsFiniteMeasureOnCompacts μ<VAR>LinearOrder X<VAR>CompactIccSpace X<VAR>T2Space X<VAR>hf : Continuous f<GOAL>MeasureTheory.IntegrableOn f (Ι a b) μ
<VAR>X : Type u_1<VAR>E : Type u_3<VAR>MeasurableSpace X<VAR>TopologicalSpace X<VAR>NormedAddCommGroup E<VAR>f : X → E<VAR>μ : MeasureTheory.Measure X<VAR>OpensMeasurableSpace X<VAR>MeasureTheory.IsFiniteMeasureOnCompacts μ<VAR>hf : Continuous f<VAR>hcf : HasCompactSupport f<GOAL>MeasureTheory.Integrable f μ
<VAR>X : Type u_1<VAR>E : Type u_3<VAR>MeasurableSpace X<VAR>TopologicalSpace X<VAR>NormedAddCommGroup E<VAR>f : X → E<VAR>μ : MeasureTheory.Measure X<VAR>s : Set X<VAR>BorelSpace X<VAR>ConditionallyCompleteLinearOrder X<VAR>ConditionallyCompleteLinearOrder E<VAR>OrderTopology X<VAR>OrderTopology E<VAR>SecondCountableTopology E<VAR>hmono : MonotoneOn f s<VAR>a b : X<VAR>ha : IsLeast s a<VAR>hb : IsGreatest s b<VAR>hs : μ s ≠ ⊤<VAR>h's : MeasurableSet s<GOAL>MeasureTheory.IntegrableOn f s μ
<VAR>X : Type u_1<VAR>E : Type u_3<VAR>MeasurableSpace X<VAR>TopologicalSpace X<VAR>NormedAddCommGroup E<VAR>f : X → E<VAR>μ : MeasureTheory.Measure X<VAR>s : Set X<VAR>BorelSpace X<VAR>ConditionallyCompleteLinearOrder X<VAR>ConditionallyCompleteLinearOrder E<VAR>OrderTopology X<VAR>OrderTopology E<VAR>SecondCountableTopology E<VAR>MeasureTheory.IsFiniteMeasureOnCompacts μ<VAR>hs : IsCompact s<VAR>hmono : MonotoneOn f s<GOAL>MeasureTheory.IntegrableOn f s μ
<VAR>X : Type u_1<VAR>E : Type u_3<VAR>MeasurableSpace X<VAR>TopologicalSpace X<VAR>NormedAddCommGroup E<VAR>f : X → E<VAR>μ : MeasureTheory.Measure X<VAR>s : Set X<VAR>BorelSpace X<VAR>ConditionallyCompleteLinearOrder X<VAR>ConditionallyCompleteLinearOrder E<VAR>OrderTopology X<VAR>OrderTopology E<VAR>SecondCountableTopology E<VAR>hanti : AntitoneOn f s<VAR>a b : X<VAR>ha : IsLeast s a<VAR>hb : IsGreatest s b<VAR>hs : μ s ≠ ⊤<VAR>h's : MeasurableSet s<GOAL>MeasureTheory.IntegrableOn f s μ
<VAR>X : Type u_1<VAR>E : Type u_3<VAR>MeasurableSpace X<VAR>TopologicalSpace X<VAR>NormedAddCommGroup E<VAR>f : X → E<VAR>μ : MeasureTheory.Measure X<VAR>s : Set X<VAR>BorelSpace X<VAR>ConditionallyCompleteLinearOrder X<VAR>ConditionallyCompleteLinearOrder E<VAR>OrderTopology X<VAR>OrderTopology E<VAR>SecondCountableTopology E<VAR>MeasureTheory.IsFiniteMeasureOnCompacts μ<VAR>hs : IsCompact s<VAR>hanti : AntitoneOn f s<GOAL>MeasureTheory.IntegrableOn f s μ
<VAR>X : Type u_1<VAR>E : Type u_3<VAR>MeasurableSpace X<VAR>TopologicalSpace X<VAR>NormedAddCommGroup E<VAR>f : X → E<VAR>μ : MeasureTheory.Measure X<VAR>BorelSpace X<VAR>ConditionallyCompleteLinearOrder X<VAR>ConditionallyCompleteLinearOrder E<VAR>OrderTopology X<VAR>OrderTopology E<VAR>SecondCountableTopology E<VAR>MeasureTheory.IsLocallyFiniteMeasure μ<VAR>hmono : Monotone f<GOAL>MeasureTheory.LocallyIntegrable f μ
<VAR>X : Type u_1<VAR>E : Type u_3<VAR>MeasurableSpace X<VAR>TopologicalSpace X<VAR>NormedAddCommGroup E<VAR>f : X → E<VAR>μ : MeasureTheory.Measure X<VAR>BorelSpace X<VAR>ConditionallyCompleteLinearOrder X<VAR>ConditionallyCompleteLinearOrder E<VAR>OrderTopology X<VAR>OrderTopology E<VAR>SecondCountableTopology E<VAR>MeasureTheory.IsLocallyFiniteMeasure μ<VAR>hanti : Antitone f<GOAL>MeasureTheory.LocallyIntegrable f μ
<VAR>X : Type u_1<VAR>R : Type u_5<VAR>MeasurableSpace X<VAR>TopologicalSpace X<VAR>μ : MeasureTheory.Measure X<VAR>OpensMeasurableSpace X<VAR>A K : Set X<VAR>NormedRing R<VAR>SecondCountableTopologyEither X R<VAR>g g' : X → R<VAR>hg : MeasureTheory.IntegrableOn g A μ<VAR>hg' : ContinuousOn g' K<VAR>hA : MeasurableSet A<VAR>hK : IsCompact K<VAR>hAK : A ⊆ K<GOAL>MeasureTheory.IntegrableOn (fun x => g x * g' x) A μ
<VAR>X : Type u_1<VAR>R : Type u_5<VAR>MeasurableSpace X<VAR>TopologicalSpace X<VAR>μ : MeasureTheory.Measure X<VAR>OpensMeasurableSpace X<VAR>K : Set X<VAR>NormedRing R<VAR>SecondCountableTopologyEither X R<VAR>g g' : X → R<VAR>T2Space X<VAR>hg : MeasureTheory.IntegrableOn g K μ<VAR>hg' : ContinuousOn g' K<VAR>hK : IsCompact K<GOAL>MeasureTheory.IntegrableOn (fun x => g x * g' x) K μ
<VAR>X : Type u_1<VAR>R : Type u_5<VAR>MeasurableSpace X<VAR>TopologicalSpace X<VAR>μ : MeasureTheory.Measure X<VAR>OpensMeasurableSpace X<VAR>A K : Set X<VAR>NormedRing R<VAR>SecondCountableTopologyEither X R<VAR>g g' : X → R<VAR>hg : ContinuousOn g K<VAR>hg' : MeasureTheory.IntegrableOn g' A μ<VAR>hK : IsCompact K<VAR>hA : MeasurableSet A<VAR>hAK : A ⊆ K<GOAL>MeasureTheory.IntegrableOn (fun x => g x * g' x) A μ
<VAR>X : Type u_1<VAR>R : Type u_5<VAR>MeasurableSpace X<VAR>TopologicalSpace X<VAR>μ : MeasureTheory.Measure X<VAR>OpensMeasurableSpace X<VAR>K : Set X<VAR>NormedRing R<VAR>SecondCountableTopologyEither X R<VAR>g g' : X → R<VAR>T2Space X<VAR>hg : ContinuousOn g K<VAR>hg' : MeasureTheory.IntegrableOn g' K μ<VAR>hK : IsCompact K<GOAL>MeasureTheory.IntegrableOn (fun x => g x * g' x) K μ
<VAR>X : Type u_1<VAR>E : Type u_3<VAR>MeasurableSpace X<VAR>TopologicalSpace X<VAR>NormedAddCommGroup E<VAR>μ : MeasureTheory.Measure X<VAR>OpensMeasurableSpace X<VAR>K : Set X<VAR>𝕜 : Type u_6<VAR>NormedField 𝕜<VAR>NormedSpace 𝕜 E<VAR>T2Space X<VAR>SecondCountableTopologyEither X 𝕜<VAR>g : X → E<VAR>hg : MeasureTheory.IntegrableOn g K μ<VAR>f : X → 𝕜<VAR>hf : ContinuousOn f K<VAR>hK : IsCompact K<GOAL>MeasureTheory.IntegrableOn (fun x => f x • g x) K μ
<VAR>X : Type u_1<VAR>E : Type u_3<VAR>MeasurableSpace X<VAR>TopologicalSpace X<VAR>NormedAddCommGroup E<VAR>μ : MeasureTheory.Measure X<VAR>OpensMeasurableSpace X<VAR>K : Set X<VAR>𝕜 : Type u_6<VAR>NormedField 𝕜<VAR>NormedSpace 𝕜 E<VAR>T2Space X<VAR>SecondCountableTopologyEither X E<VAR>f : X → 𝕜<VAR>hf : MeasureTheory.IntegrableOn f K μ<VAR>g : X → E<VAR>hg : ContinuousOn g K<VAR>hK : IsCompact K<GOAL>MeasureTheory.IntegrableOn (fun x => f x • g x) K μ
<VAR>X : Type u_1<VAR>R : Type u_5<VAR>MeasurableSpace X<VAR>TopologicalSpace X<VAR>μ : MeasureTheory.Measure X<VAR>OpensMeasurableSpace X<VAR>LocallyCompactSpace X<VAR>T2Space X<VAR>NormedRing R<VAR>SecondCountableTopologyEither X R<VAR>f g : X → R<VAR>s : Set X<VAR>hf : MeasureTheory.LocallyIntegrableOn f s μ<VAR>hg : ContinuousOn g s<VAR>hs : IsOpen s<GOAL>MeasureTheory.LocallyIntegrableOn (fun x => g x * f x) s μ
<VAR>X : Type u_1<VAR>R : Type u_5<VAR>MeasurableSpace X<VAR>TopologicalSpace X<VAR>μ : MeasureTheory.Measure X<VAR>OpensMeasurableSpace X<VAR>LocallyCompactSpace X<VAR>T2Space X<VAR>NormedRing R<VAR>SecondCountableTopologyEither X R<VAR>f g : X → R<VAR>s : Set X<VAR>hf : MeasureTheory.LocallyIntegrableOn f s μ<VAR>hg : ContinuousOn g s<VAR>hs : IsOpen s<GOAL>MeasureTheory.LocallyIntegrableOn (fun x => f x * g x) s μ
<VAR>X : Type u_1<VAR>E : Type u_3<VAR>MeasurableSpace X<VAR>TopologicalSpace X<VAR>NormedAddCommGroup E<VAR>μ : MeasureTheory.Measure X<VAR>OpensMeasurableSpace X<VAR>LocallyCompactSpace X<VAR>T2Space X<VAR>𝕜 : Type u_6<VAR>NormedField 𝕜<VAR>SecondCountableTopologyEither X 𝕜<VAR>NormedSpace 𝕜 E<VAR>f : X → E<VAR>g : X → 𝕜<VAR>s : Set X<VAR>hs : IsOpen s<VAR>hf : MeasureTheory.LocallyIntegrableOn f s μ<VAR>hg : ContinuousOn g s<GOAL>MeasureTheory.LocallyIntegrableOn (fun x => g x • f x) s μ
<VAR>X : Type u_1<VAR>E : Type u_3<VAR>MeasurableSpace X<VAR>TopologicalSpace X<VAR>NormedAddCommGroup E<VAR>μ : MeasureTheory.Measure X<VAR>OpensMeasurableSpace X<VAR>LocallyCompactSpace X<VAR>T2Space X<VAR>𝕜 : Type u_6<VAR>NormedField 𝕜<VAR>SecondCountableTopologyEither X E<VAR>NormedSpace 𝕜 E<VAR>f : X → 𝕜<VAR>g : X → E<VAR>s : Set X<VAR>hs : IsOpen s<VAR>hf : MeasureTheory.LocallyIntegrableOn f s μ<VAR>hg : ContinuousOn g s<GOAL>MeasureTheory.LocallyIntegrableOn (fun x => f x • g x) s μ
<VAR>α : Type u_2<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>r : ℝ≥0∞<VAR>s : ℕ → Set α<VAR>hs : ∀ (n : ℕ), MeasurableSet (s n)<VAR>hr₀ : r ≠ 0<VAR>hr : ∀ (n : ℕ), r ≤ μ (s n)<GOAL>∃ t, t.Infinite ∧ ∀ ⦃u : Set ℕ⦄, u ⊆ t → u.Finite → 0 < μ (⋂ n ∈ u, s n)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>r : ℝ≥0∞<VAR>Infinite ι<VAR>s : ι → Set α<VAR>hs : ∀ (i : ι), MeasurableSet (s i)<VAR>hr₀ : r ≠ 0<VAR>hr : ∀ (i : ι), r ≤ μ (s i)<GOAL>∃ t, t.Infinite ∧ ∀ ⦃u : Set ι⦄, u ⊆ t → u.Finite → 0 < μ (⋂ i ∈ u, s i)
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>NormalSpace α<VAR>MeasurableSpace α<VAR>BorelSpace α<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>μ : MeasureTheory.Measure α<VAR>p : ℝ≥0∞<VAR>NormedSpace ℝ E<VAR>μ.OuterRegular<VAR>hp : p ≠ ⊤<VAR>s u : Set α<VAR>s_closed : IsClosed s<VAR>u_open : IsOpen u<VAR>hsu : s ⊆ u<VAR>hs : μ s ≠ ⊤<VAR>c : E<VAR>ε : ℝ≥0∞<VAR>hε : ε ≠ 0<GOAL>∃ f, Continuous f ∧ MeasureTheory.eLpNorm (fun x => f x - s.indicator (fun _y => c) x) p μ ≤ ε ∧ (∀ (x : α), ‖f x‖ ≤ ‖c‖) ∧ Function.support f ⊆ u ∧ MeasureTheory.Memℒp f p μ
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>NormalSpace α<VAR>R1Space α<VAR>MeasurableSpace α<VAR>BorelSpace α<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>μ : MeasureTheory.Measure α<VAR>p : ℝ≥0∞<VAR>NormedSpace ℝ E<VAR>WeaklyLocallyCompactSpace α<VAR>μ.Regular<VAR>hp : p ≠ ⊤<VAR>f : α → E<VAR>hf : MeasureTheory.Memℒp f p μ<VAR>ε : ℝ≥0∞<VAR>hε : ε ≠ 0<GOAL>∃ g, HasCompactSupport g ∧ MeasureTheory.eLpNorm (f - g) p μ ≤ ε ∧ Continuous g ∧ MeasureTheory.Memℒp g p μ
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>NormalSpace α<VAR>R1Space α<VAR>MeasurableSpace α<VAR>BorelSpace α<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>μ : MeasureTheory.Measure α<VAR>NormedSpace ℝ E<VAR>WeaklyLocallyCompactSpace α<VAR>μ.Regular<VAR>p : ℝ<VAR>hp : 0 < p<VAR>f : α → E<VAR>hf : MeasureTheory.Memℒp f (ENNReal.ofReal p) μ<VAR>ε : ℝ<VAR>hε : 0 < ε<GOAL>∃ g, HasCompactSupport g ∧ ∫ (x : α), ‖f x - g x‖ ^ p ∂μ ≤ ε ∧ Continuous g ∧ MeasureTheory.Memℒp g (ENNReal.ofReal p) μ
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>NormalSpace α<VAR>R1Space α<VAR>MeasurableSpace α<VAR>BorelSpace α<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>μ : MeasureTheory.Measure α<VAR>NormedSpace ℝ E<VAR>WeaklyLocallyCompactSpace α<VAR>μ.Regular<VAR>f : α → E<VAR>hf : MeasureTheory.Integrable f μ<VAR>ε : ℝ≥0∞<VAR>hε : ε ≠ 0<GOAL>∃ g, HasCompactSupport g ∧ ∫⁻ (x : α), ↑‖f x - g x‖₊ ∂μ ≤ ε ∧ Continuous g ∧ MeasureTheory.Integrable g μ
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>NormalSpace α<VAR>R1Space α<VAR>MeasurableSpace α<VAR>BorelSpace α<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>μ : MeasureTheory.Measure α<VAR>NormedSpace ℝ E<VAR>WeaklyLocallyCompactSpace α<VAR>μ.Regular<VAR>f : α → E<VAR>hf : MeasureTheory.Integrable f μ<VAR>ε : ℝ<VAR>hε : 0 < ε<GOAL>∃ g, HasCompactSupport g ∧ ∫ (x : α), ‖f x - g x‖ ∂μ ≤ ε ∧ Continuous g ∧ MeasureTheory.Integrable g μ
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>NormalSpace α<VAR>MeasurableSpace α<VAR>BorelSpace α<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>μ : MeasureTheory.Measure α<VAR>p : ℝ≥0∞<VAR>NormedSpace ℝ E<VAR>μ.WeaklyRegular<VAR>hp : p ≠ ⊤<VAR>f : α → E<VAR>hf : MeasureTheory.Memℒp f p μ<VAR>ε : ℝ≥0∞<VAR>hε : ε ≠ 0<GOAL>∃ g, MeasureTheory.eLpNorm (f - ⇑g) p μ ≤ ε ∧ MeasureTheory.Memℒp (⇑g) p μ