ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>E : Type u_1<VAR>f f' : ℝ → E<VAR>a : ℝ<VAR>m : E<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>CompleteSpace E<VAR>hcont : ContinuousWithinAt f (Set.Iic a) a<VAR>hderiv : ∀ x ∈ Set.Iio a, HasDerivAt f (f' x) x<VAR>f'int : MeasureTheory.IntegrableOn f' (Set.Iic a) MeasureTheory.volume<VAR>hf : Filter.Tendsto f Filter.atBot (𝓝 m)<GOAL>∫ (x : ℝ) in Set.Iic a, f' x = f a - m
<VAR>E : Type u_1<VAR>f f' : ℝ → E<VAR>a : ℝ<VAR>m : E<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>CompleteSpace E<VAR>hderiv : ∀ x ∈ Set.Iic a, HasDerivAt f (f' x) x<VAR>f'int : MeasureTheory.IntegrableOn f' (Set.Iic a) MeasureTheory.volume<VAR>hf : Filter.Tendsto f Filter.atBot (𝓝 m)<GOAL>∫ (x : ℝ) in Set.Iic a, f' x = f a - m
<VAR>E : Type u_1<VAR>f : ℝ → E<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>CompleteSpace E<VAR>hf : ContDiff ℝ 1 f<VAR>h2f : HasCompactSupport f<VAR>b : ℝ<GOAL>∫ (x : ℝ) in Set.Iic b, deriv f x = f b
<VAR>F : Type u_2<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>f : ℝ → F<VAR>hf : ContDiff ℝ 1 f<VAR>h'f : HasCompactSupport f<VAR>x : ℝ<GOAL>↑‖f x‖₊ ≤ ∫⁻ (y : ℝ) in Set.Iic x, ↑‖deriv f y‖₊
<VAR>E : Type u_1<VAR>f f' : ℝ → E<VAR>m n : E<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>CompleteSpace E<VAR>hderiv : ∀ (x : ℝ), HasDerivAt f (f' x) x<VAR>hf' : MeasureTheory.Integrable f' MeasureTheory.volume<VAR>hbot : Filter.Tendsto f Filter.atBot (𝓝 m)<VAR>htop : Filter.Tendsto f Filter.atTop (𝓝 n)<GOAL>∫ (x : ℝ), f' x = n - m
<VAR>E : Type u_1<VAR>f f' : ℝ → E<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>hderiv : ∀ (x : ℝ), HasDerivAt f (f' x) x<VAR>hf' : MeasureTheory.Integrable f' MeasureTheory.volume<VAR>hf : MeasureTheory.Integrable f MeasureTheory.volume<GOAL>∫ (x : ℝ), f' x = 0
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>f f' : ℝ → ℝ<VAR>g : ℝ → E<VAR>a : ℝ<VAR>hf : ContinuousOn f (Set.Ici a)<VAR>hft : Filter.Tendsto f Filter.atTop Filter.atTop<VAR>hff' : ∀ x ∈ Set.Ioi a, HasDerivWithinAt f (f' x) (Set.Ioi x) x<VAR>hg_cont : ContinuousOn g (f '' Set.Ioi a)<VAR>hg1 : MeasureTheory.IntegrableOn g (f '' Set.Ici a) MeasureTheory.volume<VAR>hg2 : MeasureTheory.IntegrableOn (fun x => f' x • (g ∘ f) x) (Set.Ici a) MeasureTheory.volume<GOAL>∫ (x : ℝ) in Set.Ioi a, f' x • (g ∘ f) x = ∫ (u : ℝ) in Set.Ioi (f a), g u
<VAR>f f' g : ℝ → ℝ<VAR>a : ℝ<VAR>hf : ContinuousOn f (Set.Ici a)<VAR>hft : Filter.Tendsto f Filter.atTop Filter.atTop<VAR>hff' : ∀ x ∈ Set.Ioi a, HasDerivWithinAt f (f' x) (Set.Ioi x) x<VAR>hg_cont : ContinuousOn g (f '' Set.Ioi a)<VAR>hg1 : MeasureTheory.IntegrableOn g (f '' Set.Ici a) MeasureTheory.volume<VAR>hg2 : MeasureTheory.IntegrableOn (fun x => (g ∘ f) x * f' x) (Set.Ici a) MeasureTheory.volume<GOAL>∫ (x : ℝ) in Set.Ioi a, (g ∘ f) x * f' x = ∫ (u : ℝ) in Set.Ioi (f a), g u
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>g : ℝ → E<VAR>p : ℝ<VAR>hp : p ≠ 0<GOAL>∫ (x : ℝ) in Set.Ioi 0, (|p| * x ^ (p - 1)) • g (x ^ p) = ∫ (y : ℝ) in Set.Ioi 0, g y
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>g : ℝ → E<VAR>p : ℝ<VAR>hp : 0 < p<GOAL>∫ (x : ℝ) in Set.Ioi 0, (p * x ^ (p - 1)) • g (x ^ p) = ∫ (y : ℝ) in Set.Ioi 0, g y
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>g : ℝ → E<VAR>a : ℝ<VAR>b : ℝ<VAR>hb : 0 < b<GOAL>∫ (x : ℝ) in Set.Ioi a, g (b * x) = b⁻¹ • ∫ (x : ℝ) in Set.Ioi (b * a), g x
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>g : ℝ → E<VAR>a : ℝ<VAR>b : ℝ<VAR>hb : 0 < b<GOAL>∫ (x : ℝ) in Set.Ioi a, g (x * b) = b⁻¹ • ∫ (x : ℝ) in Set.Ioi (a * b), g x
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>f : ℝ → E<VAR>p : ℝ<VAR>hp : p ≠ 0<GOAL>MeasureTheory.IntegrableOn (fun x => (|p| * x ^ (p - 1)) • f (x ^ p)) (Set.Ioi 0) MeasureTheory.volume ↔ MeasureTheory.IntegrableOn f (Set.Ioi 0) MeasureTheory.volume
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>f : ℝ → E<VAR>p : ℝ<VAR>hp : p ≠ 0<GOAL>MeasureTheory.IntegrableOn (fun x => x ^ (p - 1) • f (x ^ p)) (Set.Ioi 0) MeasureTheory.volume ↔ MeasureTheory.IntegrableOn f (Set.Ioi 0) MeasureTheory.volume
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>f : ℝ → E<VAR>c : ℝ<VAR>a : ℝ<VAR>ha : 0 < a<GOAL>MeasureTheory.IntegrableOn (fun x => f (a * x)) (Set.Ioi c) MeasureTheory.volume ↔ MeasureTheory.IntegrableOn f (Set.Ioi (a * c)) MeasureTheory.volume
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>f : ℝ → E<VAR>c : ℝ<VAR>a : ℝ<VAR>ha : 0 < a<GOAL>MeasureTheory.IntegrableOn (fun x => f (x * a)) (Set.Ioi c) MeasureTheory.volume ↔ MeasureTheory.IntegrableOn f (Set.Ioi (c * a)) MeasureTheory.volume
<VAR>E : Type u_1<VAR>F : Type u_2<VAR>G : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>NormedAddCommGroup G<VAR>NormedSpace ℝ G<VAR>L : E →L[ℝ] F →L[ℝ] G<VAR>u : ℝ → E<VAR>v : ℝ → F<VAR>u' : ℝ → E<VAR>v' : ℝ → F<VAR>m n : G<VAR>CompleteSpace G<VAR>hu : ∀ (x : ℝ), HasDerivAt u (u' x) x<VAR>hv : ∀ (x : ℝ), HasDerivAt v (v' x) x<VAR>huv : MeasureTheory.Integrable (fun x => (L (u x)) (v' x) + (L (u' x)) (v x)) MeasureTheory.volume<VAR>h_bot : Filter.Tendsto (fun x => (L (u x)) (v x)) Filter.atBot (𝓝 m)<VAR>h_top : Filter.Tendsto (fun x => (L (u x)) (v x)) Filter.atTop (𝓝 n)<GOAL>∫ (x : ℝ), (L (u x)) (v' x) + (L (u' x)) (v x) = n - m
<VAR>E : Type u_1<VAR>F : Type u_2<VAR>G : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>NormedAddCommGroup G<VAR>NormedSpace ℝ G<VAR>L : E →L[ℝ] F →L[ℝ] G<VAR>u : ℝ → E<VAR>v : ℝ → F<VAR>u' : ℝ → E<VAR>v' : ℝ → F<VAR>m n : G<VAR>CompleteSpace G<VAR>hu : ∀ (x : ℝ), HasDerivAt u (u' x) x<VAR>hv : ∀ (x : ℝ), HasDerivAt v (v' x) x<VAR>huv' : MeasureTheory.Integrable (fun x => (L (u x)) (v' x)) MeasureTheory.volume<VAR>hu'v : MeasureTheory.Integrable (fun x => (L (u' x)) (v x)) MeasureTheory.volume<VAR>h_bot : Filter.Tendsto (fun x => (L (u x)) (v x)) Filter.atBot (𝓝 m)<VAR>h_top : Filter.Tendsto (fun x => (L (u x)) (v x)) Filter.atTop (𝓝 n)<GOAL>∫ (x : ℝ), (L (u x)) (v' x) = n - m - ∫ (x : ℝ), (L (u' x)) (v x)
<VAR>E : Type u_1<VAR>F : Type u_2<VAR>G : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>NormedAddCommGroup G<VAR>NormedSpace ℝ G<VAR>L : E →L[ℝ] F →L[ℝ] G<VAR>u : ℝ → E<VAR>v : ℝ → F<VAR>u' : ℝ → E<VAR>v' : ℝ → F<VAR>hu : ∀ (x : ℝ), HasDerivAt u (u' x) x<VAR>hv : ∀ (x : ℝ), HasDerivAt v (v' x) x<VAR>huv' : MeasureTheory.Integrable (fun x => (L (u x)) (v' x)) MeasureTheory.volume<VAR>hu'v : MeasureTheory.Integrable (fun x => (L (u' x)) (v x)) MeasureTheory.volume<VAR>huv : MeasureTheory.Integrable (fun x => (L (u x)) (v x)) MeasureTheory.volume<GOAL>∫ (x : ℝ), (L (u x)) (v' x) = -∫ (x : ℝ), (L (u' x)) (v x)
<VAR>A : Type u_1<VAR>NormedRing A<VAR>NormedAlgebra ℝ A<VAR>a' b' : A<VAR>u v u' v' : ℝ → A<VAR>CompleteSpace A<VAR>hu : ∀ (x : ℝ), HasDerivAt u (u' x) x<VAR>hv : ∀ (x : ℝ), HasDerivAt v (v' x) x<VAR>huv : MeasureTheory.Integrable (u' * v + u * v') MeasureTheory.volume<VAR>h_bot : Filter.Tendsto (u * v) Filter.atBot (𝓝 a')<VAR>h_top : Filter.Tendsto (u * v) Filter.atTop (𝓝 b')<GOAL>∫ (x : ℝ), u' x * v x + u x * v' x = b' - a'
<VAR>A : Type u_1<VAR>NormedRing A<VAR>NormedAlgebra ℝ A<VAR>a' b' : A<VAR>u v u' v' : ℝ → A<VAR>CompleteSpace A<VAR>hu : ∀ (x : ℝ), HasDerivAt u (u' x) x<VAR>hv : ∀ (x : ℝ), HasDerivAt v (v' x) x<VAR>huv' : MeasureTheory.Integrable (u * v') MeasureTheory.volume<VAR>hu'v : MeasureTheory.Integrable (u' * v) MeasureTheory.volume<VAR>h_bot : Filter.Tendsto (u * v) Filter.atBot (𝓝 a')<VAR>h_top : Filter.Tendsto (u * v) Filter.atTop (𝓝 b')<GOAL>∫ (x : ℝ), u x * v' x = b' - a' - ∫ (x : ℝ), u' x * v x
<VAR>A : Type u_1<VAR>NormedRing A<VAR>NormedAlgebra ℝ A<VAR>u v u' v' : ℝ → A<VAR>hu : ∀ (x : ℝ), HasDerivAt u (u' x) x<VAR>hv : ∀ (x : ℝ), HasDerivAt v (v' x) x<VAR>huv' : MeasureTheory.Integrable (u * v') MeasureTheory.volume<VAR>hu'v : MeasureTheory.Integrable (u' * v) MeasureTheory.volume<VAR>huv : MeasureTheory.Integrable (u * v) MeasureTheory.volume<GOAL>∫ (x : ℝ), u x * v' x = -∫ (x : ℝ), u' x * v x
<VAR>A : Type u_1<VAR>NormedRing A<VAR>NormedAlgebra ℝ A<VAR>a : ℝ<VAR>a' b' : A<VAR>u v u' v' : ℝ → A<VAR>CompleteSpace A<VAR>hu : ∀ x ∈ Set.Ioi a, HasDerivAt u (u' x) x<VAR>hv : ∀ x ∈ Set.Ioi a, HasDerivAt v (v' x) x<VAR>huv : MeasureTheory.IntegrableOn (u' * v + u * v') (Set.Ioi a) MeasureTheory.volume<VAR>h_zero : Filter.Tendsto (u * v) (𝓝[>] a) (𝓝 a')<VAR>h_infty : Filter.Tendsto (u * v) Filter.atTop (𝓝 b')<GOAL>∫ (x : ℝ) in Set.Ioi a, u' x * v x + u x * v' x = b' - a'
<VAR>A : Type u_1<VAR>NormedRing A<VAR>NormedAlgebra ℝ A<VAR>a : ℝ<VAR>a' b' : A<VAR>u v u' v' : ℝ → A<VAR>CompleteSpace A<VAR>hu : ∀ x ∈ Set.Ioi a, HasDerivAt u (u' x) x<VAR>hv : ∀ x ∈ Set.Ioi a, HasDerivAt v (v' x) x<VAR>huv' : MeasureTheory.IntegrableOn (u * v') (Set.Ioi a) MeasureTheory.volume<VAR>hu'v : MeasureTheory.IntegrableOn (u' * v) (Set.Ioi a) MeasureTheory.volume<VAR>h_zero : Filter.Tendsto (u * v) (𝓝[>] a) (𝓝 a')<VAR>h_infty : Filter.Tendsto (u * v) Filter.atTop (𝓝 b')<GOAL>∫ (x : ℝ) in Set.Ioi a, u x * v' x = b' - a' - ∫ (x : ℝ) in Set.Ioi a, u' x * v x
<VAR>A : Type u_1<VAR>NormedRing A<VAR>NormedAlgebra ℝ A<VAR>a : ℝ<VAR>a' b' : A<VAR>u v u' v' : ℝ → A<VAR>CompleteSpace A<VAR>hu : ∀ x ∈ Set.Iio a, HasDerivAt u (u' x) x<VAR>hv : ∀ x ∈ Set.Iio a, HasDerivAt v (v' x) x<VAR>huv : MeasureTheory.IntegrableOn (u' * v + u * v') (Set.Iic a) MeasureTheory.volume<VAR>h_zero : Filter.Tendsto (u * v) (𝓝[<] a) (𝓝 a')<VAR>h_infty : Filter.Tendsto (u * v) Filter.atBot (𝓝 b')<GOAL>∫ (x : ℝ) in Set.Iic a, u' x * v x + u x * v' x = a' - b'
<VAR>A : Type u_1<VAR>NormedRing A<VAR>NormedAlgebra ℝ A<VAR>a : ℝ<VAR>a' b' : A<VAR>u v u' v' : ℝ → A<VAR>CompleteSpace A<VAR>hu : ∀ x ∈ Set.Iio a, HasDerivAt u (u' x) x<VAR>hv : ∀ x ∈ Set.Iio a, HasDerivAt v (v' x) x<VAR>huv' : MeasureTheory.IntegrableOn (u * v') (Set.Iic a) MeasureTheory.volume<VAR>hu'v : MeasureTheory.IntegrableOn (u' * v) (Set.Iic a) MeasureTheory.volume<VAR>h_zero : Filter.Tendsto (u * v) (𝓝[<] a) (𝓝 a')<VAR>h_infty : Filter.Tendsto (u * v) Filter.atBot (𝓝 b')<GOAL>∫ (x : ℝ) in Set.Iic a, u x * v' x = a' - b' - ∫ (x : ℝ) in Set.Iic a, u' x * v x
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<GOAL>⨍⁻ (_x : α), 0 ∂μ = 0
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>f : α → ℝ≥0∞<GOAL>⨍⁻ (x : α), f x ∂0 = 0
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f : α → ℝ≥0∞<GOAL>⨍⁻ (x : α), f x ∂μ = ∫⁻ (x : α), f x ∂(μ Set.univ)⁻¹ • μ
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f : α → ℝ≥0∞<GOAL>⨍⁻ (x : α), f x ∂μ = (∫⁻ (x : α), f x ∂μ) / μ Set.univ
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>MeasureTheory.IsProbabilityMeasure μ<VAR>f : α → ℝ≥0∞<GOAL>⨍⁻ (x : α), f x ∂μ = ∫⁻ (x : α), f x ∂μ
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>f : α → ℝ≥0∞<GOAL>μ Set.univ * ⨍⁻ (x : α), f x ∂μ = ∫⁻ (x : α), f x ∂μ
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f : α → ℝ≥0∞<VAR>s : Set α<GOAL>⨍⁻ (x : α) in s, f x ∂μ = (∫⁻ (x : α) in s, f x ∂μ) / μ s
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f : α → ℝ≥0∞<VAR>s : Set α<GOAL>⨍⁻ (x : α) in s, f x ∂μ = ∫⁻ (x : α), f x ∂(μ s)⁻¹ • μ.restrict s
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f g : α → ℝ≥0∞<VAR>h : f =ᵐ[μ] g<GOAL>⨍⁻ (x : α), f x ∂μ = ⨍⁻ (x : α), g x ∂μ
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s t : Set α<VAR>f : α → ℝ≥0∞<VAR>h : s =ᵐ[μ] t<GOAL>⨍⁻ (x : α) in s, f x ∂μ = ⨍⁻ (x : α) in t, f x ∂μ
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s : Set α<VAR>f g : α → ℝ≥0∞<VAR>hs : MeasurableSet s<VAR>h : ∀ᵐ (x : α) ∂μ, x ∈ s → f x = g x<GOAL>⨍⁻ (x : α) in s, f x ∂μ = ⨍⁻ (x : α) in s, g x ∂μ
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f : α → ℝ≥0∞<VAR>hf : ∫⁻ (x : α), f x ∂μ ≠ ⊤<GOAL>⨍⁻ (x : α), f x ∂μ < ⊤
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s : Set α<VAR>f : α → ℝ≥0∞<GOAL>∫⁻ (x : α) in s, f x ∂μ ≠ ⊤ → ⨍⁻ (x : α) in s, f x ∂μ < ⊤
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ ν : MeasureTheory.Measure α<VAR>f : α → ℝ≥0∞<GOAL>⨍⁻ (x : α), f x ∂(μ + ν) = μ Set.univ / (μ Set.univ + ν Set.univ) * ⨍⁻ (x : α), f x ∂μ + ν Set.univ / (μ Set.univ + ν Set.univ) * ⨍⁻ (x : α), f x ∂ν
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s : Set α<VAR>f : α → ℝ≥0∞<VAR>h : μ s ≠ ⊤<GOAL>μ s * ⨍⁻ (x : α) in s, f x ∂μ = ∫⁻ (x : α) in s, f x ∂μ
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s t : Set α<VAR>f : α → ℝ≥0∞<VAR>hd : MeasureTheory.AEDisjoint μ s t<VAR>ht : MeasureTheory.NullMeasurableSet t μ<GOAL>⨍⁻ (x : α) in s ∪ t, f x ∂μ = μ s / (μ s + μ t) * ⨍⁻ (x : α) in s, f x ∂μ + μ t / (μ s + μ t) * ⨍⁻ (x : α) in t, f x ∂μ
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s t : Set α<VAR>f : α → ℝ≥0∞<VAR>hd : MeasureTheory.AEDisjoint μ s t<VAR>ht : MeasureTheory.NullMeasurableSet t μ<VAR>hs₀ : μ s ≠ 0<VAR>ht₀ : μ t ≠ 0<VAR>hsμ : μ s ≠ ⊤<VAR>htμ : μ t ≠ ⊤<GOAL>⨍⁻ (x : α) in s ∪ t, f x ∂μ ∈ openSegment ℝ≥0∞ (⨍⁻ (x : α) in s, f x ∂μ) (⨍⁻ (x : α) in t, f x ∂μ)
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s t : Set α<VAR>f : α → ℝ≥0∞<VAR>hd : MeasureTheory.AEDisjoint μ s t<VAR>ht : MeasureTheory.NullMeasurableSet t μ<VAR>hsμ : μ s ≠ ⊤<VAR>htμ : μ t ≠ ⊤<GOAL>⨍⁻ (x : α) in s ∪ t, f x ∂μ ∈ [⨍⁻ (x : α) in s, f x ∂μ-[ℝ≥0∞]⨍⁻ (x : α) in t, f x ∂μ]
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s : Set α<VAR>f : α → ℝ≥0∞<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>hs : MeasureTheory.NullMeasurableSet s μ<VAR>hs₀ : μ s ≠ 0<VAR>hsc₀ : μ sᶜ ≠ 0<GOAL>⨍⁻ (x : α), f x ∂μ ∈ openSegment ℝ≥0∞ (⨍⁻ (x : α) in s, f x ∂μ) (⨍⁻ (x : α) in sᶜ, f x ∂μ)
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>h : NeZero μ<VAR>c : ℝ≥0∞<GOAL>⨍⁻ (_x : α), c ∂μ = c
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s : Set α<VAR>hs₀ : μ s ≠ 0<VAR>hs : μ s ≠ ⊤<VAR>c : ℝ≥0∞<GOAL>⨍⁻ (_x : α) in s, c ∂μ = c
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>NeZero μ<GOAL>⨍⁻ (_x : α), 1 ∂μ = 1
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s : Set α<VAR>hs₀ : μ s ≠ 0<VAR>hs : μ s ≠ ⊤<GOAL>⨍⁻ (_x : α) in s, 1 ∂μ = 1
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>f : α → ℝ≥0∞<GOAL>∫⁻ (_x : α), ⨍⁻ (a : α), f a ∂μ ∂μ = ∫⁻ (x : α), f x ∂μ
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>f : α → ℝ≥0∞<VAR>s : Set α<GOAL>∫⁻ (_x : α) in s, ⨍⁻ (a : α) in s, f a ∂μ ∂μ = ∫⁻ (x : α) in s, f x ∂μ
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m0 : MeasurableSpace α<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>μ : MeasureTheory.Measure α<GOAL>⨍ (x : α), 0 ∂μ = 0
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m0 : MeasurableSpace α<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>f : α → E<GOAL>⨍ (x : α), f x ∂0 = 0
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m0 : MeasurableSpace α<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>μ : MeasureTheory.Measure α<VAR>f : α → E<GOAL>⨍ (x : α), -f x ∂μ = -⨍ (x : α), f x ∂μ
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m0 : MeasurableSpace α<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>μ : MeasureTheory.Measure α<VAR>f : α → E<GOAL>⨍ (x : α), f x ∂μ = ∫ (x : α), f x ∂(μ Set.univ)⁻¹ • μ
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m0 : MeasurableSpace α<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>μ : MeasureTheory.Measure α<VAR>f : α → E<GOAL>⨍ (x : α), f x ∂μ = (μ Set.univ).toReal⁻¹ • ∫ (x : α), f x ∂μ
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m0 : MeasurableSpace α<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>μ : MeasureTheory.Measure α<VAR>MeasureTheory.IsProbabilityMeasure μ<VAR>f : α → E<GOAL>⨍ (x : α), f x ∂μ = ∫ (x : α), f x ∂μ
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m0 : MeasurableSpace α<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>μ : MeasureTheory.Measure α<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>f : α → E<GOAL>(μ Set.univ).toReal • ⨍ (x : α), f x ∂μ = ∫ (x : α), f x ∂μ
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m0 : MeasurableSpace α<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>μ : MeasureTheory.Measure α<VAR>f : α → E<VAR>s : Set α<GOAL>⨍ (x : α) in s, f x ∂μ = (μ s).toReal⁻¹ • ∫ (x : α) in s, f x ∂μ
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m0 : MeasurableSpace α<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>μ : MeasureTheory.Measure α<VAR>f : α → E<VAR>s : Set α<GOAL>⨍ (x : α) in s, f x ∂μ = ∫ (x : α), f x ∂(μ s)⁻¹ • μ.restrict s
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m0 : MeasurableSpace α<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>μ : MeasureTheory.Measure α<VAR>f g : α → E<VAR>h : f =ᵐ[μ] g<GOAL>⨍ (x : α), f x ∂μ = ⨍ (x : α), g x ∂μ
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m0 : MeasurableSpace α<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>μ : MeasureTheory.Measure α<VAR>s t : Set α<VAR>f : α → E<VAR>h : s =ᵐ[μ] t<GOAL>⨍ (x : α) in s, f x ∂μ = ⨍ (x : α) in t, f x ∂μ
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m0 : MeasurableSpace α<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>μ : MeasureTheory.Measure α<VAR>s : Set α<VAR>f g : α → E<VAR>hs : MeasurableSet s<VAR>h : ∀ᵐ (x : α) ∂μ, x ∈ s → f x = g x<GOAL>⨍ (x : α) in s, f x ∂μ = ⨍ (x : α) in s, g x ∂μ
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m0 : MeasurableSpace α<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>μ : MeasureTheory.Measure α<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>ν : MeasureTheory.Measure α<VAR>MeasureTheory.IsFiniteMeasure ν<VAR>f : α → E<VAR>hμ : MeasureTheory.Integrable f μ<VAR>hν : MeasureTheory.Integrable f ν<GOAL>⨍ (x : α), f x ∂(μ + ν) = ((μ Set.univ).toReal / ((μ Set.univ).toReal + (ν Set.univ).toReal)) • ⨍ (x : α), f x ∂μ + ((ν Set.univ).toReal / ((μ Set.univ).toReal + (ν Set.univ).toReal)) • ⨍ (x : α), f x ∂ν
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>m0 : MeasurableSpace α<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>CompleteSpace E<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>CompleteSpace F<VAR>μ : MeasureTheory.Measure α<VAR>f : α → E<VAR>g : α → F<VAR>hfi : MeasureTheory.Integrable f μ<VAR>hgi : MeasureTheory.Integrable g μ<GOAL>⨍ (x : α), (f x, g x) ∂μ = (⨍ (x : α), f x ∂μ, ⨍ (x : α), g x ∂μ)
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m0 : MeasurableSpace α<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>μ : MeasureTheory.Measure α<VAR>f : α → E<VAR>s : Set α<VAR>h : μ s ≠ ⊤<GOAL>(μ s).toReal • ⨍ (x : α) in s, f x ∂μ = ∫ (x : α) in s, f x ∂μ
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m0 : MeasurableSpace α<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>μ : MeasureTheory.Measure α<VAR>f : α → E<VAR>s t : Set α<VAR>hd : MeasureTheory.AEDisjoint μ s t<VAR>ht : MeasureTheory.NullMeasurableSet t μ<VAR>hsμ : μ s ≠ ⊤<VAR>htμ : μ t ≠ ⊤<VAR>hfs : MeasureTheory.IntegrableOn f s μ<VAR>hft : MeasureTheory.IntegrableOn f t μ<GOAL>⨍ (x : α) in s ∪ t, f x ∂μ = ((μ s).toReal / ((μ s).toReal + (μ t).toReal)) • ⨍ (x : α) in s, f x ∂μ + ((μ t).toReal / ((μ s).toReal + (μ t).toReal)) • ⨍ (x : α) in t, f x ∂μ
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m0 : MeasurableSpace α<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>μ : MeasureTheory.Measure α<VAR>f : α → E<VAR>s t : Set α<VAR>hd : MeasureTheory.AEDisjoint μ s t<VAR>ht : MeasureTheory.NullMeasurableSet t μ<VAR>hs₀ : μ s ≠ 0<VAR>ht₀ : μ t ≠ 0<VAR>hsμ : μ s ≠ ⊤<VAR>htμ : μ t ≠ ⊤<VAR>hfs : MeasureTheory.IntegrableOn f s μ<VAR>hft : MeasureTheory.IntegrableOn f t μ<GOAL>⨍ (x : α) in s ∪ t, f x ∂μ ∈ openSegment ℝ (⨍ (x : α) in s, f x ∂μ) (⨍ (x : α) in t, f x ∂μ)
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m0 : MeasurableSpace α<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>μ : MeasureTheory.Measure α<VAR>f : α → E<VAR>s t : Set α<VAR>hd : MeasureTheory.AEDisjoint μ s t<VAR>ht : MeasureTheory.NullMeasurableSet t μ<VAR>hsμ : μ s ≠ ⊤<VAR>htμ : μ t ≠ ⊤<VAR>hfs : MeasureTheory.IntegrableOn f s μ<VAR>hft : MeasureTheory.IntegrableOn f t μ<GOAL>⨍ (x : α) in s ∪ t, f x ∂μ ∈ [⨍ (x : α) in s, f x ∂μ-[ℝ]⨍ (x : α) in t, f x ∂μ]
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m0 : MeasurableSpace α<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>μ : MeasureTheory.Measure α<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>f : α → E<VAR>s : Set α<VAR>hs : MeasureTheory.NullMeasurableSet s μ<VAR>hs₀ : μ s ≠ 0<VAR>hsc₀ : μ sᶜ ≠ 0<VAR>hfi : MeasureTheory.Integrable f μ<GOAL>⨍ (x : α), f x ∂μ ∈ openSegment ℝ (⨍ (x : α) in s, f x ∂μ) (⨍ (x : α) in sᶜ, f x ∂μ)
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m0 : MeasurableSpace α<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>CompleteSpace E<VAR>μ : MeasureTheory.Measure α<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>h : NeZero μ<VAR>c : E<GOAL>⨍ (_x : α), c ∂μ = c
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m0 : MeasurableSpace α<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>CompleteSpace E<VAR>μ : MeasureTheory.Measure α<VAR>s : Set α<VAR>hs₀ : μ s ≠ 0<VAR>hs : μ s ≠ ⊤<VAR>c : E<GOAL>⨍ (x : α) in s, c ∂μ = c
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m0 : MeasurableSpace α<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>CompleteSpace E<VAR>μ : MeasureTheory.Measure α<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>f : α → E<GOAL>∫ (x : α), ⨍ (a : α), f a ∂μ ∂μ = ∫ (x : α), f x ∂μ
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m0 : MeasurableSpace α<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>CompleteSpace E<VAR>μ : MeasureTheory.Measure α<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>f : α → E<VAR>s : Set α<GOAL>∫ (x : α) in s, ⨍ (a : α) in s, f a ∂μ ∂μ = ∫ (x : α) in s, f x ∂μ
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m0 : MeasurableSpace α<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>CompleteSpace E<VAR>μ : MeasureTheory.Measure α<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>f : α → E<GOAL>∫ (x : α), f x - ⨍ (a : α), f a ∂μ ∂μ = 0
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m0 : MeasurableSpace α<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>CompleteSpace E<VAR>μ : MeasureTheory.Measure α<VAR>s : Set α<VAR>hs : μ s ≠ ⊤<VAR>f : α → E<GOAL>∫ (x : α) in s, f x - ⨍ (a : α) in s, f a ∂μ ∂μ = 0
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m0 : MeasurableSpace α<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>CompleteSpace E<VAR>μ : MeasureTheory.Measure α<VAR>f : α → E<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>hf : MeasureTheory.Integrable f μ<GOAL>∫ (x : α), ⨍ (a : α), f a ∂μ - f x ∂μ = 0
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m0 : MeasurableSpace α<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>CompleteSpace E<VAR>μ : MeasureTheory.Measure α<VAR>s : Set α<VAR>f : α → E<VAR>hs : μ s ≠ ⊤<VAR>hf : MeasureTheory.IntegrableOn f s μ<GOAL>∫ (x : α) in s, ⨍ (a : α) in s, f a ∂μ - f x ∂μ = 0
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f : α → ℝ<VAR>hf : MeasureTheory.Integrable f μ<VAR>hf₀ : 0 ≤ᵐ[μ] f<GOAL>ENNReal.ofReal (⨍ (x : α), f x ∂μ) = (∫⁻ (x : α), ENNReal.ofReal (f x) ∂μ) / μ Set.univ
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s : Set α<VAR>f : α → ℝ<VAR>hf : MeasureTheory.IntegrableOn f s μ<VAR>hf₀ : 0 ≤ᵐ[μ.restrict s] f<GOAL>ENNReal.ofReal (⨍ (x : α) in s, f x ∂μ) = (∫⁻ (x : α) in s, ENNReal.ofReal (f x) ∂μ) / μ s
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f : α → ℝ≥0∞<VAR>hf : AEMeasurable f μ<VAR>hf' : ∀ᵐ (x : α) ∂μ, f x ≠ ⊤<GOAL>(⨍⁻ (x : α), f x ∂μ).toReal = ⨍ (x : α), (f x).toReal ∂μ
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s : Set α<VAR>f : α → ℝ≥0∞<VAR>hf : AEMeasurable f (μ.restrict s)<VAR>hf' : ∀ᵐ (x : α) ∂μ.restrict s, f x ≠ ⊤<GOAL>(⨍⁻ (x : α) in s, f x ∂μ).toReal = ⨍ (x : α) in s, (f x).toReal ∂μ
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s : Set α<VAR>f : α → ℝ<VAR>hμ : μ s ≠ 0<VAR>hμ₁ : μ s ≠ ⊤<VAR>hf : MeasureTheory.IntegrableOn f s μ<GOAL>0 < μ {x | x ∈ s ∧ f x ≤ ⨍ (a : α) in s, f a ∂μ}