ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>M : Type u_1<VAR>α : Type u_3<VAR>E : Type u_4<VAR>MeasurableSpace M<VAR>MeasurableSpace α<VAR>NormedAddCommGroup E<VAR>μ : MeasureTheory.Measure α<VAR>p : ℝ≥0∞<VAR>VAdd M α<VAR>MeasureTheory.VAddInvariantMeasure M α μ<VAR>MeasurableVAdd M α<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>c : Mᵈᵃᵃ<VAR>a : E<GOAL>c +ᵥ (MeasureTheory.Lp.const p μ) a = (MeasureTheory.Lp.const p μ) a
<VAR>M : Type u_1<VAR>α : Type u_3<VAR>E : Type u_4<VAR>MeasurableSpace M<VAR>MeasurableSpace α<VAR>NormedAddCommGroup E<VAR>μ : MeasureTheory.Measure α<VAR>p : ℝ≥0∞<VAR>SMul M α<VAR>MeasureTheory.SMulInvariantMeasure M α μ<VAR>MeasurableSMul M α<VAR>c : M<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>hμs : μ s ≠ ⊤<VAR>b : E<GOAL>DomMulAct.mk c • MeasureTheory.indicatorConstLp p hs hμs b = MeasureTheory.indicatorConstLp p ⋯ ⋯ b
<VAR>M : Type u_1<VAR>α : Type u_3<VAR>E : Type u_4<VAR>MeasurableSpace M<VAR>MeasurableSpace α<VAR>NormedAddCommGroup E<VAR>μ : MeasureTheory.Measure α<VAR>p : ℝ≥0∞<VAR>VAdd M α<VAR>MeasureTheory.VAddInvariantMeasure M α μ<VAR>MeasurableVAdd M α<VAR>c : M<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>hμs : μ s ≠ ⊤<VAR>b : E<GOAL>DomAddAct.mk c +ᵥ MeasureTheory.indicatorConstLp p hs hμs b = MeasureTheory.indicatorConstLp p ⋯ ⋯ b
<VAR>M : Type u_1<VAR>α : Type u_3<VAR>E : Type u_4<VAR>MeasurableSpace M<VAR>MeasurableSpace α<VAR>NormedAddCommGroup E<VAR>μ : MeasureTheory.Measure α<VAR>p : ℝ≥0∞<VAR>VAdd M α<VAR>MeasureTheory.VAddInvariantMeasure M α μ<VAR>MeasurableVAdd M α<VAR>c : Mᵈᵃᵃ<VAR>f g : ↥(MeasureTheory.Lp E p μ)<GOAL>c +ᵥ (f + g) = c +ᵥ f + (c +ᵥ g)
<VAR>M : Type u_1<VAR>α : Type u_3<VAR>E : Type u_4<VAR>MeasurableSpace M<VAR>MeasurableSpace α<VAR>NormedAddCommGroup E<VAR>μ : MeasureTheory.Measure α<VAR>p : ℝ≥0∞<VAR>SMul M α<VAR>MeasureTheory.SMulInvariantMeasure M α μ<VAR>MeasurableSMul M α<VAR>c : Mᵈᵐᵃ<VAR>f g : ↥(MeasureTheory.Lp E p μ)<GOAL>c • (f + g) = c • f + c • g
<VAR>M : Type u_1<VAR>α : Type u_3<VAR>E : Type u_4<VAR>MeasurableSpace M<VAR>MeasurableSpace α<VAR>NormedAddCommGroup E<VAR>μ : MeasureTheory.Measure α<VAR>p : ℝ≥0∞<VAR>SMul M α<VAR>MeasureTheory.SMulInvariantMeasure M α μ<VAR>MeasurableSMul M α<VAR>c : Mᵈᵐᵃ<GOAL>c • 0 = 0
<VAR>M : Type u_1<VAR>α : Type u_3<VAR>E : Type u_4<VAR>MeasurableSpace M<VAR>MeasurableSpace α<VAR>NormedAddCommGroup E<VAR>μ : MeasureTheory.Measure α<VAR>p : ℝ≥0∞<VAR>VAdd M α<VAR>MeasureTheory.VAddInvariantMeasure M α μ<VAR>MeasurableVAdd M α<VAR>c : Mᵈᵃᵃ<GOAL>c +ᵥ 0 = 0
<VAR>M : Type u_1<VAR>α : Type u_3<VAR>E : Type u_4<VAR>MeasurableSpace M<VAR>MeasurableSpace α<VAR>NormedAddCommGroup E<VAR>μ : MeasureTheory.Measure α<VAR>p : ℝ≥0∞<VAR>VAdd M α<VAR>MeasureTheory.VAddInvariantMeasure M α μ<VAR>MeasurableVAdd M α<VAR>c : Mᵈᵃᵃ<VAR>f : ↥(MeasureTheory.Lp E p μ)<GOAL>c +ᵥ -f = -(c +ᵥ f)
<VAR>M : Type u_1<VAR>α : Type u_3<VAR>E : Type u_4<VAR>MeasurableSpace M<VAR>MeasurableSpace α<VAR>NormedAddCommGroup E<VAR>μ : MeasureTheory.Measure α<VAR>p : ℝ≥0∞<VAR>SMul M α<VAR>MeasureTheory.SMulInvariantMeasure M α μ<VAR>MeasurableSMul M α<VAR>c : Mᵈᵐᵃ<VAR>f : ↥(MeasureTheory.Lp E p μ)<GOAL>c • -f = -(c • f)
<VAR>M : Type u_1<VAR>α : Type u_3<VAR>E : Type u_4<VAR>MeasurableSpace M<VAR>MeasurableSpace α<VAR>NormedAddCommGroup E<VAR>μ : MeasureTheory.Measure α<VAR>p : ℝ≥0∞<VAR>VAdd M α<VAR>MeasureTheory.VAddInvariantMeasure M α μ<VAR>MeasurableVAdd M α<VAR>c : Mᵈᵃᵃ<VAR>f g : ↥(MeasureTheory.Lp E p μ)<GOAL>c +ᵥ (f - g) = c +ᵥ f - (c +ᵥ g)
<VAR>M : Type u_1<VAR>α : Type u_3<VAR>E : Type u_4<VAR>MeasurableSpace M<VAR>MeasurableSpace α<VAR>NormedAddCommGroup E<VAR>μ : MeasureTheory.Measure α<VAR>p : ℝ≥0∞<VAR>SMul M α<VAR>MeasureTheory.SMulInvariantMeasure M α μ<VAR>MeasurableSMul M α<VAR>c : Mᵈᵐᵃ<VAR>f g : ↥(MeasureTheory.Lp E p μ)<GOAL>c • (f - g) = c • f - c • g
<VAR>M : Type u_1<VAR>α : Type u_3<VAR>E : Type u_4<VAR>MeasurableSpace M<VAR>MeasurableSpace α<VAR>NormedAddCommGroup E<VAR>μ : MeasureTheory.Measure α<VAR>p : ℝ≥0∞<VAR>VAdd M α<VAR>MeasureTheory.VAddInvariantMeasure M α μ<VAR>MeasurableVAdd M α<VAR>c : Mᵈᵃᵃ<VAR>f : ↥(MeasureTheory.Lp E p μ)<GOAL>‖c +ᵥ f‖ = ‖f‖
<VAR>M : Type u_1<VAR>α : Type u_3<VAR>E : Type u_4<VAR>MeasurableSpace M<VAR>MeasurableSpace α<VAR>NormedAddCommGroup E<VAR>μ : MeasureTheory.Measure α<VAR>p : ℝ≥0∞<VAR>SMul M α<VAR>MeasureTheory.SMulInvariantMeasure M α μ<VAR>MeasurableSMul M α<VAR>c : Mᵈᵐᵃ<VAR>f : ↥(MeasureTheory.Lp E p μ)<GOAL>‖c • f‖ = ‖f‖
<VAR>M : Type u_1<VAR>α : Type u_3<VAR>E : Type u_4<VAR>MeasurableSpace M<VAR>MeasurableSpace α<VAR>NormedAddCommGroup E<VAR>μ : MeasureTheory.Measure α<VAR>p : ℝ≥0∞<VAR>SMul M α<VAR>MeasureTheory.SMulInvariantMeasure M α μ<VAR>MeasurableSMul M α<VAR>c : Mᵈᵐᵃ<VAR>f : ↥(MeasureTheory.Lp E p μ)<GOAL>‖c • f‖₊ = ‖f‖₊
<VAR>M : Type u_1<VAR>α : Type u_3<VAR>E : Type u_4<VAR>MeasurableSpace M<VAR>MeasurableSpace α<VAR>NormedAddCommGroup E<VAR>μ : MeasureTheory.Measure α<VAR>p : ℝ≥0∞<VAR>VAdd M α<VAR>MeasureTheory.VAddInvariantMeasure M α μ<VAR>MeasurableVAdd M α<VAR>c : Mᵈᵃᵃ<VAR>f : ↥(MeasureTheory.Lp E p μ)<GOAL>‖c +ᵥ f‖₊ = ‖f‖₊
<VAR>M : Type u_1<VAR>α : Type u_3<VAR>E : Type u_4<VAR>MeasurableSpace M<VAR>MeasurableSpace α<VAR>NormedAddCommGroup E<VAR>μ : MeasureTheory.Measure α<VAR>p : ℝ≥0∞<VAR>SMul M α<VAR>MeasureTheory.SMulInvariantMeasure M α μ<VAR>MeasurableSMul M α<VAR>c : Mᵈᵐᵃ<VAR>f g : ↥(MeasureTheory.Lp E p μ)<GOAL>dist (c • f) (c • g) = dist f g
<VAR>M : Type u_1<VAR>α : Type u_3<VAR>E : Type u_4<VAR>MeasurableSpace M<VAR>MeasurableSpace α<VAR>NormedAddCommGroup E<VAR>μ : MeasureTheory.Measure α<VAR>p : ℝ≥0∞<VAR>VAdd M α<VAR>MeasureTheory.VAddInvariantMeasure M α μ<VAR>MeasurableVAdd M α<VAR>c : Mᵈᵃᵃ<VAR>f g : ↥(MeasureTheory.Lp E p μ)<GOAL>dist (c +ᵥ f) (c +ᵥ g) = dist f g
<VAR>M : Type u_1<VAR>α : Type u_3<VAR>E : Type u_4<VAR>MeasurableSpace M<VAR>MeasurableSpace α<VAR>NormedAddCommGroup E<VAR>μ : MeasureTheory.Measure α<VAR>p : ℝ≥0∞<VAR>VAdd M α<VAR>MeasureTheory.VAddInvariantMeasure M α μ<VAR>MeasurableVAdd M α<VAR>c : Mᵈᵃᵃ<VAR>f g : ↥(MeasureTheory.Lp E p μ)<GOAL>edist (c +ᵥ f) (c +ᵥ g) = edist f g
<VAR>M : Type u_1<VAR>α : Type u_3<VAR>E : Type u_4<VAR>MeasurableSpace M<VAR>MeasurableSpace α<VAR>NormedAddCommGroup E<VAR>μ : MeasureTheory.Measure α<VAR>p : ℝ≥0∞<VAR>SMul M α<VAR>MeasureTheory.SMulInvariantMeasure M α μ<VAR>MeasurableSMul M α<VAR>c : Mᵈᵐᵃ<VAR>f g : ↥(MeasureTheory.Lp E p μ)<GOAL>edist (c • f) (c • g) = edist f g
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>PseudoEMetricSpace α<VAR>OpensMeasurableSpace α<VAR>e : ℕ → α<GOAL>MeasureTheory.SimpleFunc.nearestPtInd e 0 = MeasureTheory.SimpleFunc.const α 0
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>PseudoEMetricSpace α<VAR>OpensMeasurableSpace α<VAR>e : ℕ → α<GOAL>MeasureTheory.SimpleFunc.nearestPt e 0 = MeasureTheory.SimpleFunc.const α (e 0)
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>PseudoEMetricSpace α<VAR>OpensMeasurableSpace α<VAR>e : ℕ → α<VAR>N : ℕ<VAR>x : α<GOAL>↑(MeasureTheory.SimpleFunc.nearestPtInd e (N + 1)) x = if ∀ k ≤ N, edist (e (N + 1)) x < edist (e k) x then N + 1 else ↑(MeasureTheory.SimpleFunc.nearestPtInd e N) x
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>PseudoEMetricSpace α<VAR>OpensMeasurableSpace α<VAR>e : ℕ → α<VAR>N : ℕ<VAR>x : α<GOAL>↑(MeasureTheory.SimpleFunc.nearestPtInd e N) x ≤ N
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>PseudoEMetricSpace α<VAR>OpensMeasurableSpace α<VAR>e : ℕ → α<VAR>x : α<VAR>k N : ℕ<VAR>hk : k ≤ N<GOAL>edist (↑(MeasureTheory.SimpleFunc.nearestPt e N) x) x ≤ edist (e k) x
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>PseudoEMetricSpace α<VAR>OpensMeasurableSpace α<VAR>e : ℕ → α<VAR>x : α<VAR>hx : x ∈ closure (Set.range e)<GOAL>Filter.Tendsto (fun N => ↑(MeasureTheory.SimpleFunc.nearestPt e N) x) Filter.atTop (𝓝 x)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>MeasurableSpace α<VAR>PseudoEMetricSpace α<VAR>OpensMeasurableSpace α<VAR>MeasurableSpace β<VAR>f : β → α<VAR>hf : Measurable f<VAR>s : Set α<VAR>y₀ : α<VAR>h₀ : y₀ ∈ s<VAR>TopologicalSpace.SeparableSpace ↑s<VAR>x : β<GOAL>↑(MeasureTheory.SimpleFunc.approxOn f hf s y₀ h₀ 0) x = y₀
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>MeasurableSpace α<VAR>PseudoEMetricSpace α<VAR>OpensMeasurableSpace α<VAR>MeasurableSpace β<VAR>f : β → α<VAR>hf : Measurable f<VAR>s : Set α<VAR>y₀ : α<VAR>h₀ : y₀ ∈ s<VAR>TopologicalSpace.SeparableSpace ↑s<VAR>n : ℕ<VAR>x : β<GOAL>↑(MeasureTheory.SimpleFunc.approxOn f hf s y₀ h₀ n) x ∈ s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>MeasurableSpace α<VAR>PseudoEMetricSpace α<VAR>OpensMeasurableSpace α<VAR>MeasurableSpace β<VAR>γ : Type u_7<VAR>MeasurableSpace γ<VAR>f : β → α<VAR>hf : Measurable f<VAR>g : γ → β<VAR>hg : Measurable g<VAR>s : Set α<VAR>y₀ : α<VAR>h₀ : y₀ ∈ s<VAR>TopologicalSpace.SeparableSpace ↑s<VAR>n : ℕ<GOAL>MeasureTheory.SimpleFunc.approxOn (f ∘ g) ⋯ s y₀ h₀ n = (MeasureTheory.SimpleFunc.approxOn f hf s y₀ h₀ n).comp g hg
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>MeasurableSpace α<VAR>PseudoEMetricSpace α<VAR>OpensMeasurableSpace α<VAR>MeasurableSpace β<VAR>f : β → α<VAR>hf : Measurable f<VAR>s : Set α<VAR>y₀ : α<VAR>h₀ : y₀ ∈ s<VAR>TopologicalSpace.SeparableSpace ↑s<VAR>x : β<VAR>hx : f x ∈ closure s<GOAL>Filter.Tendsto (fun n => ↑(MeasureTheory.SimpleFunc.approxOn f hf s y₀ h₀ n) x) Filter.atTop (𝓝 (f x))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>MeasurableSpace α<VAR>PseudoEMetricSpace α<VAR>OpensMeasurableSpace α<VAR>MeasurableSpace β<VAR>f : β → α<VAR>hf : Measurable f<VAR>s : Set α<VAR>y₀ : α<VAR>h₀ : y₀ ∈ s<VAR>TopologicalSpace.SeparableSpace ↑s<VAR>x : β<VAR>m n : ℕ<VAR>h : m ≤ n<GOAL>edist (↑(MeasureTheory.SimpleFunc.approxOn f hf s y₀ h₀ n) x) (f x) ≤ edist (↑(MeasureTheory.SimpleFunc.approxOn f hf s y₀ h₀ m) x) (f x)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>MeasurableSpace α<VAR>PseudoEMetricSpace α<VAR>OpensMeasurableSpace α<VAR>MeasurableSpace β<VAR>f : β → α<VAR>hf : Measurable f<VAR>s : Set α<VAR>y₀ : α<VAR>h₀ : y₀ ∈ s<VAR>TopologicalSpace.SeparableSpace ↑s<VAR>x : β<VAR>n : ℕ<GOAL>edist (↑(MeasureTheory.SimpleFunc.approxOn f hf s y₀ h₀ n) x) (f x) ≤ edist y₀ (f x)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>MeasurableSpace α<VAR>PseudoEMetricSpace α<VAR>OpensMeasurableSpace α<VAR>MeasurableSpace β<VAR>f : β → α<VAR>hf : Measurable f<VAR>s : Set α<VAR>y₀ : α<VAR>h₀ : y₀ ∈ s<VAR>TopologicalSpace.SeparableSpace ↑s<VAR>x : β<VAR>n : ℕ<GOAL>edist y₀ (↑(MeasureTheory.SimpleFunc.approxOn f hf s y₀ h₀ n) x) ≤ edist y₀ (f x) + edist y₀ (f x)
<VAR>X : Type u_7<VAR>Y : Type u_8<VAR>α : Type u_9<VAR>Zero α<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>MeasurableSpace X<VAR>MeasurableSpace Y<VAR>OpensMeasurableSpace X<VAR>OpensMeasurableSpace Y<VAR>PseudoMetricSpace α<VAR>f : X × Y → α<VAR>hf : Continuous f<VAR>h'f : HasCompactSupport f<VAR>ε : ℝ<VAR>hε : 0 < ε<GOAL>∃ g, ∀ (x : X × Y), dist (f x) (↑g x) < ε
<VAR>X : Type u_7<VAR>Y : Type u_8<VAR>α : Type u_9<VAR>Zero α<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>MeasurableSpace X<VAR>MeasurableSpace Y<VAR>OpensMeasurableSpace X<VAR>OpensMeasurableSpace Y<VAR>TopologicalSpace α<VAR>TopologicalSpace.PseudoMetrizableSpace α<VAR>MeasurableSpace α<VAR>BorelSpace α<VAR>f : X × Y → α<VAR>hf : Continuous f<VAR>h'f : HasCompactSupport f<GOAL>Measurable f
<VAR>α : Type u_1<VAR>G : Type u_2<VAR>p : ℝ≥0∞<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup G<VAR>f : α → G<VAR>hf : MeasureTheory.Memℒp f p μ<VAR>hf_meas : MeasureTheory.StronglyMeasurable f<VAR>hp_ne_zero : p ≠ 0<VAR>hp_ne_top : p ≠ ⊤<GOAL>MeasureTheory.FinStronglyMeasurable f μ
<VAR>α : Type u_1<VAR>G : Type u_2<VAR>p : ℝ≥0∞<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup G<VAR>f : α → G<VAR>hf : MeasureTheory.Memℒp f p μ<VAR>hp_ne_zero : p ≠ 0<VAR>hp_ne_top : p ≠ ⊤<GOAL>MeasureTheory.AEFinStronglyMeasurable f μ
<VAR>α : Type u_1<VAR>G : Type u_2<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup G<VAR>f : α → G<VAR>hf : MeasureTheory.Integrable f μ<GOAL>MeasureTheory.AEFinStronglyMeasurable f μ
<VAR>α : Type u_1<VAR>G : Type u_2<VAR>p : ℝ≥0∞<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup G<VAR>f : ↥(MeasureTheory.Lp G p μ)<VAR>hp_ne_zero : p ≠ 0<VAR>hp_ne_top : p ≠ ⊤<GOAL>MeasureTheory.FinStronglyMeasurable (↑↑f) μ
<VAR>a : outParam ℝ<VAR>outer : Filter ℝ<VAR>inner : outParam (Filter ℝ)<VAR>self : intervalIntegral.FTCFilter a outer inner<GOAL>Filter.IsMeasurablyGenerated inner
<VAR>a : outParam ℝ<VAR>outer : Filter ℝ<VAR>inner : outParam (Filter ℝ)<VAR>self : intervalIntegral.FTCFilter a outer inner<GOAL>inner ≤ 𝓝 a
<VAR>a : outParam ℝ<VAR>outer : Filter ℝ<VAR>inner : outParam (Filter ℝ)<VAR>self : intervalIntegral.FTCFilter a outer inner<GOAL>pure a ≤ outer
<VAR>a : ℝ<VAR>l : Filter ℝ<VAR>l' : Filter ℝ<VAR>h : intervalIntegral.FTCFilter a l l'<VAR>μ : MeasureTheory.Measure ℝ<VAR>MeasureTheory.IsLocallyFiniteMeasure μ<GOAL>μ.FiniteAtFilter l'
<VAR>ι : Type u_1<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>f : ℝ → E<VAR>c : E<VAR>l l' : Filter ℝ<VAR>lt : Filter ι<VAR>μ : MeasureTheory.Measure ℝ<VAR>u v : ι → ℝ<VAR>l'.IsMeasurablyGenerated<VAR>Filter.TendstoIxxClass Set.Ioc l l'<VAR>hfm : StronglyMeasurableAtFilter f l' μ<VAR>hf : Filter.Tendsto f (l' ⊓ MeasureTheory.ae μ) (𝓝 c)<VAR>hl : μ.FiniteAtFilter l'<VAR>hu : Filter.Tendsto u lt l<VAR>hv : Filter.Tendsto v lt l<GOAL>(fun t => ∫ (x : ℝ) in u t..v t, f x ∂μ - ∫ (x : ℝ) in u t..v t, c ∂μ) =o[lt] fun t => ∫ (x : ℝ) in u t..v t, 1 ∂μ
<VAR>ι : Type u_1<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>f : ℝ → E<VAR>c : E<VAR>l l' : Filter ℝ<VAR>lt : Filter ι<VAR>μ : MeasureTheory.Measure ℝ<VAR>u v : ι → ℝ<VAR>CompleteSpace E<VAR>l'.IsMeasurablyGenerated<VAR>Filter.TendstoIxxClass Set.Ioc l l'<VAR>hfm : StronglyMeasurableAtFilter f l' μ<VAR>hf : Filter.Tendsto f (l' ⊓ MeasureTheory.ae μ) (𝓝 c)<VAR>hl : μ.FiniteAtFilter l'<VAR>hu : Filter.Tendsto u lt l<VAR>hv : Filter.Tendsto v lt l<VAR>huv : u ≤ᶠ[lt] v<GOAL>(fun t => ∫ (x : ℝ) in u t..v t, f x ∂μ - (μ (Set.Ioc (u t) (v t))).toReal • c) =o[lt] fun t => (μ (Set.Ioc (u t) (v t))).toReal
<VAR>ι : Type u_1<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>f : ℝ → E<VAR>c : E<VAR>l l' : Filter ℝ<VAR>lt : Filter ι<VAR>μ : MeasureTheory.Measure ℝ<VAR>u v : ι → ℝ<VAR>CompleteSpace E<VAR>l'.IsMeasurablyGenerated<VAR>Filter.TendstoIxxClass Set.Ioc l l'<VAR>hfm : StronglyMeasurableAtFilter f l' μ<VAR>hf : Filter.Tendsto f (l' ⊓ MeasureTheory.ae μ) (𝓝 c)<VAR>hl : μ.FiniteAtFilter l'<VAR>hu : Filter.Tendsto u lt l<VAR>hv : Filter.Tendsto v lt l<VAR>huv : v ≤ᶠ[lt] u<GOAL>(fun t => ∫ (x : ℝ) in u t..v t, f x ∂μ + (μ (Set.Ioc (v t) (u t))).toReal • c) =o[lt] fun t => (μ (Set.Ioc (v t) (u t))).toReal
<VAR>ι : Type u_1<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>f : ℝ → E<VAR>a : ℝ<VAR>c : E<VAR>l l' : Filter ℝ<VAR>lt : Filter ι<VAR>μ : MeasureTheory.Measure ℝ<VAR>u v : ι → ℝ<VAR>MeasureTheory.IsLocallyFiniteMeasure μ<VAR>intervalIntegral.FTCFilter a l l'<VAR>hfm : StronglyMeasurableAtFilter f l' μ<VAR>hf : Filter.Tendsto f (l' ⊓ MeasureTheory.ae μ) (𝓝 c)<VAR>hu : Filter.Tendsto u lt l<VAR>hv : Filter.Tendsto v lt l<GOAL>(fun t => ∫ (x : ℝ) in u t..v t, f x ∂μ - ∫ (x : ℝ) in u t..v t, c ∂μ) =o[lt] fun t => ∫ (x : ℝ) in u t..v t, 1 ∂μ
<VAR>ι : Type u_1<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>f : ℝ → E<VAR>a : ℝ<VAR>c : E<VAR>l l' : Filter ℝ<VAR>lt : Filter ι<VAR>μ : MeasureTheory.Measure ℝ<VAR>u v : ι → ℝ<VAR>CompleteSpace E<VAR>MeasureTheory.IsLocallyFiniteMeasure μ<VAR>intervalIntegral.FTCFilter a l l'<VAR>hfm : StronglyMeasurableAtFilter f l' μ<VAR>hf : Filter.Tendsto f (l' ⊓ MeasureTheory.ae μ) (𝓝 c)<VAR>hu : Filter.Tendsto u lt l<VAR>hv : Filter.Tendsto v lt l<VAR>huv : u ≤ᶠ[lt] v<GOAL>(fun t => ∫ (x : ℝ) in u t..v t, f x ∂μ - (μ (Set.Ioc (u t) (v t))).toReal • c) =o[lt] fun t => (μ (Set.Ioc (u t) (v t))).toReal
<VAR>ι : Type u_1<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>f : ℝ → E<VAR>a : ℝ<VAR>c : E<VAR>l l' : Filter ℝ<VAR>lt : Filter ι<VAR>μ : MeasureTheory.Measure ℝ<VAR>u v : ι → ℝ<VAR>CompleteSpace E<VAR>MeasureTheory.IsLocallyFiniteMeasure μ<VAR>intervalIntegral.FTCFilter a l l'<VAR>hfm : StronglyMeasurableAtFilter f l' μ<VAR>hf : Filter.Tendsto f (l' ⊓ MeasureTheory.ae μ) (𝓝 c)<VAR>hu : Filter.Tendsto u lt l<VAR>hv : Filter.Tendsto v lt l<VAR>huv : v ≤ᶠ[lt] u<GOAL>(fun t => ∫ (x : ℝ) in u t..v t, f x ∂μ + (μ (Set.Ioc (v t) (u t))).toReal • c) =o[lt] fun t => (μ (Set.Ioc (v t) (u t))).toReal
<VAR>ι : Type u_1<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>f : ℝ → E<VAR>a b : ℝ<VAR>ca cb : E<VAR>la la' lb lb' : Filter ℝ<VAR>lt : Filter ι<VAR>μ : MeasureTheory.Measure ℝ<VAR>ua va ub vb : ι → ℝ<VAR>intervalIntegral.FTCFilter a la la'<VAR>intervalIntegral.FTCFilter b lb lb'<VAR>MeasureTheory.IsLocallyFiniteMeasure μ<VAR>hab : IntervalIntegrable f μ a b<VAR>hmeas_a : StronglyMeasurableAtFilter f la' μ<VAR>hmeas_b : StronglyMeasurableAtFilter f lb' μ<VAR>ha_lim : Filter.Tendsto f (la' ⊓ MeasureTheory.ae μ) (𝓝 ca)<VAR>hb_lim : Filter.Tendsto f (lb' ⊓ MeasureTheory.ae μ) (𝓝 cb)<VAR>hua : Filter.Tendsto ua lt la<VAR>hva : Filter.Tendsto va lt la<VAR>hub : Filter.Tendsto ub lt lb<VAR>hvb : Filter.Tendsto vb lt lb<GOAL>(fun t => ∫ (x : ℝ) in va t..vb t, f x ∂μ - ∫ (x : ℝ) in ua t..ub t, f x ∂μ - (∫ (x : ℝ) in ub t..vb t, cb ∂μ - ∫ (x : ℝ) in ua t..va t, ca ∂μ)) =o[lt] fun t => ‖∫ (x : ℝ) in ua t..va t, 1 ∂μ‖ + ‖∫ (x : ℝ) in ub t..vb t, 1 ∂μ‖
<VAR>ι : Type u_1<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>f : ℝ → E<VAR>a b : ℝ<VAR>c : E<VAR>lb lb' : Filter ℝ<VAR>lt : Filter ι<VAR>μ : MeasureTheory.Measure ℝ<VAR>u v : ι → ℝ<VAR>intervalIntegral.FTCFilter b lb lb'<VAR>MeasureTheory.IsLocallyFiniteMeasure μ<VAR>hab : IntervalIntegrable f μ a b<VAR>hmeas : StronglyMeasurableAtFilter f lb' μ<VAR>hf : Filter.Tendsto f (lb' ⊓ MeasureTheory.ae μ) (𝓝 c)<VAR>hu : Filter.Tendsto u lt lb<VAR>hv : Filter.Tendsto v lt lb<GOAL>(fun t => ∫ (x : ℝ) in a..v t, f x ∂μ - ∫ (x : ℝ) in a..u t, f x ∂μ - ∫ (x : ℝ) in u t..v t, c ∂μ) =o[lt] fun t => ∫ (x : ℝ) in u t..v t, 1 ∂μ
<VAR>ι : Type u_1<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>f : ℝ → E<VAR>a b : ℝ<VAR>c : E<VAR>la la' : Filter ℝ<VAR>lt : Filter ι<VAR>μ : MeasureTheory.Measure ℝ<VAR>u v : ι → ℝ<VAR>intervalIntegral.FTCFilter a la la'<VAR>MeasureTheory.IsLocallyFiniteMeasure μ<VAR>hab : IntervalIntegrable f μ a b<VAR>hmeas : StronglyMeasurableAtFilter f la' μ<VAR>hf : Filter.Tendsto f (la' ⊓ MeasureTheory.ae μ) (𝓝 c)<VAR>hu : Filter.Tendsto u lt la<VAR>hv : Filter.Tendsto v lt la<GOAL>(fun t => ∫ (x : ℝ) in v t..b, f x ∂μ - ∫ (x : ℝ) in u t..b, f x ∂μ + ∫ (x : ℝ) in u t..v t, c ∂μ) =o[lt] fun t => ∫ (x : ℝ) in u t..v t, 1 ∂μ
<VAR>ι : Type u_1<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>CompleteSpace E<VAR>f : ℝ → E<VAR>c : E<VAR>l l' : Filter ℝ<VAR>lt : Filter ι<VAR>a : ℝ<VAR>intervalIntegral.FTCFilter a l l'<VAR>hfm : StronglyMeasurableAtFilter f l' MeasureTheory.volume<VAR>hf : Filter.Tendsto f (l' ⊓ MeasureTheory.ae MeasureTheory.volume) (𝓝 c)<VAR>u v : ι → ℝ<VAR>hu : Filter.Tendsto u lt l<VAR>hv : Filter.Tendsto v lt l<GOAL>(fun t => (∫ (x : ℝ) in u t..v t, f x) - (v t - u t) • c) =o[lt] (v - u)
<VAR>ι : Type u_1<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>CompleteSpace E<VAR>f : ℝ → E<VAR>ca cb : E<VAR>la la' lb lb' : Filter ℝ<VAR>lt : Filter ι<VAR>a b : ℝ<VAR>ua ub va vb : ι → ℝ<VAR>intervalIntegral.FTCFilter a la la'<VAR>intervalIntegral.FTCFilter b lb lb'<VAR>hab : IntervalIntegrable f MeasureTheory.volume a b<VAR>hmeas_a : StronglyMeasurableAtFilter f la' MeasureTheory.volume<VAR>hmeas_b : StronglyMeasurableAtFilter f lb' MeasureTheory.volume<VAR>ha_lim : Filter.Tendsto f (la' ⊓ MeasureTheory.ae MeasureTheory.volume) (𝓝 ca)<VAR>hb_lim : Filter.Tendsto f (lb' ⊓ MeasureTheory.ae MeasureTheory.volume) (𝓝 cb)<VAR>hua : Filter.Tendsto ua lt la<VAR>hva : Filter.Tendsto va lt la<VAR>hub : Filter.Tendsto ub lt lb<VAR>hvb : Filter.Tendsto vb lt lb<GOAL>(fun t => ((∫ (x : ℝ) in va t..vb t, f x) - ∫ (x : ℝ) in ua t..ub t, f x) - ((vb t - ub t) • cb - (va t - ua t) • ca)) =o[lt] fun t => ‖va t - ua t‖ + ‖vb t - ub t‖
<VAR>ι : Type u_1<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>CompleteSpace E<VAR>f : ℝ → E<VAR>c : E<VAR>lb lb' : Filter ℝ<VAR>lt : Filter ι<VAR>a b : ℝ<VAR>u v : ι → ℝ<VAR>intervalIntegral.FTCFilter b lb lb'<VAR>hab : IntervalIntegrable f MeasureTheory.volume a b<VAR>hmeas : StronglyMeasurableAtFilter f lb' MeasureTheory.volume<VAR>hf : Filter.Tendsto f (lb' ⊓ MeasureTheory.ae MeasureTheory.volume) (𝓝 c)<VAR>hu : Filter.Tendsto u lt lb<VAR>hv : Filter.Tendsto v lt lb<GOAL>(fun t => ((∫ (x : ℝ) in a..v t, f x) - ∫ (x : ℝ) in a..u t, f x) - (v t - u t) • c) =o[lt] (v - u)
<VAR>ι : Type u_1<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>CompleteSpace E<VAR>f : ℝ → E<VAR>c : E<VAR>la la' : Filter ℝ<VAR>lt : Filter ι<VAR>a b : ℝ<VAR>u v : ι → ℝ<VAR>intervalIntegral.FTCFilter a la la'<VAR>hab : IntervalIntegrable f MeasureTheory.volume a b<VAR>hmeas : StronglyMeasurableAtFilter f la' MeasureTheory.volume<VAR>hf : Filter.Tendsto f (la' ⊓ MeasureTheory.ae MeasureTheory.volume) (𝓝 c)<VAR>hu : Filter.Tendsto u lt la<VAR>hv : Filter.Tendsto v lt la<GOAL>(fun t => ((∫ (x : ℝ) in v t..b, f x) - ∫ (x : ℝ) in u t..b, f x) + (v t - u t) • c) =o[lt] (v - u)
<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>CompleteSpace E<VAR>f : ℝ → E<VAR>ca cb : E<VAR>a b : ℝ<VAR>hf : IntervalIntegrable f MeasureTheory.volume a b<VAR>hmeas_a : StronglyMeasurableAtFilter f (𝓝 a) MeasureTheory.volume<VAR>hmeas_b : StronglyMeasurableAtFilter f (𝓝 b) MeasureTheory.volume<VAR>ha : Filter.Tendsto f (𝓝 a ⊓ MeasureTheory.ae MeasureTheory.volume) (𝓝 ca)<VAR>hb : Filter.Tendsto f (𝓝 b ⊓ MeasureTheory.ae MeasureTheory.volume) (𝓝 cb)<GOAL>HasStrictFDerivAt (fun p => ∫ (x : ℝ) in p.1 ..p.2, f x) ((ContinuousLinearMap.snd ℝ ℝ ℝ).smulRight cb - (ContinuousLinearMap.fst ℝ ℝ ℝ).smulRight ca) (a, b)
<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>CompleteSpace E<VAR>f : ℝ → E<VAR>a b : ℝ<VAR>hf : IntervalIntegrable f MeasureTheory.volume a b<VAR>hmeas_a : StronglyMeasurableAtFilter f (𝓝 a) MeasureTheory.volume<VAR>hmeas_b : StronglyMeasurableAtFilter f (𝓝 b) MeasureTheory.volume<VAR>ha : ContinuousAt f a<VAR>hb : ContinuousAt f b<GOAL>HasStrictFDerivAt (fun p => ∫ (x : ℝ) in p.1 ..p.2, f x) ((ContinuousLinearMap.snd ℝ ℝ ℝ).smulRight (f b) - (ContinuousLinearMap.fst ℝ ℝ ℝ).smulRight (f a)) (a, b)
<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>CompleteSpace E<VAR>f : ℝ → E<VAR>c : E<VAR>a b : ℝ<VAR>hf : IntervalIntegrable f MeasureTheory.volume a b<VAR>hmeas : StronglyMeasurableAtFilter f (𝓝 b) MeasureTheory.volume<VAR>hb : Filter.Tendsto f (𝓝 b ⊓ MeasureTheory.ae MeasureTheory.volume) (𝓝 c)<GOAL>HasStrictDerivAt (fun u => ∫ (x : ℝ) in a..u, f x) c b
<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>CompleteSpace E<VAR>f : ℝ → E<VAR>a b : ℝ<VAR>hf : IntervalIntegrable f MeasureTheory.volume a b<VAR>hmeas : StronglyMeasurableAtFilter f (𝓝 b) MeasureTheory.volume<VAR>hb : ContinuousAt f b<GOAL>HasStrictDerivAt (fun u => ∫ (x : ℝ) in a..u, f x) (f b) b
<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>CompleteSpace E<VAR>f : ℝ → E<VAR>c : E<VAR>a b : ℝ<VAR>hf : IntervalIntegrable f MeasureTheory.volume a b<VAR>hmeas : StronglyMeasurableAtFilter f (𝓝 a) MeasureTheory.volume<VAR>ha : Filter.Tendsto f (𝓝 a ⊓ MeasureTheory.ae MeasureTheory.volume) (𝓝 c)<GOAL>HasStrictDerivAt (fun u => ∫ (x : ℝ) in u..b, f x) (-c) a
<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>CompleteSpace E<VAR>f : ℝ → E<VAR>a b : ℝ<VAR>hf : IntervalIntegrable f MeasureTheory.volume a b<VAR>hmeas : StronglyMeasurableAtFilter f (𝓝 a) MeasureTheory.volume<VAR>ha : ContinuousAt f a<GOAL>HasStrictDerivAt (fun u => ∫ (x : ℝ) in u..b, f x) (-f a) a
<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>CompleteSpace E<VAR>f : ℝ → E<VAR>hf : Continuous f<VAR>a b : ℝ<GOAL>HasStrictDerivAt (fun u => ∫ (x : ℝ) in a..u, f x) (f b) b
<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>CompleteSpace E<VAR>f : ℝ → E<VAR>hf : Continuous f<VAR>a b : ℝ<GOAL>deriv (fun u => ∫ (x : ℝ) in a..u, f x) b = f b