ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>μ : MeasureTheory.Measure ℝ<VAR>MeasureTheory.IsLocallyFiniteMeasure μ<VAR>ConditionallyCompleteLinearOrder E<VAR>OrderTopology E<VAR>SecondCountableTopology E<VAR>u : ℝ → E<VAR>a b : ℝ<VAR>hu : Antitone u<GOAL>IntervalIntegrable u μ a b
<VAR>ι : Type u_1<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>f : ℝ → E<VAR>μ : MeasureTheory.Measure ℝ<VAR>l l' : Filter ℝ<VAR>hfm : StronglyMeasurableAtFilter f l' μ<VAR>Filter.TendstoIxxClass Set.Ioc l l'<VAR>l'.IsMeasurablyGenerated<VAR>hμ : μ.FiniteAtFilter l'<VAR>c : E<VAR>hf : Filter.Tendsto f (l' ⊓ MeasureTheory.ae μ) (𝓝 c)<VAR>u v : ι → ℝ<VAR>lt : Filter ι<VAR>hu : Filter.Tendsto u lt l<VAR>hv : Filter.Tendsto v lt l<GOAL>∀ᶠ (t : ι) in lt, IntervalIntegrable f μ (u t) (v t)
<VAR>ι : Type u_1<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>f : ℝ → E<VAR>μ : MeasureTheory.Measure ℝ<VAR>l l' : Filter ℝ<VAR>hfm : StronglyMeasurableAtFilter f l' μ<VAR>Filter.TendstoIxxClass Set.Ioc l l'<VAR>l'.IsMeasurablyGenerated<VAR>hμ : μ.FiniteAtFilter l'<VAR>c : E<VAR>hf : Filter.Tendsto f l' (𝓝 c)<VAR>u v : ι → ℝ<VAR>lt : Filter ι<VAR>hu : Filter.Tendsto u lt l<VAR>hv : Filter.Tendsto v lt l<GOAL>∀ᶠ (t : ι) in lt, IntervalIntegrable f μ (u t) (v t)
<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>a b : ℝ<VAR>μ : MeasureTheory.Measure ℝ<GOAL>∫ (x : ℝ) in a..b, 0 ∂μ = 0
<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>a b : ℝ<VAR>f : ℝ → E<VAR>μ : MeasureTheory.Measure ℝ<VAR>h : a ≤ b<GOAL>∫ (x : ℝ) in a..b, f x ∂μ = ∫ (x : ℝ) in Set.Ioc a b, f x ∂μ
<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>a : ℝ<VAR>f : ℝ → E<VAR>μ : MeasureTheory.Measure ℝ<GOAL>∫ (x : ℝ) in a..a, f x ∂μ = 0
<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>f : ℝ → E<VAR>μ : MeasureTheory.Measure ℝ<VAR>a b : ℝ<GOAL>∫ (x : ℝ) in b..a, f x ∂μ = -∫ (x : ℝ) in a..b, f x ∂μ
<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>a b : ℝ<VAR>f : ℝ → E<VAR>μ : MeasureTheory.Measure ℝ<VAR>h : b ≤ a<GOAL>∫ (x : ℝ) in a..b, f x ∂μ = -∫ (x : ℝ) in Set.Ioc b a, f x ∂μ
<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>f : ℝ → E<VAR>a b : ℝ<VAR>μ : MeasureTheory.Measure ℝ<GOAL>∫ (x : ℝ) in a..b, f x ∂μ = (if a ≤ b then 1 else -1) • ∫ (x : ℝ) in Ι a b, f x ∂μ
<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>f : ℝ → E<VAR>a b : ℝ<VAR>μ : MeasureTheory.Measure ℝ<GOAL>‖∫ (x : ℝ) in a..b, f x ∂μ‖ = ‖∫ (x : ℝ) in Ι a b, f x ∂μ‖
<VAR>f : ℝ → ℝ<VAR>a b : ℝ<VAR>μ : MeasureTheory.Measure ℝ<GOAL>|∫ (x : ℝ) in a..b, f x ∂μ| = |∫ (x : ℝ) in Ι a b, f x ∂μ|
<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>μ : MeasureTheory.Measure ℝ<VAR>f : ℝ → E<VAR>a b : ℝ<GOAL>∫ (x : ℝ) in a..b, f x ∂μ ∈ {∫ (x : ℝ) in Ι a b, f x ∂μ, -∫ (x : ℝ) in Ι a b, f x ∂μ}
<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>a b : ℝ<VAR>f : ℝ → E<VAR>μ : MeasureTheory.Measure ℝ<VAR>h : ¬IntervalIntegrable f μ a b<GOAL>∫ (x : ℝ) in a..b, f x ∂μ = 0
<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>a b : ℝ<VAR>f : ℝ → E<VAR>μ : MeasureTheory.Measure ℝ<VAR>h : ∫ (x : ℝ) in a..b, f x ∂μ ≠ 0<GOAL>IntervalIntegrable f μ a b
<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>a b : ℝ<VAR>f : ℝ → E<VAR>μ : MeasureTheory.Measure ℝ<VAR>hf : ¬MeasureTheory.AEStronglyMeasurable f (μ.restrict (Ι a b))<GOAL>∫ (x : ℝ) in a..b, f x ∂μ = 0
<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>a b : ℝ<VAR>f : ℝ → E<VAR>μ : MeasureTheory.Measure ℝ<VAR>h : a ≤ b<VAR>hf : ¬MeasureTheory.AEStronglyMeasurable f (μ.restrict (Set.Ioc a b))<GOAL>∫ (x : ℝ) in a..b, f x ∂μ = 0
<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>a b : ℝ<VAR>μ : MeasureTheory.Measure ℝ<VAR>f : ℝ → E<GOAL>‖∫ (x : ℝ) in min a b..max a b, f x ∂μ‖ = ‖∫ (x : ℝ) in a..b, f x ∂μ‖
<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>a b : ℝ<VAR>μ : MeasureTheory.Measure ℝ<VAR>f : ℝ → E<GOAL>‖∫ (x : ℝ) in a..b, f x ∂μ‖ = ‖∫ (x : ℝ) in Ι a b, f x ∂μ‖
<VAR>a b : ℝ<VAR>μ : MeasureTheory.Measure ℝ<VAR>f : ℝ → ℝ<GOAL>|∫ (x : ℝ) in a..b, f x ∂μ| = |∫ (x : ℝ) in Ι a b, f x ∂μ|
<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>a b : ℝ<VAR>f : ℝ → E<VAR>μ : MeasureTheory.Measure ℝ<GOAL>‖∫ (x : ℝ) in a..b, f x ∂μ‖ ≤ ∫ (x : ℝ) in Ι a b, ‖f x‖ ∂μ
<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>a b : ℝ<VAR>f : ℝ → E<VAR>μ : MeasureTheory.Measure ℝ<GOAL>‖∫ (x : ℝ) in a..b, f x ∂μ‖ ≤ |∫ (x : ℝ) in a..b, ‖f x‖ ∂μ|
<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>a b : ℝ<VAR>f : ℝ → E<VAR>μ : MeasureTheory.Measure ℝ<VAR>h : a ≤ b<GOAL>‖∫ (x : ℝ) in a..b, f x ∂μ‖ ≤ ∫ (x : ℝ) in a..b, ‖f x‖ ∂μ
<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>a b : ℝ<VAR>f : ℝ → E<VAR>μ : MeasureTheory.Measure ℝ<VAR>g : ℝ → ℝ<VAR>h : ∀ᵐ (t : ℝ) ∂μ.restrict (Ι a b), ‖f t‖ ≤ g t<VAR>hbound : IntervalIntegrable g μ a b<GOAL>‖∫ (t : ℝ) in a..b, f t ∂μ‖ ≤ |∫ (t : ℝ) in a..b, g t ∂μ|
<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>a b C : ℝ<VAR>f : ℝ → E<VAR>h : ∀ᵐ (x : ℝ), x ∈ Ι a b → ‖f x‖ ≤ C<GOAL>‖∫ (x : ℝ) in a..b, f x‖ ≤ C * |b - a|
<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>a b C : ℝ<VAR>f : ℝ → E<VAR>h : ∀ x ∈ Ι a b, ‖f x‖ ≤ C<GOAL>‖∫ (x : ℝ) in a..b, f x‖ ≤ C * |b - a|
<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>a b : ℝ<VAR>f g : ℝ → E<VAR>μ : MeasureTheory.Measure ℝ<VAR>hf : IntervalIntegrable f μ a b<VAR>hg : IntervalIntegrable g μ a b<GOAL>∫ (x : ℝ) in a..b, f x + g x ∂μ = ∫ (x : ℝ) in a..b, f x ∂μ + ∫ (x : ℝ) in a..b, g x ∂μ
<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>a b : ℝ<VAR>μ : MeasureTheory.Measure ℝ<VAR>ι : Type u_6<VAR>s : Finset ι<VAR>f : ι → ℝ → E<VAR>h : ∀ i ∈ s, IntervalIntegrable (f i) μ a b<GOAL>∫ (x : ℝ) in a..b, ∑ i ∈ s, f i x ∂μ = ∑ i ∈ s, ∫ (x : ℝ) in a..b, f i x ∂μ
<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>a b : ℝ<VAR>f : ℝ → E<VAR>μ : MeasureTheory.Measure ℝ<GOAL>∫ (x : ℝ) in a..b, -f x ∂μ = -∫ (x : ℝ) in a..b, f x ∂μ
<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>a b : ℝ<VAR>f g : ℝ → E<VAR>μ : MeasureTheory.Measure ℝ<VAR>hf : IntervalIntegrable f μ a b<VAR>hg : IntervalIntegrable g μ a b<GOAL>∫ (x : ℝ) in a..b, f x - g x ∂μ = ∫ (x : ℝ) in a..b, f x ∂μ - ∫ (x : ℝ) in a..b, g x ∂μ
<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>a b : ℝ<VAR>μ : MeasureTheory.Measure ℝ<VAR>𝕜 : Type u_6<VAR>NontriviallyNormedField 𝕜<VAR>NormedSpace 𝕜 E<VAR>SMulCommClass ℝ 𝕜 E<VAR>r : 𝕜<VAR>f : ℝ → E<GOAL>∫ (x : ℝ) in a..b, r • f x ∂μ = r • ∫ (x : ℝ) in a..b, f x ∂μ
<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>CompleteSpace E<VAR>NormedSpace ℝ E<VAR>a b : ℝ<VAR>μ : MeasureTheory.Measure ℝ<VAR>𝕜 : Type u_6<VAR>RCLike 𝕜<VAR>NormedSpace 𝕜 E<VAR>f : ℝ → 𝕜<VAR>c : E<GOAL>∫ (x : ℝ) in a..b, f x • c ∂μ = (∫ (x : ℝ) in a..b, f x ∂μ) • c
<VAR>a b : ℝ<VAR>μ : MeasureTheory.Measure ℝ<VAR>𝕜 : Type u_6<VAR>RCLike 𝕜<VAR>r : 𝕜<VAR>f : ℝ → 𝕜<GOAL>∫ (x : ℝ) in a..b, r * f x ∂μ = r * ∫ (x : ℝ) in a..b, f x ∂μ
<VAR>a b : ℝ<VAR>μ : MeasureTheory.Measure ℝ<VAR>𝕜 : Type u_6<VAR>RCLike 𝕜<VAR>r : 𝕜<VAR>f : ℝ → 𝕜<GOAL>∫ (x : ℝ) in a..b, f x * r ∂μ = (∫ (x : ℝ) in a..b, f x ∂μ) * r
<VAR>a b : ℝ<VAR>μ : MeasureTheory.Measure ℝ<VAR>𝕜 : Type u_6<VAR>RCLike 𝕜<VAR>r : 𝕜<VAR>f : ℝ → 𝕜<GOAL>∫ (x : ℝ) in a..b, f x / r ∂μ = (∫ (x : ℝ) in a..b, f x ∂μ) / r
<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>CompleteSpace E<VAR>NormedSpace ℝ E<VAR>a b : ℝ<VAR>μ : MeasureTheory.Measure ℝ<VAR>c : E<GOAL>∫ (x : ℝ) in a..b, c ∂μ = ((μ (Set.Ioc a b)).toReal - (μ (Set.Ioc b a)).toReal) • c
<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>CompleteSpace E<VAR>NormedSpace ℝ E<VAR>a b : ℝ<VAR>c : E<GOAL>∫ (x : ℝ) in a..b, c = (b - a) • c
<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>a b : ℝ<VAR>f : ℝ → E<VAR>μ : MeasureTheory.Measure ℝ<VAR>c : ℝ≥0∞<GOAL>∫ (x : ℝ) in a..b, f x ∂c • μ = c.toReal • ∫ (x : ℝ) in a..b, f x ∂μ
<VAR>𝕜 : Type u_6<VAR>RCLike 𝕜<VAR>a b : ℝ<VAR>μ : MeasureTheory.Measure ℝ<VAR>f : ℝ → ℝ<GOAL>∫ (x : ℝ) in a..b, ↑(f x) ∂μ = ↑(∫ (x : ℝ) in a..b, f x ∂μ)
<VAR>a b : ℝ<VAR>μ : MeasureTheory.Measure ℝ<VAR>f : ℝ → ℝ<GOAL>∫ (x : ℝ) in a..b, ↑(f x) ∂μ = ↑(∫ (x : ℝ) in a..b, f x ∂μ)
<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>μ : MeasureTheory.Measure ℝ<VAR>RCLike 𝕜<VAR>NormedSpace 𝕜 E<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>a b : ℝ<VAR>φ : ℝ → F →L[𝕜] E<VAR>hφ : IntervalIntegrable φ μ a b<VAR>v : F<GOAL>(∫ (x : ℝ) in a..b, φ x ∂μ) v = ∫ (x : ℝ) in a..b, (φ x) v ∂μ
<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>NormedAddCommGroup E<VAR>CompleteSpace E<VAR>NormedSpace ℝ E<VAR>a b : ℝ<VAR>μ : MeasureTheory.Measure ℝ<VAR>f : ℝ → E<VAR>RCLike 𝕜<VAR>NormedSpace 𝕜 E<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>NormedSpace ℝ F<VAR>CompleteSpace F<VAR>L : E →L[𝕜] F<VAR>hf : IntervalIntegrable f μ a b<GOAL>∫ (x : ℝ) in a..b, L (f x) ∂μ = L (∫ (x : ℝ) in a..b, f x ∂μ)
<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>a b c : ℝ<VAR>f : ℝ → E<VAR>hc : c ≠ 0<GOAL>∫ (x : ℝ) in a..b, f (x * c) = c⁻¹ • ∫ (x : ℝ) in a * c..b * c, f x
<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>CompleteSpace E<VAR>NormedSpace ℝ E<VAR>a b : ℝ<VAR>f : ℝ → E<VAR>c : ℝ<GOAL>c • ∫ (x : ℝ) in a..b, f (x * c) = ∫ (x : ℝ) in a * c..b * c, f x
<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>a b c : ℝ<VAR>f : ℝ → E<VAR>hc : c ≠ 0<GOAL>∫ (x : ℝ) in a..b, f (c * x) = c⁻¹ • ∫ (x : ℝ) in c * a..c * b, f x
<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>CompleteSpace E<VAR>NormedSpace ℝ E<VAR>a b : ℝ<VAR>f : ℝ → E<VAR>c : ℝ<GOAL>c • ∫ (x : ℝ) in a..b, f (c * x) = ∫ (x : ℝ) in c * a..c * b, f x
<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>a b c : ℝ<VAR>f : ℝ → E<VAR>hc : c ≠ 0<GOAL>∫ (x : ℝ) in a..b, f (x / c) = c • ∫ (x : ℝ) in a / c..b / c, f x
<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>CompleteSpace E<VAR>NormedSpace ℝ E<VAR>a b : ℝ<VAR>f : ℝ → E<VAR>c : ℝ<GOAL>c⁻¹ • ∫ (x : ℝ) in a..b, f (x / c) = ∫ (x : ℝ) in a / c..b / c, f x
<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>a b : ℝ<VAR>f : ℝ → E<VAR>d : ℝ<GOAL>∫ (x : ℝ) in a..b, f (x + d) = ∫ (x : ℝ) in a + d..b + d, f x
<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>a b : ℝ<VAR>f : ℝ → E<VAR>d : ℝ<GOAL>∫ (x : ℝ) in a..b, f (d + x) = ∫ (x : ℝ) in d + a..d + b, f x
<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>a b c : ℝ<VAR>f : ℝ → E<VAR>hc : c ≠ 0<VAR>d : ℝ<GOAL>∫ (x : ℝ) in a..b, f (c * x + d) = c⁻¹ • ∫ (x : ℝ) in c * a + d..c * b + d, f x
<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>CompleteSpace E<VAR>NormedSpace ℝ E<VAR>a b : ℝ<VAR>f : ℝ → E<VAR>c d : ℝ<GOAL>c • ∫ (x : ℝ) in a..b, f (c * x + d) = ∫ (x : ℝ) in c * a + d..c * b + d, f x
<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>a b c : ℝ<VAR>f : ℝ → E<VAR>hc : c ≠ 0<VAR>d : ℝ<GOAL>∫ (x : ℝ) in a..b, f (d + c * x) = c⁻¹ • ∫ (x : ℝ) in d + c * a..d + c * b, f x
<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>CompleteSpace E<VAR>NormedSpace ℝ E<VAR>a b : ℝ<VAR>f : ℝ → E<VAR>c d : ℝ<GOAL>c • ∫ (x : ℝ) in a..b, f (d + c * x) = ∫ (x : ℝ) in d + c * a..d + c * b, f x
<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>a b c : ℝ<VAR>f : ℝ → E<VAR>hc : c ≠ 0<VAR>d : ℝ<GOAL>∫ (x : ℝ) in a..b, f (x / c + d) = c • ∫ (x : ℝ) in a / c + d..b / c + d, f x
<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>CompleteSpace E<VAR>NormedSpace ℝ E<VAR>a b : ℝ<VAR>f : ℝ → E<VAR>c d : ℝ<GOAL>c⁻¹ • ∫ (x : ℝ) in a..b, f (x / c + d) = ∫ (x : ℝ) in a / c + d..b / c + d, f x
<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>a b c : ℝ<VAR>f : ℝ → E<VAR>hc : c ≠ 0<VAR>d : ℝ<GOAL>∫ (x : ℝ) in a..b, f (d + x / c) = c • ∫ (x : ℝ) in d + a / c..d + b / c, f x
<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>CompleteSpace E<VAR>NormedSpace ℝ E<VAR>a b : ℝ<VAR>f : ℝ → E<VAR>c d : ℝ<GOAL>c⁻¹ • ∫ (x : ℝ) in a..b, f (d + x / c) = ∫ (x : ℝ) in d + a / c..d + b / c, f x
<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>a b c : ℝ<VAR>f : ℝ → E<VAR>hc : c ≠ 0<VAR>d : ℝ<GOAL>∫ (x : ℝ) in a..b, f (c * x - d) = c⁻¹ • ∫ (x : ℝ) in c * a - d..c * b - d, f x
<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>CompleteSpace E<VAR>NormedSpace ℝ E<VAR>a b : ℝ<VAR>f : ℝ → E<VAR>c d : ℝ<GOAL>c • ∫ (x : ℝ) in a..b, f (c * x - d) = ∫ (x : ℝ) in c * a - d..c * b - d, f x
<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>a b c : ℝ<VAR>f : ℝ → E<VAR>hc : c ≠ 0<VAR>d : ℝ<GOAL>∫ (x : ℝ) in a..b, f (d - c * x) = c⁻¹ • ∫ (x : ℝ) in d - c * b..d - c * a, f x
<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>CompleteSpace E<VAR>NormedSpace ℝ E<VAR>a b : ℝ<VAR>f : ℝ → E<VAR>c d : ℝ<GOAL>c • ∫ (x : ℝ) in a..b, f (d - c * x) = ∫ (x : ℝ) in d - c * b..d - c * a, f x
<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>a b c : ℝ<VAR>f : ℝ → E<VAR>hc : c ≠ 0<VAR>d : ℝ<GOAL>∫ (x : ℝ) in a..b, f (x / c - d) = c • ∫ (x : ℝ) in a / c - d..b / c - d, f x
<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>CompleteSpace E<VAR>NormedSpace ℝ E<VAR>a b : ℝ<VAR>f : ℝ → E<VAR>c d : ℝ<GOAL>c⁻¹ • ∫ (x : ℝ) in a..b, f (x / c - d) = ∫ (x : ℝ) in a / c - d..b / c - d, f x
<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>a b c : ℝ<VAR>f : ℝ → E<VAR>hc : c ≠ 0<VAR>d : ℝ<GOAL>∫ (x : ℝ) in a..b, f (d - x / c) = c • ∫ (x : ℝ) in d - b / c..d - a / c, f x
<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>CompleteSpace E<VAR>NormedSpace ℝ E<VAR>a b : ℝ<VAR>f : ℝ → E<VAR>c d : ℝ<GOAL>c⁻¹ • ∫ (x : ℝ) in a..b, f (d - x / c) = ∫ (x : ℝ) in d - b / c..d - a / c, f x
<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>a b : ℝ<VAR>f : ℝ → E<VAR>d : ℝ<GOAL>∫ (x : ℝ) in a..b, f (x - d) = ∫ (x : ℝ) in a - d..b - d, f x
<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>a b : ℝ<VAR>f : ℝ → E<VAR>d : ℝ<GOAL>∫ (x : ℝ) in a..b, f (d - x) = ∫ (x : ℝ) in d - b..d - a, f x
<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>a b : ℝ<VAR>f : ℝ → E<GOAL>∫ (x : ℝ) in a..b, f (-x) = ∫ (x : ℝ) in -b..-a, f x
<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>f g : ℝ → E<VAR>μ : MeasureTheory.Measure ℝ<VAR>a b : ℝ<VAR>h : Set.EqOn f g [[a, b]]<GOAL>∫ (x : ℝ) in a..b, f x ∂μ = ∫ (x : ℝ) in a..b, g x ∂μ
<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>a b c : ℝ<VAR>f : ℝ → E<VAR>μ : MeasureTheory.Measure ℝ<VAR>hab : IntervalIntegrable f μ a b<VAR>hbc : IntervalIntegrable f μ b c<GOAL>∫ (x : ℝ) in a..b, f x ∂μ + ∫ (x : ℝ) in b..c, f x ∂μ + ∫ (x : ℝ) in c..a, f x ∂μ = 0
<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>a b c : ℝ<VAR>f : ℝ → E<VAR>μ : MeasureTheory.Measure ℝ<VAR>hab : IntervalIntegrable f μ a b<VAR>hbc : IntervalIntegrable f μ b c<GOAL>∫ (x : ℝ) in a..b, f x ∂μ + ∫ (x : ℝ) in b..c, f x ∂μ = ∫ (x : ℝ) in a..c, f x ∂μ
<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>f : ℝ → E<VAR>μ : MeasureTheory.Measure ℝ<VAR>a : ℕ → ℝ<VAR>m n : ℕ<VAR>hmn : m ≤ n<VAR>hint : ∀ k ∈ Set.Ico m n, IntervalIntegrable f μ (a k) (a (k + 1))<GOAL>∑ k ∈ Finset.Ico m n, ∫ (x : ℝ) in a k..a (k + 1), f x ∂μ = ∫ (x : ℝ) in a m..a n, f x ∂μ
<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>f : ℝ → E<VAR>μ : MeasureTheory.Measure ℝ<VAR>a : ℕ → ℝ<VAR>n : ℕ<VAR>hint : ∀ k < n, IntervalIntegrable f μ (a k) (a (k + 1))<GOAL>∑ k ∈ Finset.range n, ∫ (x : ℝ) in a k..a (k + 1), f x ∂μ = ∫ (x : ℝ) in a 0 ..a n, f x ∂μ
<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>a b c : ℝ<VAR>f : ℝ → E<VAR>μ : MeasureTheory.Measure ℝ<VAR>hab : IntervalIntegrable f μ a b<VAR>hac : IntervalIntegrable f μ a c<GOAL>∫ (x : ℝ) in a..b, f x ∂μ - ∫ (x : ℝ) in a..c, f x ∂μ = ∫ (x : ℝ) in c..b, f x ∂μ
<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>a b c d : ℝ<VAR>f : ℝ → E<VAR>μ : MeasureTheory.Measure ℝ<VAR>hab : IntervalIntegrable f μ a b<VAR>hcd : IntervalIntegrable f μ c d<VAR>hac : IntervalIntegrable f μ a c<GOAL>∫ (x : ℝ) in a..b, f x ∂μ + ∫ (x : ℝ) in c..d, f x ∂μ = ∫ (x : ℝ) in a..d, f x ∂μ + ∫ (x : ℝ) in c..b, f x ∂μ
<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>a b c d : ℝ<VAR>f : ℝ → E<VAR>μ : MeasureTheory.Measure ℝ<VAR>hab : IntervalIntegrable f μ a b<VAR>hcd : IntervalIntegrable f μ c d<VAR>hac : IntervalIntegrable f μ a c<GOAL>∫ (x : ℝ) in a..b, f x ∂μ - ∫ (x : ℝ) in c..d, f x ∂μ = ∫ (x : ℝ) in a..c, f x ∂μ - ∫ (x : ℝ) in b..d, f x ∂μ
<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>a b c d : ℝ<VAR>f : ℝ → E<VAR>μ : MeasureTheory.Measure ℝ<VAR>hab : IntervalIntegrable f μ a b<VAR>hcd : IntervalIntegrable f μ c d<VAR>hac : IntervalIntegrable f μ a c<GOAL>∫ (x : ℝ) in a..b, f x ∂μ - ∫ (x : ℝ) in c..d, f x ∂μ = ∫ (x : ℝ) in d..b, f x ∂μ - ∫ (x : ℝ) in c..a, f x ∂μ
<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>a b : ℝ<VAR>f : ℝ → E<VAR>μ : MeasureTheory.Measure ℝ<VAR>ha : MeasureTheory.IntegrableOn f (Set.Iic a) μ<VAR>hb : MeasureTheory.IntegrableOn f (Set.Iic b) μ<GOAL>∫ (x : ℝ) in Set.Iic b, f x ∂μ - ∫ (x : ℝ) in Set.Iic a, f x ∂μ = ∫ (x : ℝ) in a..b, f x ∂μ
<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>b : ℝ<VAR>f : ℝ → E<VAR>μ : MeasureTheory.Measure ℝ<VAR>h_left : MeasureTheory.IntegrableOn f (Set.Iic b) μ<VAR>h_right : MeasureTheory.IntegrableOn f (Set.Ioi b) μ<GOAL>∫ (x : ℝ) in Set.Iic b, f x ∂μ + ∫ (x : ℝ) in Set.Ioi b, f x ∂μ = ∫ (x : ℝ), f x ∂μ
<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>b : ℝ<VAR>f : ℝ → E<VAR>μ : MeasureTheory.Measure ℝ<VAR>h_left : MeasureTheory.IntegrableOn f (Set.Iio b) μ<VAR>h_right : MeasureTheory.IntegrableOn f (Set.Ici b) μ<GOAL>∫ (x : ℝ) in Set.Iio b, f x ∂μ + ∫ (x : ℝ) in Set.Ici b, f x ∂μ = ∫ (x : ℝ), f x ∂μ
<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>CompleteSpace E<VAR>NormedSpace ℝ E<VAR>a b : ℝ<VAR>μ : MeasureTheory.Measure ℝ<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>c : E<GOAL>∫ (x : ℝ) in a..b, c ∂μ = ((μ (Set.Iic b)).toReal - (μ (Set.Iic a)).toReal) • c
<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>f : ℝ → E<VAR>μ : MeasureTheory.Measure ℝ<VAR>a b : ℝ<VAR>h : Function.support f ⊆ Set.Ioc a b<GOAL>∫ (x : ℝ) in a..b, f x ∂μ = ∫ (x : ℝ), f x ∂μ
<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>a b : ℝ<VAR>f g : ℝ → E<VAR>μ : MeasureTheory.Measure ℝ<VAR>h : ∀ᵐ (x : ℝ) ∂μ, x ∈ Set.Ioc a b → f x = g x<VAR>h' : ∀ᵐ (x : ℝ) ∂μ, x ∈ Set.Ioc b a → f x = g x<GOAL>∫ (x : ℝ) in a..b, f x ∂μ = ∫ (x : ℝ) in a..b, g x ∂μ
<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>a b : ℝ<VAR>f g : ℝ → E<VAR>μ : MeasureTheory.Measure ℝ<VAR>h : ∀ᵐ (x : ℝ) ∂μ, x ∈ Ι a b → f x = g x<GOAL>∫ (x : ℝ) in a..b, f x ∂μ = ∫ (x : ℝ) in a..b, g x ∂μ
<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>a b : ℝ<VAR>f : ℝ → E<VAR>μ : MeasureTheory.Measure ℝ<VAR>h : ∀ᵐ (x : ℝ) ∂μ, x ∈ Ι a b → f x = 0<GOAL>∫ (x : ℝ) in a..b, f x ∂μ = 0
<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>f : ℝ → E<VAR>μ : MeasureTheory.Measure ℝ<VAR>a₁ a₂ a₃ : ℝ<VAR>h : a₂ ∈ Set.Icc a₁ a₃<GOAL>∫ (x : ℝ) in a₁..a₃, {x | x ≤ a₂}.indicator f x ∂μ = ∫ (x : ℝ) in a₁..a₂, f x ∂μ
<VAR>f : ℝ → ℝ<VAR>a b : ℝ<VAR>μ : MeasureTheory.Measure ℝ<VAR>hab : a ≤ b<VAR>hf : 0 ≤ᵐ[μ.restrict (Set.Ioc a b)] f<VAR>hfi : IntervalIntegrable f μ a b<GOAL>∫ (x : ℝ) in a..b, f x ∂μ = 0 ↔ f =ᵐ[μ.restrict (Set.Ioc a b)] 0
<VAR>f : ℝ → ℝ<VAR>a b : ℝ<VAR>μ : MeasureTheory.Measure ℝ<VAR>hf : 0 ≤ᵐ[μ.restrict (Set.Ioc a b ∪ Set.Ioc b a)] f<VAR>hfi : IntervalIntegrable f μ a b<GOAL>∫ (x : ℝ) in a..b, f x ∂μ = 0 ↔ f =ᵐ[μ.restrict (Set.Ioc a b ∪ Set.Ioc b a)] 0
<VAR>f : ℝ → ℝ<VAR>a b : ℝ<VAR>μ : MeasureTheory.Measure ℝ<VAR>hf : 0 ≤ᵐ[μ.restrict (Ι a b)] f<VAR>hfi : IntervalIntegrable f μ a b<GOAL>0 < ∫ (x : ℝ) in a..b, f x ∂μ ↔ a < b ∧ 0 < μ (Function.support f ∩ Set.Ioc a b)
<VAR>f : ℝ → ℝ<VAR>a b : ℝ<VAR>μ : MeasureTheory.Measure ℝ<VAR>hf : 0 ≤ᵐ[μ] f<VAR>hfi : IntervalIntegrable f μ a b<GOAL>0 < ∫ (x : ℝ) in a..b, f x ∂μ ↔ a < b ∧ 0 < μ (Function.support f ∩ Set.Ioc a b)
<VAR>f : ℝ → ℝ<VAR>a b : ℝ<VAR>hfi : IntervalIntegrable f MeasureTheory.volume a b<VAR>hpos : ∀ x ∈ Set.Ioo a b, 0 < f x<VAR>hab : a < b<GOAL>0 < ∫ (x : ℝ) in a..b, f x
<VAR>f : ℝ → ℝ<VAR>a b : ℝ<VAR>hfi : IntervalIntegrable f MeasureTheory.volume a b<VAR>hpos : ∀ (x : ℝ), 0 < f x<VAR>hab : a < b<GOAL>0 < ∫ (x : ℝ) in a..b, f x
<VAR>f g : ℝ → ℝ<VAR>a b : ℝ<VAR>μ : MeasureTheory.Measure ℝ<VAR>hab : a ≤ b<VAR>hfi : IntervalIntegrable f μ a b<VAR>hgi : IntervalIntegrable g μ a b<VAR>hle : f ≤ᵐ[μ.restrict (Set.Ioc a b)] g<VAR>hlt : (μ.restrict (Set.Ioc a b)) {x | f x < g x} ≠ 0<GOAL>∫ (x : ℝ) in a..b, f x ∂μ < ∫ (x : ℝ) in a..b, g x ∂μ
<VAR>f g : ℝ → ℝ<VAR>a b : ℝ<VAR>hab : a < b<VAR>hfc : ContinuousOn f (Set.Icc a b)<VAR>hgc : ContinuousOn g (Set.Icc a b)<VAR>hle : ∀ x ∈ Set.Ioc a b, f x ≤ g x<VAR>hlt : ∃ c ∈ Set.Icc a b, f c < g c<GOAL>∫ (x : ℝ) in a..b, f x < ∫ (x : ℝ) in a..b, g x
<VAR>f : ℝ → ℝ<VAR>a b : ℝ<VAR>μ : MeasureTheory.Measure ℝ<VAR>hab : a ≤ b<VAR>hf : 0 ≤ᵐ[μ.restrict (Set.Icc a b)] f<GOAL>0 ≤ ∫ (u : ℝ) in a..b, f u ∂μ
<VAR>f : ℝ → ℝ<VAR>a b : ℝ<VAR>μ : MeasureTheory.Measure ℝ<VAR>hab : a ≤ b<VAR>hf : 0 ≤ᵐ[μ] f<GOAL>0 ≤ ∫ (u : ℝ) in a..b, f u ∂μ
<VAR>f : ℝ → ℝ<VAR>a b : ℝ<VAR>μ : MeasureTheory.Measure ℝ<VAR>hab : a ≤ b<VAR>hf : ∀ (u : ℝ), 0 ≤ f u<GOAL>0 ≤ ∫ (u : ℝ) in a..b, f u ∂μ
<VAR>f : ℝ → ℝ<VAR>a b : ℝ<VAR>μ : MeasureTheory.Measure ℝ<VAR>hab : a ≤ b<VAR>hf : ∀ u ∈ Set.Icc a b, 0 ≤ f u<GOAL>0 ≤ ∫ (u : ℝ) in a..b, f u ∂μ
<VAR>f : ℝ → ℝ<VAR>a b : ℝ<VAR>μ : MeasureTheory.Measure ℝ<VAR>hab : a ≤ b<GOAL>|∫ (x : ℝ) in a..b, f x ∂μ| ≤ ∫ (x : ℝ) in a..b, |f x| ∂μ
<VAR>f g : ℝ → ℝ<VAR>a b : ℝ<VAR>μ : MeasureTheory.Measure ℝ<VAR>hab : a ≤ b<VAR>hf : IntervalIntegrable f μ a b<VAR>hg : IntervalIntegrable g μ a b<VAR>h : f ≤ᵐ[μ.restrict (Set.Icc a b)] g<GOAL>∫ (u : ℝ) in a..b, f u ∂μ ≤ ∫ (u : ℝ) in a..b, g u ∂μ
<VAR>f g : ℝ → ℝ<VAR>a b : ℝ<VAR>μ : MeasureTheory.Measure ℝ<VAR>hab : a ≤ b<VAR>hf : IntervalIntegrable f μ a b<VAR>hg : IntervalIntegrable g μ a b<VAR>h : f ≤ᵐ[μ] g<GOAL>∫ (u : ℝ) in a..b, f u ∂μ ≤ ∫ (u : ℝ) in a..b, g u ∂μ
<VAR>f g : ℝ → ℝ<VAR>a b : ℝ<VAR>μ : MeasureTheory.Measure ℝ<VAR>hab : a ≤ b<VAR>hf : IntervalIntegrable f μ a b<VAR>hg : IntervalIntegrable g μ a b<VAR>h : ∀ x ∈ Set.Icc a b, f x ≤ g x<GOAL>∫ (u : ℝ) in a..b, f u ∂μ ≤ ∫ (u : ℝ) in a..b, g u ∂μ
<VAR>f g : ℝ → ℝ<VAR>a b : ℝ<VAR>μ : MeasureTheory.Measure ℝ<VAR>hab : a ≤ b<VAR>hf : IntervalIntegrable f μ a b<VAR>hg : IntervalIntegrable g μ a b<VAR>h : f ≤ g<GOAL>∫ (u : ℝ) in a..b, f u ∂μ ≤ ∫ (u : ℝ) in a..b, g u ∂μ
<VAR>f : ℝ → ℝ<VAR>a b : ℝ<VAR>μ : MeasureTheory.Measure ℝ<VAR>c d : ℝ<VAR>hca : c ≤ a<VAR>hab : a ≤ b<VAR>hbd : b ≤ d<VAR>hf : 0 ≤ᵐ[μ.restrict (Set.Ioc c d)] f<VAR>hfi : IntervalIntegrable f μ c d<GOAL>∫ (x : ℝ) in a..b, f x ∂μ ≤ ∫ (x : ℝ) in c..d, f x ∂μ
<VAR>f : ℝ → ℝ<VAR>a b : ℝ<VAR>μ : MeasureTheory.Measure ℝ<VAR>c d : ℝ<VAR>h : Ι a b ⊆ Ι c d<VAR>hf : 0 ≤ᵐ[μ.restrict (Ι c d)] f<VAR>hfi : IntervalIntegrable f μ c d<GOAL>|∫ (x : ℝ) in a..b, f x ∂μ| ≤ |∫ (x : ℝ) in c..d, f x ∂μ|
<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>μ : MeasureTheory.Measure ℝ<VAR>f : ℝ → E<VAR>hfi : MeasureTheory.Integrable f μ<VAR>y : ℝ<GOAL>HasSum (fun n => ∫ (x : ℝ) in y + ↑n..y + ↑n + 1, f x ∂μ) (∫ (x : ℝ), f x ∂μ)
<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>f : ℝ → E<VAR>hfi : MeasureTheory.Integrable f MeasureTheory.volume<GOAL>HasSum (fun n => ∫ (x : ℝ) in 0 ..1, f (x + ↑n)) (∫ (x : ℝ), f x)
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>SecondCountableTopology α<VAR>LinearOrder α<VAR>OrderTopology α<GOAL>borel α = MeasurableSpace.generateFrom (Set.range Set.Iio)
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>SecondCountableTopology α<VAR>LinearOrder α<VAR>OrderTopology α<GOAL>borel α = MeasurableSpace.generateFrom (Set.range Set.Ioi)
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>SecondCountableTopology α<VAR>LinearOrder α<VAR>OrderTopology α<GOAL>borel α = MeasurableSpace.generateFrom (Set.range Set.Iic)
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>SecondCountableTopology α<VAR>LinearOrder α<VAR>OrderTopology α<GOAL>borel α = MeasurableSpace.generateFrom (Set.range Set.Ici)