ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>X : Type u_1<VAR>E : Type u_3<VAR>MeasurableSpace X<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>μ : MeasureTheory.Measure X<VAR>Y : Type u_5<GOAL>∀ {x : MeasurableSpace Y} {f : X → Y} {ν : MeasureTheory.Measure Y}, MeasureTheory.MeasurePreserving f μ ν → MeasurableEmbedding f → ∀ (g : Y → E) (s : Set X), ∫ (y : Y) in f '' s, g y ∂ν = ∫ (x : X) in s, g (f x) ∂μ
<VAR>X : Type u_1<VAR>E : Type u_3<VAR>MeasurableSpace X<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>μ : MeasureTheory.Measure X<VAR>Y : Type u_5<VAR>MeasurableSpace Y<VAR>e : X ≃ᵐ Y<VAR>f : Y → E<VAR>s : Set Y<GOAL>∫ (y : Y) in s, f y ∂MeasureTheory.Measure.map (⇑e) μ = ∫ (x : X) in ⇑e ⁻¹' s, f (e x) ∂μ
<VAR>X : Type u_1<VAR>E : Type u_3<VAR>MeasurableSpace X<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>f : X → E<VAR>s : Set X<VAR>μ : MeasureTheory.Measure X<VAR>C : ℝ<VAR>hs : μ s < ⊤<VAR>hC : ∀ᵐ (x : X) ∂μ.restrict s, ‖f x‖ ≤ C<GOAL>‖∫ (x : X) in s, f x ∂μ‖ ≤ C * (μ s).toReal
<VAR>X : Type u_1<VAR>E : Type u_3<VAR>MeasurableSpace X<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>f : X → E<VAR>s : Set X<VAR>μ : MeasureTheory.Measure X<VAR>C : ℝ<VAR>hs : μ s < ⊤<VAR>hC : ∀ᵐ (x : X) ∂μ, x ∈ s → ‖f x‖ ≤ C<VAR>hfm : MeasureTheory.AEStronglyMeasurable f (μ.restrict s)<GOAL>‖∫ (x : X) in s, f x ∂μ‖ ≤ C * (μ s).toReal
<VAR>X : Type u_1<VAR>E : Type u_3<VAR>MeasurableSpace X<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>f : X → E<VAR>s : Set X<VAR>μ : MeasureTheory.Measure X<VAR>C : ℝ<VAR>hs : μ s < ⊤<VAR>hsm : MeasurableSet s<VAR>hC : ∀ᵐ (x : X) ∂μ, x ∈ s → ‖f x‖ ≤ C<GOAL>‖∫ (x : X) in s, f x ∂μ‖ ≤ C * (μ s).toReal
<VAR>X : Type u_1<VAR>E : Type u_3<VAR>MeasurableSpace X<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>f : X → E<VAR>s : Set X<VAR>μ : MeasureTheory.Measure X<VAR>C : ℝ<VAR>hs : μ s < ⊤<VAR>hC : ∀ x ∈ s, ‖f x‖ ≤ C<VAR>hfm : MeasureTheory.AEStronglyMeasurable f (μ.restrict s)<GOAL>‖∫ (x : X) in s, f x ∂μ‖ ≤ C * (μ s).toReal
<VAR>X : Type u_1<VAR>E : Type u_3<VAR>MeasurableSpace X<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>f : X → E<VAR>s : Set X<VAR>μ : MeasureTheory.Measure X<VAR>C : ℝ<VAR>hs : μ s < ⊤<VAR>hsm : MeasurableSet s<VAR>hC : ∀ x ∈ s, ‖f x‖ ≤ C<GOAL>‖∫ (x : X) in s, f x ∂μ‖ ≤ C * (μ s).toReal
<VAR>X : Type u_1<VAR>MeasurableSpace X<VAR>s : Set X<VAR>μ : MeasureTheory.Measure X<VAR>f : X → ℝ<VAR>hf : 0 ≤ᵐ[μ.restrict s] f<VAR>hfi : MeasureTheory.IntegrableOn f s μ<GOAL>∫ (x : X) in s, f x ∂μ = 0 ↔ f =ᵐ[μ.restrict s] 0
<VAR>X : Type u_1<VAR>MeasurableSpace X<VAR>s : Set X<VAR>μ : MeasureTheory.Measure X<VAR>f : X → ℝ<VAR>hf : 0 ≤ᵐ[μ.restrict s] f<VAR>hfi : MeasureTheory.IntegrableOn f s μ<GOAL>0 < ∫ (x : X) in s, f x ∂μ ↔ 0 < μ (Function.support f ∩ s)
<VAR>X : Type u_1<VAR>MeasurableSpace X<VAR>μ : MeasureTheory.Measure X<VAR>R : ℝ<VAR>f : X → ℝ<VAR>hR : 0 ≤ R<VAR>hfint : MeasureTheory.IntegrableOn f {x | R < f x} μ<VAR>hμ : μ {x | R < f x} ≠ 0<GOAL>(μ {x | R < f x}).toReal * R < ∫ (x : X) in {x | R < f x}, f x ∂μ
<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>X : Type u_5<VAR>m m0 : MeasurableSpace X<VAR>μ : MeasureTheory.Measure X<VAR>hm : m ≤ m0<VAR>f : X → E<VAR>hf_meas : MeasureTheory.StronglyMeasurable f<VAR>s : Set X<VAR>hs : MeasurableSet s<GOAL>∫ (x : X) in s, f x ∂μ = ∫ (x : X) in s, f x ∂μ.trim hm
<VAR>X : Type u_1<VAR>E : Type u_3<VAR>MeasurableSpace X<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>f : X → E<VAR>μ : MeasureTheory.Measure X<VAR>PartialOrder X<VAR>x y : X<VAR>hx : μ {x} = 0<GOAL>∫ (t : X) in Set.Icc x y, f t ∂μ = ∫ (t : X) in Set.Ioc x y, f t ∂μ
<VAR>X : Type u_1<VAR>E : Type u_3<VAR>MeasurableSpace X<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>f : X → E<VAR>μ : MeasureTheory.Measure X<VAR>PartialOrder X<VAR>x y : X<VAR>hy : μ {y} = 0<GOAL>∫ (t : X) in Set.Icc x y, f t ∂μ = ∫ (t : X) in Set.Ico x y, f t ∂μ
<VAR>X : Type u_1<VAR>E : Type u_3<VAR>MeasurableSpace X<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>f : X → E<VAR>μ : MeasureTheory.Measure X<VAR>PartialOrder X<VAR>x y : X<VAR>hy : μ {y} = 0<GOAL>∫ (t : X) in Set.Ioc x y, f t ∂μ = ∫ (t : X) in Set.Ioo x y, f t ∂μ
<VAR>X : Type u_1<VAR>E : Type u_3<VAR>MeasurableSpace X<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>f : X → E<VAR>μ : MeasureTheory.Measure X<VAR>PartialOrder X<VAR>x y : X<VAR>hx : μ {x} = 0<GOAL>∫ (t : X) in Set.Ico x y, f t ∂μ = ∫ (t : X) in Set.Ioo x y, f t ∂μ
<VAR>X : Type u_1<VAR>E : Type u_3<VAR>MeasurableSpace X<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>f : X → E<VAR>μ : MeasureTheory.Measure X<VAR>PartialOrder X<VAR>x y : X<VAR>hx : μ {x} = 0<VAR>hy : μ {y} = 0<GOAL>∫ (t : X) in Set.Icc x y, f t ∂μ = ∫ (t : X) in Set.Ioo x y, f t ∂μ
<VAR>X : Type u_1<VAR>E : Type u_3<VAR>MeasurableSpace X<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>f : X → E<VAR>μ : MeasureTheory.Measure X<VAR>PartialOrder X<VAR>x : X<VAR>hx : μ {x} = 0<GOAL>∫ (t : X) in Set.Iic x, f t ∂μ = ∫ (t : X) in Set.Iio x, f t ∂μ
<VAR>X : Type u_1<VAR>E : Type u_3<VAR>MeasurableSpace X<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>f : X → E<VAR>μ : MeasureTheory.Measure X<VAR>PartialOrder X<VAR>x : X<VAR>hx : μ {x} = 0<GOAL>∫ (t : X) in Set.Ici x, f t ∂μ = ∫ (t : X) in Set.Ioi x, f t ∂μ
<VAR>X : Type u_1<VAR>E : Type u_3<VAR>MeasurableSpace X<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>f : X → E<VAR>μ : MeasureTheory.Measure X<VAR>PartialOrder X<VAR>x y : X<VAR>MeasureTheory.NoAtoms μ<GOAL>∫ (t : X) in Set.Icc x y, f t ∂μ = ∫ (t : X) in Set.Ioc x y, f t ∂μ
<VAR>X : Type u_1<VAR>E : Type u_3<VAR>MeasurableSpace X<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>f : X → E<VAR>μ : MeasureTheory.Measure X<VAR>PartialOrder X<VAR>x y : X<VAR>MeasureTheory.NoAtoms μ<GOAL>∫ (t : X) in Set.Icc x y, f t ∂μ = ∫ (t : X) in Set.Ico x y, f t ∂μ
<VAR>X : Type u_1<VAR>E : Type u_3<VAR>MeasurableSpace X<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>f : X → E<VAR>μ : MeasureTheory.Measure X<VAR>PartialOrder X<VAR>x y : X<VAR>MeasureTheory.NoAtoms μ<GOAL>∫ (t : X) in Set.Ioc x y, f t ∂μ = ∫ (t : X) in Set.Ioo x y, f t ∂μ
<VAR>X : Type u_1<VAR>E : Type u_3<VAR>MeasurableSpace X<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>f : X → E<VAR>μ : MeasureTheory.Measure X<VAR>PartialOrder X<VAR>x y : X<VAR>MeasureTheory.NoAtoms μ<GOAL>∫ (t : X) in Set.Ico x y, f t ∂μ = ∫ (t : X) in Set.Ioo x y, f t ∂μ
<VAR>X : Type u_1<VAR>E : Type u_3<VAR>MeasurableSpace X<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>f : X → E<VAR>μ : MeasureTheory.Measure X<VAR>PartialOrder X<VAR>x y : X<VAR>MeasureTheory.NoAtoms μ<GOAL>∫ (t : X) in Set.Icc x y, f t ∂μ = ∫ (t : X) in Set.Ioo x y, f t ∂μ
<VAR>X : Type u_1<VAR>E : Type u_3<VAR>MeasurableSpace X<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>f : X → E<VAR>μ : MeasureTheory.Measure X<VAR>PartialOrder X<VAR>x : X<VAR>MeasureTheory.NoAtoms μ<GOAL>∫ (t : X) in Set.Iic x, f t ∂μ = ∫ (t : X) in Set.Iio x, f t ∂μ
<VAR>X : Type u_1<VAR>E : Type u_3<VAR>MeasurableSpace X<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>f : X → E<VAR>μ : MeasureTheory.Measure X<VAR>PartialOrder X<VAR>x : X<VAR>MeasureTheory.NoAtoms μ<GOAL>∫ (t : X) in Set.Ici x, f t ∂μ = ∫ (t : X) in Set.Ioi x, f t ∂μ
<VAR>X : Type u_1<VAR>MeasurableSpace X<VAR>μ : MeasureTheory.Measure X<VAR>f g : X → ℝ<VAR>s : Set X<VAR>hf : MeasureTheory.IntegrableOn f s μ<VAR>hg : MeasureTheory.IntegrableOn g s μ<VAR>h : f ≤ᵐ[μ.restrict s] g<GOAL>∫ (x : X) in s, f x ∂μ ≤ ∫ (x : X) in s, g x ∂μ
<VAR>X : Type u_1<VAR>MeasurableSpace X<VAR>μ : MeasureTheory.Measure X<VAR>f g : X → ℝ<VAR>s : Set X<VAR>hf : MeasureTheory.IntegrableOn f s μ<VAR>hg : MeasureTheory.IntegrableOn g s μ<VAR>h : f ≤ᵐ[μ] g<GOAL>∫ (x : X) in s, f x ∂μ ≤ ∫ (x : X) in s, g x ∂μ
<VAR>X : Type u_1<VAR>MeasurableSpace X<VAR>μ : MeasureTheory.Measure X<VAR>f g : X → ℝ<VAR>s : Set X<VAR>hf : MeasureTheory.IntegrableOn f s μ<VAR>hg : MeasureTheory.IntegrableOn g s μ<VAR>hs : MeasurableSet s<VAR>h : ∀ x ∈ s, f x ≤ g x<GOAL>∫ (x : X) in s, f x ∂μ ≤ ∫ (x : X) in s, g x ∂μ
<VAR>X : Type u_1<VAR>MeasurableSpace X<VAR>μ : MeasureTheory.Measure X<VAR>f g : X → ℝ<VAR>s : Set X<VAR>hf : MeasureTheory.IntegrableOn f s μ<VAR>hg : MeasureTheory.IntegrableOn g s μ<VAR>hs : MeasurableSet s<VAR>h : ∀ᵐ (x : X) ∂μ, x ∈ s → f x ≤ g x<GOAL>∫ (x : X) in s, f x ∂μ ≤ ∫ (x : X) in s, g x ∂μ
<VAR>X : Type u_1<VAR>MeasurableSpace X<VAR>μ : MeasureTheory.Measure X<VAR>f g : X → ℝ<VAR>s : Set X<VAR>hf : MeasureTheory.IntegrableOn f s μ<VAR>hg : MeasureTheory.IntegrableOn g s μ<VAR>h : f ≤ g<GOAL>∫ (x : X) in s, f x ∂μ ≤ ∫ (x : X) in s, g x ∂μ
<VAR>X : Type u_1<VAR>MeasurableSpace X<VAR>μ : MeasureTheory.Measure X<VAR>f : X → ℝ<VAR>s t : Set X<VAR>hfi : MeasureTheory.IntegrableOn f t μ<VAR>hf : 0 ≤ᵐ[μ.restrict t] f<VAR>hst : s ≤ᵐ[μ] t<GOAL>∫ (x : X) in s, f x ∂μ ≤ ∫ (x : X) in t, f x ∂μ
<VAR>X : Type u_1<VAR>MeasurableSpace X<VAR>μ : MeasureTheory.Measure X<VAR>f : X → ℝ<VAR>s : Set X<VAR>hfi : MeasureTheory.Integrable f μ<VAR>hf : 0 ≤ᵐ[μ] f<GOAL>∫ (x : X) in s, f x ∂μ ≤ ∫ (x : X), f x ∂μ
<VAR>X : Type u_1<VAR>MeasurableSpace X<VAR>μ : MeasureTheory.Measure X<VAR>f : X → ℝ<VAR>s : Set X<VAR>c : ℝ<VAR>hs : MeasurableSet s<VAR>hμs : μ s ≠ ⊤<VAR>hf : ∀ x ∈ s, c ≤ f x<VAR>hfint : MeasureTheory.IntegrableOn (fun x => f x) s μ<GOAL>c * (μ s).toReal ≤ ∫ (x : X) in s, f x ∂μ
<VAR>X : Type u_1<VAR>MeasurableSpace X<VAR>μ : MeasureTheory.Measure X<VAR>f : X → ℝ<VAR>s : Set X<VAR>hf : 0 ≤ᵐ[μ.restrict s] f<GOAL>0 ≤ ∫ (x : X) in s, f x ∂μ
<VAR>X : Type u_1<VAR>MeasurableSpace X<VAR>μ : MeasureTheory.Measure X<VAR>f : X → ℝ<VAR>s : Set X<VAR>hf : 0 ≤ᵐ[μ] f<GOAL>0 ≤ ∫ (x : X) in s, f x ∂μ
<VAR>X : Type u_1<VAR>MeasurableSpace X<VAR>μ : MeasureTheory.Measure X<VAR>f : X → ℝ<VAR>s : Set X<VAR>hs : MeasurableSet s<VAR>hf : ∀ x ∈ s, 0 ≤ f x<GOAL>0 ≤ ∫ (x : X) in s, f x ∂μ
<VAR>X : Type u_1<VAR>MeasurableSpace X<VAR>μ : MeasureTheory.Measure X<VAR>f : X → ℝ<VAR>s : Set X<VAR>hs : MeasurableSet s<VAR>hf : ∀ᵐ (x : X) ∂μ, x ∈ s → 0 ≤ f x<GOAL>0 ≤ ∫ (x : X) in s, f x ∂μ
<VAR>X : Type u_1<VAR>MeasurableSpace X<VAR>μ : MeasureTheory.Measure X<VAR>f : X → ℝ<VAR>s : Set X<VAR>hs : MeasurableSet s<VAR>hf : MeasureTheory.StronglyMeasurable f<VAR>hfi : MeasureTheory.Integrable f μ<GOAL>∫ (x : X) in s, f x ∂μ ≤ ∫ (x : X) in {y | 0 ≤ f y}, f x ∂μ
<VAR>X : Type u_1<VAR>MeasurableSpace X<VAR>μ : MeasureTheory.Measure X<VAR>f : X → ℝ<VAR>s : Set X<VAR>hf : f ≤ᵐ[μ.restrict s] 0<GOAL>∫ (x : X) in s, f x ∂μ ≤ 0
<VAR>X : Type u_1<VAR>MeasurableSpace X<VAR>μ : MeasureTheory.Measure X<VAR>f : X → ℝ<VAR>s : Set X<VAR>hf : f ≤ᵐ[μ] 0<GOAL>∫ (x : X) in s, f x ∂μ ≤ 0
<VAR>X : Type u_1<VAR>MeasurableSpace X<VAR>μ : MeasureTheory.Measure X<VAR>f : X → ℝ<VAR>s : Set X<VAR>hs : MeasurableSet s<VAR>hf : ∀ᵐ (x : X) ∂μ, x ∈ s → f x ≤ 0<GOAL>∫ (x : X) in s, f x ∂μ ≤ 0
<VAR>X : Type u_1<VAR>MeasurableSpace X<VAR>μ : MeasureTheory.Measure X<VAR>f : X → ℝ<VAR>s : Set X<VAR>hs : MeasurableSet s<VAR>hf : ∀ x ∈ s, f x ≤ 0<GOAL>∫ (x : X) in s, f x ∂μ ≤ 0
<VAR>X : Type u_1<VAR>MeasurableSpace X<VAR>μ : MeasureTheory.Measure X<VAR>f : X → ℝ<VAR>s : Set X<VAR>hs : MeasurableSet s<VAR>hf : MeasureTheory.StronglyMeasurable f<VAR>hfi : MeasureTheory.Integrable f μ<GOAL>∫ (x : X) in {y | f y ≤ 0}, f x ∂μ ≤ ∫ (x : X) in s, f x ∂μ
<VAR>X : Type u_1<VAR>MeasurableSpace X<VAR>μ : MeasureTheory.Measure X<VAR>f : X → ℝ<VAR>f_int : MeasureTheory.Integrable f μ<VAR>f_nonneg : 0 ≤ᵐ[μ] f<VAR>s : Set X<VAR>hs : ∀ x ∈ s, 1 ≤ f x<GOAL>μ s ≤ ENNReal.ofReal (∫ (x : X), f x ∂μ)
<VAR>X : Type u_1<VAR>MeasurableSpace X<VAR>μ : MeasureTheory.Measure X<VAR>f : X → ℝ<VAR>s : Set X<VAR>hs : ∀ x ∈ s, f x ≤ 1<VAR>h's : ∀ x ∈ sᶜ, f x ≤ 0<GOAL>ENNReal.ofReal (∫ (x : X), f x ∂μ) ≤ μ s
<VAR>X : Type u_1<VAR>E : Type u_3<VAR>MeasurableSpace X<VAR>ι : Type u_5<VAR>Countable ι<VAR>μ : MeasureTheory.Measure X<VAR>NormedAddCommGroup E<VAR>f : X → E<VAR>s : ι → Set X<VAR>hs : ∀ (i : ι), MeasurableSet (s i)<VAR>hi : ∀ (i : ι), MeasureTheory.IntegrableOn f (s i) μ<VAR>h : Summable fun i => ∫ (x : X) in s i, ‖f x‖ ∂μ<GOAL>MeasureTheory.IntegrableOn f (Set.iUnion s) μ
<VAR>X : Type u_1<VAR>E : Type u_3<VAR>MeasurableSpace X<VAR>ι : Type u_5<VAR>Countable ι<VAR>μ : MeasureTheory.Measure X<VAR>NormedAddCommGroup E<VAR>TopologicalSpace X<VAR>BorelSpace X<VAR>TopologicalSpace.MetrizableSpace X<VAR>MeasureTheory.IsLocallyFiniteMeasure μ<VAR>f : C(X, E)<VAR>s : ι → TopologicalSpace.Compacts X<VAR>hf : Summable fun i => ‖ContinuousMap.restrict (↑(s i)) f‖ * (μ ↑(s i)).toReal<GOAL>MeasureTheory.IntegrableOn (⇑f) (⋃ i, ↑(s i)) μ
<VAR>X : Type u_1<VAR>E : Type u_3<VAR>MeasurableSpace X<VAR>ι : Type u_5<VAR>Countable ι<VAR>μ : MeasureTheory.Measure X<VAR>NormedAddCommGroup E<VAR>TopologicalSpace X<VAR>BorelSpace X<VAR>TopologicalSpace.MetrizableSpace X<VAR>MeasureTheory.IsLocallyFiniteMeasure μ<VAR>f : C(X, E)<VAR>s : ι → TopologicalSpace.Compacts X<VAR>hf : Summable fun i => ‖ContinuousMap.restrict (↑(s i)) f‖ * (μ ↑(s i)).toReal<VAR>hs : ⋃ i, ↑(s i) = Set.univ<GOAL>MeasureTheory.Integrable (⇑f) μ
<VAR>X : Type u_1<VAR>E : Type u_3<VAR>MeasurableSpace X<VAR>NormedAddCommGroup E<VAR>p : ℝ≥0∞<VAR>μ : MeasureTheory.Measure X<VAR>f g : ↥(MeasureTheory.Lp E p μ)<VAR>s : Set X<GOAL>MeasureTheory.Memℒp.toLp ↑↑(f + g) ⋯ = MeasureTheory.Memℒp.toLp ↑↑f ⋯ + MeasureTheory.Memℒp.toLp ↑↑g ⋯
<VAR>X : Type u_1<VAR>F : Type u_4<VAR>MeasurableSpace X<VAR>𝕜 : Type u_5<VAR>NormedField 𝕜<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>p : ℝ≥0∞<VAR>μ : MeasureTheory.Measure X<VAR>c : 𝕜<VAR>f : ↥(MeasureTheory.Lp F p μ)<VAR>s : Set X<GOAL>MeasureTheory.Memℒp.toLp ↑↑(c • f) ⋯ = c • MeasureTheory.Memℒp.toLp ↑↑f ⋯
<VAR>X : Type u_1<VAR>E : Type u_3<VAR>MeasurableSpace X<VAR>NormedAddCommGroup E<VAR>p : ℝ≥0∞<VAR>μ : MeasureTheory.Measure X<VAR>s : Set X<VAR>f : ↥(MeasureTheory.Lp E p μ)<GOAL>‖MeasureTheory.Memℒp.toLp ↑↑f ⋯‖ ≤ ‖f‖
<VAR>X : Type u_1<VAR>F : Type u_4<VAR>MeasurableSpace X<VAR>𝕜 : Type u_5<VAR>NormedField 𝕜<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>p : ℝ≥0∞<VAR>μ : MeasureTheory.Measure X<VAR>Fact (1 ≤ p)<VAR>s : Set X<VAR>f : ↥(MeasureTheory.Lp F p μ)<GOAL>↑↑((MeasureTheory.LpToLpRestrictCLM X F 𝕜 μ p s) f) =ᵐ[μ.restrict s] ↑↑f
<VAR>X : Type u_1<VAR>E : Type u_3<VAR>MeasurableSpace X<VAR>NormedAddCommGroup E<VAR>μ : MeasureTheory.Measure X<VAR>NormedSpace ℝ E<VAR>s : Set X<GOAL>Continuous fun f => ∫ (x : X) in s, ↑↑f x ∂μ
<VAR>X : Type u_1<VAR>MeasurableSpace X<VAR>TopologicalSpace X<VAR>OpensMeasurableSpace X<VAR>μ : MeasureTheory.Measure X<VAR>μ.IsOpenPosMeasure<VAR>MeasureTheory.IsFiniteMeasureOnCompacts μ<VAR>f : X → ℝ<VAR>x : X<VAR>f_cont : Continuous f<VAR>f_comp : HasCompactSupport f<VAR>f_nonneg : 0 ≤ f<VAR>f_x : f x ≠ 0<GOAL>0 < ∫ (x : X), f x ∂μ
<VAR>X : Type u_1<VAR>E : Type u_3<VAR>MeasurableSpace X<VAR>ι : Type u_5<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>CompleteSpace E<VAR>μ : MeasureTheory.Measure X<VAR>l : Filter X<VAR>l.IsMeasurablyGenerated<VAR>f : X → E<VAR>b : E<VAR>h : Filter.Tendsto f (l ⊓ MeasureTheory.ae μ) (𝓝 b)<VAR>hfm : StronglyMeasurableAtFilter f l μ<VAR>hμ : μ.FiniteAtFilter l<VAR>s : ι → Set X<VAR>li : Filter ι<VAR>hs : Filter.Tendsto s li l.smallSets<VAR>m : ι → ℝ := fun i => (μ (s i)).toReal<VAR>hsμ : (fun i => (μ (s i)).toReal) =ᶠ[li] m := by rfl<GOAL>(fun i => ∫ (x : X) in s i, f x ∂μ - m i • b) =o[li] m
<VAR>X : Type u_1<VAR>E : Type u_3<VAR>MeasurableSpace X<VAR>ι : Type u_5<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>CompleteSpace E<VAR>TopologicalSpace X<VAR>OpensMeasurableSpace X<VAR>μ : MeasureTheory.Measure X<VAR>MeasureTheory.IsLocallyFiniteMeasure μ<VAR>x : X<VAR>t : Set X<VAR>f : X → E<VAR>hx : ContinuousWithinAt f t x<VAR>ht : MeasurableSet t<VAR>hfm : StronglyMeasurableAtFilter f (𝓝[t] x) μ<VAR>s : ι → Set X<VAR>li : Filter ι<VAR>hs : Filter.Tendsto s li (𝓝[t] x).smallSets<VAR>m : ι → ℝ := fun i => (μ (s i)).toReal<VAR>hsμ : (fun i => (μ (s i)).toReal) =ᶠ[li] m := by rfl<GOAL>(fun i => ∫ (x : X) in s i, f x ∂μ - m i • f x) =o[li] m
<VAR>X : Type u_1<VAR>E : Type u_3<VAR>MeasurableSpace X<VAR>ι : Type u_5<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>CompleteSpace E<VAR>TopologicalSpace X<VAR>OpensMeasurableSpace X<VAR>μ : MeasureTheory.Measure X<VAR>MeasureTheory.IsLocallyFiniteMeasure μ<VAR>x : X<VAR>f : X → E<VAR>hx : ContinuousAt f x<VAR>hfm : StronglyMeasurableAtFilter f (𝓝 x) μ<VAR>s : ι → Set X<VAR>li : Filter ι<VAR>hs : Filter.Tendsto s li (𝓝 x).smallSets<VAR>m : ι → ℝ := fun i => (μ (s i)).toReal<VAR>hsμ : (fun i => (μ (s i)).toReal) =ᶠ[li] m := by rfl<GOAL>(fun i => ∫ (x : X) in s i, f x ∂μ - m i • f x) =o[li] m
<VAR>X : Type u_1<VAR>E : Type u_3<VAR>MeasurableSpace X<VAR>ι : Type u_5<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>CompleteSpace E<VAR>TopologicalSpace X<VAR>OpensMeasurableSpace X<VAR>SecondCountableTopologyEither X E<VAR>μ : MeasureTheory.Measure X<VAR>MeasureTheory.IsLocallyFiniteMeasure μ<VAR>x : X<VAR>t : Set X<VAR>f : X → E<VAR>hft : ContinuousOn f t<VAR>hx : x ∈ t<VAR>ht : MeasurableSet t<VAR>s : ι → Set X<VAR>li : Filter ι<VAR>hs : Filter.Tendsto s li (𝓝[t] x).smallSets<VAR>m : ι → ℝ := fun i => (μ (s i)).toReal<VAR>hsμ : (fun i => (μ (s i)).toReal) =ᶠ[li] m := by rfl<GOAL>(fun i => ∫ (x : X) in s i, f x ∂μ - m i • f x) =o[li] m
<VAR>X : Type u_1<VAR>E : Type u_3<VAR>F : Type u_4<VAR>MeasurableSpace X<VAR>μ : MeasureTheory.Measure X<VAR>𝕜 : Type u_5<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>p : ℝ≥0∞<VAR>NormedSpace ℝ F<VAR>L : E →L[𝕜] F<VAR>φ : ↥(MeasureTheory.Lp E p μ)<GOAL>∫ (x : X), ↑↑(L.compLp φ) x ∂μ = ∫ (x : X), L (↑↑φ x) ∂μ
<VAR>X : Type u_1<VAR>E : Type u_3<VAR>F : Type u_4<VAR>MeasurableSpace X<VAR>μ : MeasureTheory.Measure X<VAR>𝕜 : Type u_5<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>p : ℝ≥0∞<VAR>NormedSpace ℝ F<VAR>L : E →L[𝕜] F<VAR>φ : ↥(MeasureTheory.Lp E p μ)<VAR>s : Set X<VAR>hs : MeasurableSet s<GOAL>∫ (x : X) in s, ↑↑(L.compLp φ) x ∂μ = ∫ (x : X) in s, L (↑↑φ x) ∂μ
<VAR>X : Type u_1<VAR>E : Type u_3<VAR>F : Type u_4<VAR>MeasurableSpace X<VAR>μ : MeasureTheory.Measure X<VAR>𝕜 : Type u_5<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>NormedSpace ℝ F<VAR>L : E →L[𝕜] F<GOAL>Continuous fun φ => ∫ (x : X), L (↑↑φ x) ∂μ
<VAR>X : Type u_1<VAR>E : Type u_3<VAR>F : Type u_4<VAR>MeasurableSpace X<VAR>μ : MeasureTheory.Measure X<VAR>𝕜 : Type u_5<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>NormedSpace ℝ F<VAR>CompleteSpace F<VAR>NormedSpace ℝ E<VAR>CompleteSpace E<VAR>L : E →L[𝕜] F<VAR>φ : X → E<VAR>φ_int : MeasureTheory.Integrable φ μ<GOAL>∫ (x : X), L (φ x) ∂μ = L (∫ (x : X), φ x ∂μ)
<VAR>X : Type u_1<VAR>E : Type u_3<VAR>MeasurableSpace X<VAR>μ : MeasureTheory.Measure X<VAR>𝕜 : Type u_5<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>NormedSpace ℝ E<VAR>H : Type u_6<VAR>NormedAddCommGroup H<VAR>NormedSpace 𝕜 H<VAR>φ : X → H →L[𝕜] E<VAR>φ_int : MeasureTheory.Integrable φ μ<VAR>v : H<GOAL>(∫ (x : X), φ x ∂μ) v = ∫ (x : X), (φ x) v ∂μ
<VAR>X : Type u_1<VAR>E : Type u_3<VAR>MeasurableSpace X<VAR>μ : MeasureTheory.Measure X<VAR>𝕜 : Type u_5<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>NormedSpace ℝ E<VAR>ι : Type u_6<VAR>Fintype ι<VAR>M : ι → Type u_7<VAR>(i : ι) → NormedAddCommGroup (M i)<VAR>(i : ι) → NormedSpace 𝕜 (M i)<VAR>φ : X → ContinuousMultilinearMap 𝕜 M E<VAR>φ_int : MeasureTheory.Integrable φ μ<VAR>m : (i : ι) → M i<GOAL>(∫ (x : X), φ x ∂μ) m = ∫ (x : X), (φ x) m ∂μ
<VAR>X : Type u_1<VAR>E : Type u_3<VAR>F : Type u_4<VAR>MeasurableSpace X<VAR>μ : MeasureTheory.Measure X<VAR>𝕜 : Type u_5<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>NormedSpace ℝ F<VAR>CompleteSpace F<VAR>NormedSpace ℝ E<VAR>CompleteSpace E<VAR>L : E →L[𝕜] F<VAR>K : ℝ≥0<VAR>hL : AntilipschitzWith K ⇑L<VAR>φ : X → E<GOAL>∫ (x : X), L (φ x) ∂μ = L (∫ (x : X), φ x ∂μ)
<VAR>X : Type u_1<VAR>E : Type u_3<VAR>F : Type u_4<VAR>MeasurableSpace X<VAR>μ : MeasureTheory.Measure X<VAR>𝕜 : Type u_5<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>NormedSpace ℝ F<VAR>CompleteSpace F<VAR>NormedSpace ℝ E<VAR>CompleteSpace E<VAR>L : E →L[𝕜] F<VAR>φ : ↥(MeasureTheory.Lp E 1 μ)<GOAL>∫ (x : X), L (↑↑φ x) ∂μ = L (∫ (x : X), ↑↑φ x ∂μ)
<VAR>X : Type u_1<VAR>E : Type u_3<VAR>F : Type u_4<VAR>MeasurableSpace X<VAR>μ : MeasureTheory.Measure X<VAR>𝕜 : Type u_5<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>CompleteSpace F<VAR>NormedSpace ℝ F<VAR>CompleteSpace E<VAR>NormedSpace ℝ E<VAR>L : E →ₗᵢ[𝕜] F<VAR>φ : X → E<GOAL>∫ (x : X), L (φ x) ∂μ = L (∫ (x : X), φ x ∂μ)
<VAR>X : Type u_1<VAR>E : Type u_3<VAR>F : Type u_4<VAR>MeasurableSpace X<VAR>μ : MeasureTheory.Measure X<VAR>𝕜 : Type u_5<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>NormedSpace ℝ F<VAR>NormedSpace ℝ E<VAR>L : E ≃L[𝕜] F<VAR>φ : X → E<GOAL>∫ (x : X), L (φ x) ∂μ = L (∫ (x : X), φ x ∂μ)
<VAR>X : Type u_1<VAR>MeasurableSpace X<VAR>μ : MeasureTheory.Measure X<VAR>𝕜 : Type u_5<VAR>RCLike 𝕜<VAR>f : X → ℝ<GOAL>∫ (x : X), ↑(f x) ∂μ = ↑(∫ (x : X), f x ∂μ)
<VAR>X : Type u_1<VAR>MeasurableSpace X<VAR>μ : MeasureTheory.Measure X<VAR>𝕜 : Type u_5<VAR>RCLike 𝕜<VAR>f : X → 𝕜<VAR>hf : MeasureTheory.Integrable f μ<GOAL>∫ (x : X), RCLike.re (f x) ∂μ = RCLike.re (∫ (x : X), f x ∂μ)
<VAR>X : Type u_1<VAR>MeasurableSpace X<VAR>μ : MeasureTheory.Measure X<VAR>𝕜 : Type u_5<VAR>RCLike 𝕜<VAR>f : X → 𝕜<VAR>hf : MeasureTheory.Integrable f μ<GOAL>∫ (x : X), RCLike.im (f x) ∂μ = RCLike.im (∫ (x : X), f x ∂μ)
<VAR>X : Type u_1<VAR>MeasurableSpace X<VAR>μ : MeasureTheory.Measure X<VAR>𝕜 : Type u_5<VAR>RCLike 𝕜<VAR>f : X → 𝕜<GOAL>∫ (x : X), (starRingEnd 𝕜) (f x) ∂μ = (starRingEnd 𝕜) (∫ (x : X), f x ∂μ)
<VAR>X : Type u_1<VAR>MeasurableSpace X<VAR>μ : MeasureTheory.Measure X<VAR>𝕜 : Type u_5<VAR>RCLike 𝕜<VAR>f : X → 𝕜<VAR>hf : MeasureTheory.Integrable f μ<GOAL>∫ (x : X), ↑(RCLike.re (f x)) ∂μ + (∫ (x : X), ↑(RCLike.im (f x)) ∂μ) * RCLike.I = ∫ (x : X), f x ∂μ
<VAR>X : Type u_1<VAR>MeasurableSpace X<VAR>μ : MeasureTheory.Measure X<VAR>𝕜 : Type u_5<VAR>RCLike 𝕜<VAR>f : X → 𝕜<VAR>hf : MeasureTheory.Integrable f μ<GOAL>↑(∫ (x : X), RCLike.re (f x) ∂μ) + ↑(∫ (x : X), RCLike.im (f x) ∂μ) * RCLike.I = ∫ (x : X), f x ∂μ
<VAR>X : Type u_1<VAR>MeasurableSpace X<VAR>μ : MeasureTheory.Measure X<VAR>𝕜 : Type u_5<VAR>RCLike 𝕜<VAR>f : X → 𝕜<VAR>i : Set X<VAR>hf : MeasureTheory.IntegrableOn f i μ<GOAL>↑(∫ (x : X) in i, RCLike.re (f x) ∂μ) + ↑(∫ (x : X) in i, RCLike.im (f x) ∂μ) * RCLike.I = ∫ (x : X) in i, f x ∂μ
<VAR>X : Type u_1<VAR>E : Type u_3<VAR>F : Type u_4<VAR>MeasurableSpace X<VAR>μ : MeasureTheory.Measure X<VAR>NormedAddCommGroup E<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ E<VAR>NormedSpace ℝ F<VAR>f : X → E × F<GOAL>(∫ (x : X), f x ∂μ).swap = ∫ (x : X), (f x).swap ∂μ
<VAR>X : Type u_1<VAR>E : Type u_3<VAR>F : Type u_4<VAR>MeasurableSpace X<VAR>μ : MeasureTheory.Measure X<VAR>NormedAddCommGroup E<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ E<VAR>NormedSpace ℝ F<VAR>CompleteSpace F<VAR>f : X → E × F<VAR>hf : MeasureTheory.Integrable f μ<GOAL>(∫ (x : X), f x ∂μ).1 = ∫ (x : X), (f x).1 ∂μ
<VAR>X : Type u_1<VAR>E : Type u_3<VAR>F : Type u_4<VAR>MeasurableSpace X<VAR>μ : MeasureTheory.Measure X<VAR>NormedAddCommGroup E<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ E<VAR>NormedSpace ℝ F<VAR>CompleteSpace E<VAR>f : X → E × F<VAR>hf : MeasureTheory.Integrable f μ<GOAL>(∫ (x : X), f x ∂μ).2 = ∫ (x : X), (f x).2 ∂μ
<VAR>X : Type u_1<VAR>E : Type u_3<VAR>F : Type u_4<VAR>MeasurableSpace X<VAR>μ : MeasureTheory.Measure X<VAR>NormedAddCommGroup E<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ E<VAR>NormedSpace ℝ F<VAR>CompleteSpace E<VAR>CompleteSpace F<VAR>f : X → E<VAR>g : X → F<VAR>hf : MeasureTheory.Integrable f μ<VAR>hg : MeasureTheory.Integrable g μ<GOAL>∫ (x : X), (f x, g x) ∂μ = (∫ (x : X), f x ∂μ, ∫ (x : X), g x ∂μ)
<VAR>X : Type u_1<VAR>E : Type u_3<VAR>MeasurableSpace X<VAR>μ : MeasureTheory.Measure X<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>𝕜 : Type u_6<VAR>RCLike 𝕜<VAR>NormedSpace 𝕜 E<VAR>CompleteSpace E<VAR>f : X → 𝕜<VAR>c : E<GOAL>∫ (x : X), f x • c ∂μ = (∫ (x : X), f x ∂μ) • c