ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>NormedSpace ℝ E<GOAL>‖MeasureTheory.L1.SimpleFunc.integralCLM α E μ‖ ≤ 1
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f : ↥(MeasureTheory.Lp.simpleFunc ℝ 1 μ)<GOAL>↑(MeasureTheory.Lp.simpleFunc.toSimpleFunc (MeasureTheory.L1.SimpleFunc.posPart f)) =ᵐ[μ] ↑(MeasureTheory.Lp.simpleFunc.toSimpleFunc f).posPart
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f : ↥(MeasureTheory.Lp.simpleFunc ℝ 1 μ)<GOAL>↑(MeasureTheory.Lp.simpleFunc.toSimpleFunc (MeasureTheory.L1.SimpleFunc.negPart f)) =ᵐ[μ] ↑(MeasureTheory.Lp.simpleFunc.toSimpleFunc f).negPart
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f : ↥(MeasureTheory.Lp.simpleFunc ℝ 1 μ)<GOAL>MeasureTheory.L1.SimpleFunc.integral f = ‖MeasureTheory.L1.SimpleFunc.posPart f‖ - ‖MeasureTheory.L1.SimpleFunc.negPart f‖
<VAR>α : Type u_5<VAR>E : Type u_6<VAR>NormedAddCommGroup E<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>NormedSpace ℝ E<VAR>CompleteSpace E<GOAL>MeasureTheory.L1.integral = ⇑MeasureTheory.L1.integralCLM
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>NormedSpace ℝ E<VAR>CompleteSpace E<VAR>f : ↥(MeasureTheory.Lp E 1 μ)<GOAL>MeasureTheory.L1.integral f = MeasureTheory.L1.integralCLM f
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>NormedSpace ℝ E<VAR>CompleteSpace E<VAR>f : ↥(MeasureTheory.Lp E 1 μ)<GOAL>MeasureTheory.L1.integral f = (MeasureTheory.L1.setToL1 ⋯) f
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>NormedSpace ℝ E<VAR>CompleteSpace E<VAR>f : ↥(MeasureTheory.Lp.simpleFunc E 1 μ)<GOAL>MeasureTheory.L1.integral ↑f = MeasureTheory.L1.SimpleFunc.integral f
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>NormedSpace ℝ E<VAR>CompleteSpace E<GOAL>MeasureTheory.L1.integral 0 = 0
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>NormedSpace ℝ E<VAR>CompleteSpace E<VAR>f g : ↥(MeasureTheory.Lp E 1 μ)<GOAL>MeasureTheory.L1.integral (f + g) = MeasureTheory.L1.integral f + MeasureTheory.L1.integral g
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>NormedSpace ℝ E<VAR>CompleteSpace E<VAR>f : ↥(MeasureTheory.Lp E 1 μ)<GOAL>MeasureTheory.L1.integral (-f) = -MeasureTheory.L1.integral f
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>NormedSpace ℝ E<VAR>CompleteSpace E<VAR>f g : ↥(MeasureTheory.Lp E 1 μ)<GOAL>MeasureTheory.L1.integral (f - g) = MeasureTheory.L1.integral f - MeasureTheory.L1.integral g
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>𝕜 : Type u_4<VAR>NormedAddCommGroup E<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>NormedSpace ℝ E<VAR>NontriviallyNormedField 𝕜<VAR>NormedSpace 𝕜 E<VAR>SMulCommClass ℝ 𝕜 E<VAR>CompleteSpace E<VAR>c : 𝕜<VAR>f : ↥(MeasureTheory.Lp E 1 μ)<GOAL>MeasureTheory.L1.integral (c • f) = c • MeasureTheory.L1.integral f
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>NormedSpace ℝ E<VAR>CompleteSpace E<GOAL>‖MeasureTheory.L1.integralCLM‖ ≤ 1
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>NormedSpace ℝ E<VAR>CompleteSpace E<GOAL>‖MeasureTheory.L1.integralCLM‖₊ ≤ 1
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>NormedSpace ℝ E<VAR>CompleteSpace E<VAR>f : ↥(MeasureTheory.Lp E 1 μ)<GOAL>‖MeasureTheory.L1.integral f‖ ≤ ‖f‖
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>NormedSpace ℝ E<VAR>CompleteSpace E<VAR>f : ↥(MeasureTheory.Lp E 1 μ)<GOAL>‖MeasureTheory.L1.integral f‖₊ ≤ ‖f‖₊
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>NormedSpace ℝ E<VAR>CompleteSpace E<GOAL>Continuous fun f => MeasureTheory.L1.integral f
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f : ↥(MeasureTheory.Lp ℝ 1 μ)<GOAL>MeasureTheory.L1.integral f = ‖MeasureTheory.Lp.posPart f‖ - ‖MeasureTheory.Lp.negPart f‖
<VAR>α : Type u_6<VAR>G : Type u_7<VAR>NormedAddCommGroup G<VAR>NormedSpace ℝ G<GOAL>∀ {x : MeasurableSpace α} (μ : MeasureTheory.Measure α) (f : α → G), MeasureTheory.integral μ f = if x_1 : CompleteSpace G then if hf : MeasureTheory.Integrable f μ then MeasureTheory.L1.integral (MeasureTheory.Integrable.toL1 f hf) else 0 else 0
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>hE : CompleteSpace E<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f : α → E<VAR>hf : MeasureTheory.Integrable f μ<GOAL>∫ (a : α), f a ∂μ = MeasureTheory.L1.integral (MeasureTheory.Integrable.toL1 f hf)
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>hE : CompleteSpace E<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f : α → E<GOAL>∫ (a : α), f a ∂μ = MeasureTheory.setToFun μ (MeasureTheory.weightedSMul μ) ⋯ f
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>hE : CompleteSpace E<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f : ↥(MeasureTheory.Lp E 1 μ)<GOAL>MeasureTheory.L1.integral f = ∫ (a : α), ↑↑f a ∂μ
<VAR>α : Type u_1<VAR>G : Type u_5<VAR>NormedAddCommGroup G<VAR>NormedSpace ℝ G<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f : α → G<VAR>h : ¬MeasureTheory.Integrable f μ<GOAL>∫ (a : α), f a ∂μ = 0
<VAR>α : Type u_1<VAR>G : Type u_5<VAR>NormedAddCommGroup G<VAR>NormedSpace ℝ G<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f : α → G<VAR>h : ∫ (a : α), f a ∂μ ≠ 0<GOAL>MeasureTheory.Integrable f μ
<VAR>α : Type u_1<VAR>G : Type u_5<VAR>NormedAddCommGroup G<VAR>NormedSpace ℝ G<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f : α → G<VAR>h : ¬MeasureTheory.AEStronglyMeasurable f μ<GOAL>∫ (a : α), f a ∂μ = 0
<VAR>α : Type u_1<VAR>G : Type u_5<VAR>NormedAddCommGroup G<VAR>NormedSpace ℝ G<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<GOAL>∫ (x : α), 0 ∂μ = 0
<VAR>α : Type u_1<VAR>G : Type u_5<VAR>NormedAddCommGroup G<VAR>NormedSpace ℝ G<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<GOAL>MeasureTheory.integral μ 0 = 0
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f : α → ℝ<VAR>h : ∫ (x : α), f x ∂μ = 1<GOAL>MeasureTheory.Integrable f μ
<VAR>α : Type u_1<VAR>G : Type u_5<VAR>NormedAddCommGroup G<VAR>NormedSpace ℝ G<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f g : α → G<VAR>hf : MeasureTheory.Integrable f μ<VAR>hg : MeasureTheory.Integrable g μ<GOAL>∫ (a : α), f a + g a ∂μ = ∫ (a : α), f a ∂μ + ∫ (a : α), g a ∂μ
<VAR>α : Type u_1<VAR>G : Type u_5<VAR>NormedAddCommGroup G<VAR>NormedSpace ℝ G<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f g : α → G<VAR>hf : MeasureTheory.Integrable f μ<VAR>hg : MeasureTheory.Integrable g μ<GOAL>∫ (a : α), (f + g) a ∂μ = ∫ (a : α), f a ∂μ + ∫ (a : α), g a ∂μ
<VAR>α : Type u_1<VAR>G : Type u_5<VAR>NormedAddCommGroup G<VAR>NormedSpace ℝ G<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>ι : Type u_6<VAR>s : Finset ι<VAR>f : ι → α → G<VAR>hf : ∀ i ∈ s, MeasureTheory.Integrable (f i) μ<GOAL>∫ (a : α), ∑ i ∈ s, f i a ∂μ = ∑ i ∈ s, ∫ (a : α), f i a ∂μ
<VAR>α : Type u_1<VAR>G : Type u_5<VAR>NormedAddCommGroup G<VAR>NormedSpace ℝ G<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f : α → G<GOAL>∫ (a : α), -f a ∂μ = -∫ (a : α), f a ∂μ
<VAR>α : Type u_1<VAR>G : Type u_5<VAR>NormedAddCommGroup G<VAR>NormedSpace ℝ G<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f : α → G<GOAL>∫ (a : α), (-f) a ∂μ = -∫ (a : α), f a ∂μ
<VAR>α : Type u_1<VAR>G : Type u_5<VAR>NormedAddCommGroup G<VAR>NormedSpace ℝ G<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f g : α → G<VAR>hf : MeasureTheory.Integrable f μ<VAR>hg : MeasureTheory.Integrable g μ<GOAL>∫ (a : α), f a - g a ∂μ = ∫ (a : α), f a ∂μ - ∫ (a : α), g a ∂μ
<VAR>α : Type u_1<VAR>G : Type u_5<VAR>NormedAddCommGroup G<VAR>NormedSpace ℝ G<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f g : α → G<VAR>hf : MeasureTheory.Integrable f μ<VAR>hg : MeasureTheory.Integrable g μ<GOAL>∫ (a : α), (f - g) a ∂μ = ∫ (a : α), f a ∂μ - ∫ (a : α), g a ∂μ
<VAR>α : Type u_1<VAR>𝕜 : Type u_4<VAR>NontriviallyNormedField 𝕜<VAR>G : Type u_5<VAR>NormedAddCommGroup G<VAR>NormedSpace ℝ G<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>NormedSpace 𝕜 G<VAR>SMulCommClass ℝ 𝕜 G<VAR>c : 𝕜<VAR>f : α → G<GOAL>∫ (a : α), c • f a ∂μ = c • ∫ (a : α), f a ∂μ
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>L : Type u_6<VAR>RCLike L<VAR>r : L<VAR>f : α → L<GOAL>∫ (a : α), r * f a ∂μ = r * ∫ (a : α), f a ∂μ
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>L : Type u_6<VAR>RCLike L<VAR>r : L<VAR>f : α → L<GOAL>∫ (a : α), f a * r ∂μ = (∫ (a : α), f a ∂μ) * r
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>L : Type u_6<VAR>RCLike L<VAR>r : L<VAR>f : α → L<GOAL>∫ (a : α), f a / r ∂μ = (∫ (a : α), f a ∂μ) / r
<VAR>α : Type u_1<VAR>G : Type u_5<VAR>NormedAddCommGroup G<VAR>NormedSpace ℝ G<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f g : α → G<VAR>h : f =ᵐ[μ] g<GOAL>∫ (a : α), f a ∂μ = ∫ (a : α), g a ∂μ
<VAR>α : Type u_1<VAR>G : Type u_5<VAR>NormedAddCommGroup G<VAR>NormedSpace ℝ G<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f : α → G<VAR>hf : MeasureTheory.Integrable f μ<GOAL>∫ (a : α), ↑↑(MeasureTheory.Integrable.toL1 f hf) a ∂μ = ∫ (a : α), f a ∂μ
<VAR>α : Type u_1<VAR>G : Type u_5<VAR>NormedAddCommGroup G<VAR>NormedSpace ℝ G<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<GOAL>Continuous fun f => ∫ (a : α), ↑↑f a ∂μ
<VAR>α : Type u_1<VAR>G : Type u_5<VAR>NormedAddCommGroup G<VAR>NormedSpace ℝ G<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f : α → G<GOAL>‖∫ (a : α), f a ∂μ‖ ≤ (∫⁻ (a : α), ENNReal.ofReal ‖f a‖ ∂μ).toReal
<VAR>α : Type u_1<VAR>G : Type u_5<VAR>NormedAddCommGroup G<VAR>NormedSpace ℝ G<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f : α → G<GOAL>↑‖∫ (a : α), f a ∂μ‖₊ ≤ ∫⁻ (a : α), ↑‖f a‖₊ ∂μ
<VAR>α : Type u_1<VAR>G : Type u_5<VAR>NormedAddCommGroup G<VAR>NormedSpace ℝ G<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f : α → G<VAR>hf : f =ᵐ[μ] 0<GOAL>∫ (a : α), f a ∂μ = 0
<VAR>α : Type u_1<VAR>G : Type u_5<VAR>NormedAddCommGroup G<VAR>NormedSpace ℝ G<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>ι : Type u_6<VAR>f : α → G<VAR>hf : MeasureTheory.HasFiniteIntegral f μ<VAR>l : Filter ι<VAR>s : ι → Set α<VAR>hs : Filter.Tendsto (⇑μ ∘ s) l (𝓝 0)<GOAL>Filter.Tendsto (fun i => ∫ (x : α) in s i, f x ∂μ) l (𝓝 0)
<VAR>α : Type u_1<VAR>G : Type u_5<VAR>NormedAddCommGroup G<VAR>NormedSpace ℝ G<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>ι : Type u_6<VAR>f : α → G<VAR>hf : MeasureTheory.Integrable f μ<VAR>l : Filter ι<VAR>s : ι → Set α<VAR>hs : Filter.Tendsto (⇑μ ∘ s) l (𝓝 0)<GOAL>Filter.Tendsto (fun i => ∫ (x : α) in s i, f x ∂μ) l (𝓝 0)
<VAR>α : Type u_1<VAR>G : Type u_5<VAR>NormedAddCommGroup G<VAR>NormedSpace ℝ G<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>ι : Type u_6<VAR>f : α → G<VAR>hfi : MeasureTheory.Integrable f μ<VAR>F : ι → α → G<VAR>l : Filter ι<VAR>hFi : ∀ᶠ (i : ι) in l, MeasureTheory.Integrable (F i) μ<VAR>hF : Filter.Tendsto (fun i => ∫⁻ (x : α), ↑‖F i x - f x‖₊ ∂μ) l (𝓝 0)<GOAL>Filter.Tendsto (fun i => ∫ (x : α), F i x ∂μ) l (𝓝 (∫ (x : α), f x ∂μ))
<VAR>α : Type u_1<VAR>G : Type u_5<VAR>NormedAddCommGroup G<VAR>NormedSpace ℝ G<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>ι : Type u_6<VAR>f : α → G<VAR>hfi : MeasureTheory.Integrable f μ<VAR>F : ι → α → G<VAR>l : Filter ι<VAR>hFi : ∀ᶠ (i : ι) in l, MeasureTheory.Integrable (F i) μ<VAR>hF : Filter.Tendsto (fun i => MeasureTheory.eLpNorm (F i - f) 1 μ) l (𝓝 0)<GOAL>Filter.Tendsto (fun i => ∫ (x : α), F i x ∂μ) l (𝓝 (∫ (x : α), f x ∂μ))
<VAR>α : Type u_1<VAR>G : Type u_5<VAR>NormedAddCommGroup G<VAR>NormedSpace ℝ G<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>ι : Type u_6<VAR>f : α → G<VAR>hfi : MeasureTheory.Integrable f μ<VAR>F : ι → α → G<VAR>l : Filter ι<VAR>hFi : ∀ᶠ (i : ι) in l, MeasureTheory.Integrable (F i) μ<VAR>hF : Filter.Tendsto (fun i => ∫⁻ (x : α), ↑‖F i x - f x‖₊ ∂μ) l (𝓝 0)<VAR>s : Set α<GOAL>Filter.Tendsto (fun i => ∫ (x : α) in s, F i x ∂μ) l (𝓝 (∫ (x : α) in s, f x ∂μ))
<VAR>α : Type u_1<VAR>G : Type u_5<VAR>NormedAddCommGroup G<VAR>NormedSpace ℝ G<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>ι : Type u_6<VAR>f : α → G<VAR>hfi : MeasureTheory.Integrable f μ<VAR>F : ι → α → G<VAR>l : Filter ι<VAR>hFi : ∀ᶠ (i : ι) in l, MeasureTheory.Integrable (F i) μ<VAR>hF : Filter.Tendsto (fun i => MeasureTheory.eLpNorm (F i - f) 1 μ) l (𝓝 0)<VAR>s : Set α<GOAL>Filter.Tendsto (fun i => ∫ (x : α) in s, F i x ∂μ) l (𝓝 (∫ (x : α) in s, f x ∂μ))
<VAR>α : Type u_1<VAR>G : Type u_5<VAR>NormedAddCommGroup G<VAR>NormedSpace ℝ G<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>X : Type u_6<VAR>TopologicalSpace X<VAR>FirstCountableTopology X<VAR>F : X → α → G<VAR>x₀ : X<VAR>bound : α → ℝ<VAR>s : Set X<VAR>hF_meas : ∀ᶠ (x : X) in 𝓝[s] x₀, MeasureTheory.AEStronglyMeasurable (F x) μ<VAR>h_bound : ∀ᶠ (x : X) in 𝓝[s] x₀, ∀ᵐ (a : α) ∂μ, ‖F x a‖ ≤ bound a<VAR>bound_integrable : MeasureTheory.Integrable bound μ<VAR>h_cont : ∀ᵐ (a : α) ∂μ, ContinuousWithinAt (fun x => F x a) s x₀<GOAL>ContinuousWithinAt (fun x => ∫ (a : α), F x a ∂μ) s x₀
<VAR>α : Type u_1<VAR>G : Type u_5<VAR>NormedAddCommGroup G<VAR>NormedSpace ℝ G<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>X : Type u_6<VAR>TopologicalSpace X<VAR>FirstCountableTopology X<VAR>F : X → α → G<VAR>x₀ : X<VAR>bound : α → ℝ<VAR>hF_meas : ∀ᶠ (x : X) in 𝓝 x₀, MeasureTheory.AEStronglyMeasurable (F x) μ<VAR>h_bound : ∀ᶠ (x : X) in 𝓝 x₀, ∀ᵐ (a : α) ∂μ, ‖F x a‖ ≤ bound a<VAR>bound_integrable : MeasureTheory.Integrable bound μ<VAR>h_cont : ∀ᵐ (a : α) ∂μ, ContinuousAt (fun x => F x a) x₀<GOAL>ContinuousAt (fun x => ∫ (a : α), F x a ∂μ) x₀
<VAR>α : Type u_1<VAR>G : Type u_5<VAR>NormedAddCommGroup G<VAR>NormedSpace ℝ G<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>X : Type u_6<VAR>TopologicalSpace X<VAR>FirstCountableTopology X<VAR>F : X → α → G<VAR>bound : α → ℝ<VAR>s : Set X<VAR>hF_meas : ∀ x ∈ s, MeasureTheory.AEStronglyMeasurable (F x) μ<VAR>h_bound : ∀ x ∈ s, ∀ᵐ (a : α) ∂μ, ‖F x a‖ ≤ bound a<VAR>bound_integrable : MeasureTheory.Integrable bound μ<VAR>h_cont : ∀ᵐ (a : α) ∂μ, ContinuousOn (fun x => F x a) s<GOAL>ContinuousOn (fun x => ∫ (a : α), F x a ∂μ) s
<VAR>α : Type u_1<VAR>G : Type u_5<VAR>NormedAddCommGroup G<VAR>NormedSpace ℝ G<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>X : Type u_6<VAR>TopologicalSpace X<VAR>FirstCountableTopology X<VAR>F : X → α → G<VAR>bound : α → ℝ<VAR>hF_meas : ∀ (x : X), MeasureTheory.AEStronglyMeasurable (F x) μ<VAR>h_bound : ∀ (x : X), ∀ᵐ (a : α) ∂μ, ‖F x a‖ ≤ bound a<VAR>bound_integrable : MeasureTheory.Integrable bound μ<VAR>h_cont : ∀ᵐ (a : α) ∂μ, Continuous fun x => F x a<GOAL>Continuous fun x => ∫ (a : α), F x a ∂μ
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f : α → ℝ<VAR>hf : MeasureTheory.Integrable f μ<GOAL>∫ (a : α), f a ∂μ = (∫⁻ (a : α), ENNReal.ofReal (f a) ∂μ).toReal - (∫⁻ (a : α), ENNReal.ofReal (-f a) ∂μ).toReal
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f : α → ℝ<VAR>hf : 0 ≤ᵐ[μ] f<VAR>hfm : MeasureTheory.AEStronglyMeasurable f μ<GOAL>∫ (a : α), f a ∂μ = (∫⁻ (a : α), ENNReal.ofReal (f a) ∂μ).toReal
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>P : Type u_7<VAR>NormedAddCommGroup P<VAR>f : α → P<VAR>hf : MeasureTheory.AEStronglyMeasurable f μ<GOAL>∫ (x : α), ‖f x‖ ∂μ = (∫⁻ (x : α), ↑‖f x‖₊ ∂μ).toReal
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>P : Type u_7<VAR>NormedAddCommGroup P<VAR>f : α → P<VAR>hf : MeasureTheory.Integrable f μ<GOAL>ENNReal.ofReal (∫ (x : α), ‖f x‖ ∂μ) = ∫⁻ (x : α), ↑‖f x‖₊ ∂μ
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f : α → ℝ<VAR>hf : MeasureTheory.Integrable f μ<GOAL>∫ (a : α), f a ∂μ = ∫ (a : α), ↑(f a).toNNReal ∂μ - ∫ (a : α), ↑(-f a).toNNReal ∂μ
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f : α → ℝ<VAR>hf : 0 ≤ᵐ[μ] f<GOAL>0 ≤ ∫ (a : α), f a ∂μ
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f : α → ℝ≥0<VAR>hfi : MeasureTheory.Integrable (fun x => ↑(f x)) μ<GOAL>∫⁻ (a : α), ↑(f a) ∂μ = ENNReal.ofReal (∫ (a : α), ↑(f a) ∂μ)
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f : α → ℝ<VAR>hfi : MeasureTheory.Integrable f μ<VAR>f_nn : 0 ≤ᵐ[μ] f<GOAL>ENNReal.ofReal (∫ (x : α), f x ∂μ) = ∫⁻ (x : α), ENNReal.ofReal (f x) ∂μ
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f : α → ℝ≥0∞<VAR>hfm : AEMeasurable f μ<VAR>hf : ∀ᵐ (x : α) ∂μ, f x < ⊤<GOAL>∫ (a : α), (f a).toReal ∂μ = (∫⁻ (a : α), f a ∂μ).toReal
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f : α → ℝ≥0<VAR>hfi : MeasureTheory.Integrable (fun x => ↑(f x)) μ<VAR>b : ℝ≥0<GOAL>∫⁻ (a : α), ↑(f a) ∂μ ≤ ↑b ↔ ∫ (a : α), ↑(f a) ∂μ ≤ ↑b
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f : α → ℝ≥0<VAR>b : ℝ≥0<VAR>h : ∫⁻ (a : α), ↑(f a) ∂μ ≤ ↑b<GOAL>∫ (a : α), ↑(f a) ∂μ ≤ ↑b
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f : α → ℝ<VAR>hf : 0 ≤ f<GOAL>0 ≤ ∫ (a : α), f a ∂μ
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f : α → ℝ<VAR>hf : f ≤ᵐ[μ] 0<GOAL>∫ (a : α), f a ∂μ ≤ 0
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f : α → ℝ<VAR>hf : f ≤ 0<GOAL>∫ (a : α), f a ∂μ ≤ 0
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f : α → ℝ<VAR>hf : 0 ≤ᵐ[μ] f<VAR>hfi : MeasureTheory.Integrable f μ<GOAL>∫ (x : α), f x ∂μ = 0 ↔ f =ᵐ[μ] 0
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f : α → ℝ<VAR>hf : 0 ≤ f<VAR>hfi : MeasureTheory.Integrable f μ<GOAL>∫ (x : α), f x ∂μ = 0 ↔ f =ᵐ[μ] 0
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f g : α → ℝ<VAR>hf : MeasureTheory.Integrable f μ<VAR>hg : MeasureTheory.Integrable g μ<VAR>hfg : f ≤ᵐ[μ] g<GOAL>∫ (a : α), f a ∂μ = ∫ (a : α), g a ∂μ ↔ f =ᵐ[μ] g
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f : α → ℝ<VAR>hf : 0 ≤ᵐ[μ] f<VAR>hfi : MeasureTheory.Integrable f μ<GOAL>0 < ∫ (x : α), f x ∂μ ↔ 0 < μ (Function.support f)
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f : α → ℝ<VAR>hf : 0 ≤ f<VAR>hfi : MeasureTheory.Integrable f μ<GOAL>0 < ∫ (x : α), f x ∂μ ↔ 0 < μ (Function.support f)
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f : α → ℝ<VAR>hμ : NeZero μ<VAR>hf : MeasureTheory.Integrable (fun x => Real.exp (f x)) μ<GOAL>0 < ∫ (x : α), Real.exp (f x) ∂μ
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f : ℕ → α → ℝ<VAR>F : α → ℝ<VAR>hf : ∀ (n : ℕ), MeasureTheory.Integrable (f n) μ<VAR>hF : MeasureTheory.Integrable F μ<VAR>h_mono : ∀ᵐ (x : α) ∂μ, Monotone fun n => f n x<VAR>h_tendsto : ∀ᵐ (x : α) ∂μ, Filter.Tendsto (fun n => f n x) Filter.atTop (𝓝 (F x))<GOAL>Filter.Tendsto (fun n => ∫ (x : α), f n x ∂μ) Filter.atTop (𝓝 (∫ (x : α), F x ∂μ))
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f : ℕ → α → ℝ<VAR>F : α → ℝ<VAR>hf : ∀ (n : ℕ), MeasureTheory.Integrable (f n) μ<VAR>hF : MeasureTheory.Integrable F μ<VAR>h_mono : ∀ᵐ (x : α) ∂μ, Antitone fun n => f n x<VAR>h_tendsto : ∀ᵐ (x : α) ∂μ, Filter.Tendsto (fun n => f n x) Filter.atTop (𝓝 (F x))<GOAL>Filter.Tendsto (fun n => ∫ (x : α), f n x ∂μ) Filter.atTop (𝓝 (∫ (x : α), F x ∂μ))
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f : ℕ → α → ℝ<VAR>F : α → ℝ<VAR>hf_int : ∀ (n : ℕ), MeasureTheory.Integrable (f n) μ<VAR>hF_int : MeasureTheory.Integrable F μ<VAR>hf_tendsto : Filter.Tendsto (fun i => ∫ (a : α), f i a ∂μ) Filter.atTop (𝓝 (∫ (a : α), F a ∂μ))<VAR>hf_mono : ∀ᵐ (a : α) ∂μ, Monotone fun i => f i a<VAR>hf_bound : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), f i a ≤ F a<GOAL>∀ᵐ (a : α) ∂μ, Filter.Tendsto (fun i => f i a) Filter.atTop (𝓝 (F a))
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f : ℕ → α → ℝ<VAR>F : α → ℝ<VAR>hf_int : ∀ (n : ℕ), MeasureTheory.Integrable (f n) μ<VAR>hF_int : MeasureTheory.Integrable F μ<VAR>hf_tendsto : Filter.Tendsto (fun i => ∫ (a : α), f i a ∂μ) Filter.atTop (𝓝 (∫ (a : α), F a ∂μ))<VAR>hf_mono : ∀ᵐ (a : α) ∂μ, Antitone fun i => f i a<VAR>hf_bound : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), F a ≤ f i a<GOAL>∀ᵐ (a : α) ∂μ, Filter.Tendsto (fun i => f i a) Filter.atTop (𝓝 (F a))
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>H : Type u_7<VAR>NormedAddCommGroup H<VAR>f : ↥(MeasureTheory.Lp H 1 μ)<GOAL>‖f‖ = ∫ (a : α), ‖↑↑f a‖ ∂μ
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>H : Type u_7<VAR>NormedAddCommGroup H<VAR>f g : ↥(MeasureTheory.Lp H 1 μ)<GOAL>dist f g = ∫ (a : α), dist (↑↑f a) (↑↑g a) ∂μ
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>H : Type u_7<VAR>NormedAddCommGroup H<VAR>f : α → H<VAR>hf : MeasureTheory.Integrable f μ<GOAL>‖MeasureTheory.Integrable.toL1 f hf‖ = ∫ (a : α), ‖f a‖ ∂μ
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>H : Type u_7<VAR>NormedAddCommGroup H<VAR>f : α → H<VAR>p : ℝ≥0∞<VAR>hp1 : p ≠ 0<VAR>hp2 : p ≠ ⊤<VAR>hf : MeasureTheory.Memℒp f p μ<GOAL>MeasureTheory.eLpNorm f p μ = ENNReal.ofReal ((∫ (a : α), ‖f a‖ ^ p.toReal ∂μ) ^ p.toReal⁻¹)
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f g : α → ℝ<VAR>hf : MeasureTheory.Integrable f μ<VAR>hg : MeasureTheory.Integrable g μ<VAR>h : f ≤ᵐ[μ] g<GOAL>∫ (a : α), f a ∂μ ≤ ∫ (a : α), g a ∂μ
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f g : α → ℝ<VAR>hf : MeasureTheory.Integrable f μ<VAR>hg : MeasureTheory.Integrable g μ<VAR>h : f ≤ g<GOAL>∫ (a : α), f a ∂μ ≤ ∫ (a : α), g a ∂μ
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f g : α → ℝ<VAR>hf : 0 ≤ᵐ[μ] f<VAR>hgi : MeasureTheory.Integrable g μ<VAR>h : f ≤ᵐ[μ] g<GOAL>∫ (a : α), f a ∂μ ≤ ∫ (a : α), g a ∂μ
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f : α → ℝ<VAR>ν : MeasureTheory.Measure α<VAR>hle : μ ≤ ν<VAR>hf : 0 ≤ᵐ[ν] f<VAR>hfi : MeasureTheory.Integrable f ν<GOAL>∫ (a : α), f a ∂μ ≤ ∫ (a : α), f a ∂ν
<VAR>α : Type u_1<VAR>G : Type u_5<VAR>NormedAddCommGroup G<VAR>NormedSpace ℝ G<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f : α → G<GOAL>‖∫ (a : α), f a ∂μ‖ ≤ ∫ (a : α), ‖f a‖ ∂μ
<VAR>α : Type u_1<VAR>G : Type u_5<VAR>NormedAddCommGroup G<VAR>NormedSpace ℝ G<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f : α → G<VAR>g : α → ℝ<VAR>hg : MeasureTheory.Integrable g μ<VAR>h : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ g x<GOAL>‖∫ (x : α), f x ∂μ‖ ≤ ∫ (x : α), g x ∂μ
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>hE : CompleteSpace E<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f : MeasureTheory.SimpleFunc α E<VAR>hfi : MeasureTheory.Integrable (↑f) μ<GOAL>MeasureTheory.SimpleFunc.integral μ f = ∫ (x : α), ↑f x ∂μ