ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>NontriviallyNormedField 𝕜<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : E → F<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>r : ℝ≥0∞<VAR>n : ℕ<VAR>x : E<VAR>hf : HasFiniteFPowerSeriesOnBall f p x n r<GOAL>CPolynomialOn 𝕜 f (EMetric.ball x r)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>NontriviallyNormedField 𝕜<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : E → F<GOAL>IsOpen {x | CPolynomialAt 𝕜 f x}
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>NontriviallyNormedField 𝕜<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : E → F<VAR>x : E<VAR>h : CPolynomialAt 𝕜 f x<GOAL>∀ᶠ (y : E) in 𝓝 x, CPolynomialAt 𝕜 f y
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>NontriviallyNormedField 𝕜<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : E → F<VAR>x : E<VAR>h : CPolynomialAt 𝕜 f x<GOAL>∃ s ∈ 𝓝 x, CPolynomialOn 𝕜 f s
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>NontriviallyNormedField 𝕜<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : E → F<VAR>x : E<VAR>h : CPolynomialAt 𝕜 f x<GOAL>∃ r, 0 < r ∧ CPolynomialOn 𝕜 f (Metric.ball x r)
<VAR>ι : Type u_3<VAR>M : Type u_4<VAR>AddCommMonoid M<VAR>I : WithTop (BoxIntegral.Box ι)<VAR>self : BoxIntegral.BoxAdditiveMap ι M I<VAR>J : BoxIntegral.Box ι<GOAL>↑J ≤ I → ∀ (π : BoxIntegral.Prepartition J), π.IsPartition → ∑ Ji ∈ π.boxes, self.toFun Ji = self.toFun J
<VAR>ι : Type u_1<VAR>M : Type u_2<VAR>AddCommMonoid M<VAR>I₀ : WithTop (BoxIntegral.Box ι)<VAR>f : BoxIntegral.Box ι → M<VAR>h : ∀ (J : BoxIntegral.Box ι), ↑J ≤ I₀ → ∀ (π : BoxIntegral.Prepartition J), π.IsPartition → ∑ Ji ∈ π.boxes, f Ji = f J<GOAL>⇑{ toFun := f, sum_partition_boxes' := h } = f
<VAR>ι : Type u_1<VAR>M : Type u_2<VAR>AddCommMonoid M<VAR>I₀ : WithTop (BoxIntegral.Box ι)<GOAL>Function.Injective fun f x => f x
<VAR>ι : Type u_1<VAR>M : Type u_2<VAR>AddCommMonoid M<VAR>I₀ : WithTop (BoxIntegral.Box ι)<VAR>f g : BoxIntegral.BoxAdditiveMap ι M I₀<GOAL>⇑f = ⇑g ↔ f = g
<VAR>ι : Type u_1<VAR>M : Type u_2<VAR>AddCommMonoid M<VAR>I₀ : WithTop (BoxIntegral.Box ι)<VAR>I : BoxIntegral.Box ι<VAR>f : BoxIntegral.BoxAdditiveMap ι M I₀<VAR>hI : ↑I ≤ I₀<VAR>π : BoxIntegral.Prepartition I<VAR>h : π.IsPartition<GOAL>∑ J ∈ π.boxes, f J = f I
<VAR>ι : Type u_1<VAR>M : Type u_2<VAR>AddCommMonoid M<VAR>I₀ : WithTop (BoxIntegral.Box ι)<GOAL>⇑0 = 0
<VAR>ι : Type u_1<VAR>M : Type u_2<VAR>AddCommMonoid M<VAR>I₀ : WithTop (BoxIntegral.Box ι)<VAR>I : BoxIntegral.Box ι<VAR>f : BoxIntegral.BoxAdditiveMap ι M I₀<VAR>hI : ↑I ≤ I₀<VAR>i : ι<VAR>x : ℝ<GOAL>Option.elim' 0 (⇑f) (I.splitLower i x) + Option.elim' 0 (⇑f) (I.splitUpper i x) = f I
<VAR>ι : Type u_1<VAR>M : Type u_2<VAR>AddCommMonoid M<VAR>I₀ : WithTop (BoxIntegral.Box ι)<VAR>f : BoxIntegral.BoxAdditiveMap ι M I₀<VAR>I : WithTop (BoxIntegral.Box ι)<VAR>hI : I ≤ I₀<VAR>a : BoxIntegral.Box ι<GOAL>(f.restrict I hI) a = f a
<VAR>ι : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>AddCommMonoid M<VAR>AddCommMonoid N<VAR>I₀ : WithTop (BoxIntegral.Box ι)<VAR>f : BoxIntegral.BoxAdditiveMap ι M I₀<VAR>g : M →+ N<GOAL>⇑(f.map g) = ⇑g ∘ ⇑f
<VAR>ι : Type u_1<VAR>M : Type u_2<VAR>AddCommMonoid M<VAR>I₀ : WithTop (BoxIntegral.Box ι)<VAR>I : BoxIntegral.Box ι<VAR>Finite ι<VAR>f : BoxIntegral.BoxAdditiveMap ι M I₀<VAR>hI : ↑I ≤ I₀<VAR>π₁ π₂ : BoxIntegral.Prepartition I<VAR>h : π₁.iUnion = π₂.iUnion<GOAL>∑ J ∈ π₁.boxes, f J = ∑ J ∈ π₂.boxes, f J
<VAR>ι : Type u_1<VAR>I₀ : WithTop (BoxIntegral.Box ι)<VAR>E : Type u_4<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>f : BoxIntegral.BoxAdditiveMap ι ℝ I₀<VAR>I : BoxIntegral.Box ι<VAR>x : E<GOAL>(f.toSMul I) x = f I • x
<VAR>n : ℕ<VAR>G : Type u<VAR>AddCommGroup G<VAR>I₀ : BoxIntegral.Box (Fin (n + 1))<VAR>i : Fin (n + 1)<VAR>f : ℝ → BoxIntegral.Box (Fin n) → G<VAR>fb : ↑(Set.Icc (I₀.lower i) (I₀.upper i)) → BoxIntegral.BoxAdditiveMap (Fin n) G ↑(I₀.face i)<VAR>hf : ∀ (x : ℝ) (hx : x ∈ Set.Icc (I₀.lower i) (I₀.upper i)) (J : BoxIntegral.Box (Fin n)), f x J = (fb ⟨x, hx⟩) J<VAR>J : BoxIntegral.Box (Fin (n + 1))<GOAL>(BoxIntegral.BoxAdditiveMap.upperSubLower I₀ i f fb hf) J = f (J.upper i) (J.face i) - f (J.lower i) (J.face i)
<GOAL>BoxIntegral.IntegrationParams.Henstock ≤ BoxIntegral.IntegrationParams.Riemann
<GOAL>BoxIntegral.IntegrationParams.Henstock ≤ BoxIntegral.IntegrationParams.McShane
<VAR>l : BoxIntegral.IntegrationParams<GOAL>BoxIntegral.IntegrationParams.GP ≤ l
<VAR>ι : Type u_1<VAR>Fintype ι<VAR>l : BoxIntegral.IntegrationParams<VAR>I : BoxIntegral.Box ι<VAR>c : ℝ≥0<VAR>r : (ι → ℝ) → ↑(Set.Ioi 0)<VAR>π : BoxIntegral.TaggedPrepartition I<VAR>self : l.MemBaseSet I c r π<GOAL>l.bHenstock = true → π.IsHenstock
<VAR>ι : Type u_1<VAR>Fintype ι<VAR>l : BoxIntegral.IntegrationParams<VAR>I : BoxIntegral.Box ι<VAR>c : ℝ≥0<VAR>r : (ι → ℝ) → ↑(Set.Ioi 0)<VAR>π : BoxIntegral.TaggedPrepartition I<VAR>self : l.MemBaseSet I c r π<GOAL>π.IsSubordinate r
<VAR>ι : Type u_1<VAR>Fintype ι<VAR>l : BoxIntegral.IntegrationParams<VAR>I : BoxIntegral.Box ι<VAR>c : ℝ≥0<VAR>r : (ι → ℝ) → ↑(Set.Ioi 0)<VAR>π : BoxIntegral.TaggedPrepartition I<VAR>self : l.MemBaseSet I c r π<GOAL>l.bDistortion = true → ∃ π', π'.iUnion = ↑I \ π.iUnion ∧ π'.distortion ≤ c
<VAR>ι : Type u_1<VAR>Fintype ι<VAR>l : BoxIntegral.IntegrationParams<VAR>I : BoxIntegral.Box ι<VAR>c : ℝ≥0<VAR>r : (ι → ℝ) → ↑(Set.Ioi 0)<VAR>π : BoxIntegral.TaggedPrepartition I<VAR>self : l.MemBaseSet I c r π<GOAL>l.bDistortion = true → π.distortion ≤ c
<VAR>ι : Type u_2<VAR>l : BoxIntegral.IntegrationParams<VAR>hl : l.bRiemann = false<VAR>r : (ι → ℝ) → ↑(Set.Ioi 0)<GOAL>l.RCond r
<VAR>ι : Type u_1<VAR>Fintype ι<VAR>l : BoxIntegral.IntegrationParams<VAR>I : BoxIntegral.Box ι<VAR>π₀ : BoxIntegral.Prepartition I<GOAL>l.toFilter I ⊓ 𝓟 {π | π.iUnion = π₀.iUnion} = l.toFilteriUnion I π₀
<VAR>ι : Type u_1<VAR>Fintype ι<VAR>c₁ c₂ : ℝ≥0<VAR>r₁ r₂ : (ι → ℝ) → ↑(Set.Ioi 0)<VAR>l₁ l₂ : BoxIntegral.IntegrationParams<VAR>I : BoxIntegral.Box ι<VAR>h : l₁ ≤ l₂<VAR>hc : c₁ ≤ c₂<VAR>π : BoxIntegral.TaggedPrepartition I<VAR>hr : ∀ J ∈ π, r₁ (π.tag J) ≤ r₂ (π.tag J)<VAR>hπ : l₁.MemBaseSet I c₁ r₁ π<GOAL>l₂.MemBaseSet I c₂ r₂ π
<VAR>ι : Type u_1<VAR>Fintype ι<VAR>c₁ c₂ : ℝ≥0<VAR>r₁ r₂ : (ι → ℝ) → ↑(Set.Ioi 0)<VAR>l₁ l₂ : BoxIntegral.IntegrationParams<VAR>I : BoxIntegral.Box ι<VAR>h : l₁ ≤ l₂<VAR>hc : c₁ ≤ c₂<VAR>π : BoxIntegral.TaggedPrepartition I<VAR>hr : ∀ x ∈ BoxIntegral.Box.Icc I, r₁ x ≤ r₂ x<VAR>hπ : l₁.MemBaseSet I c₁ r₁ π<GOAL>l₂.MemBaseSet I c₂ r₂ π
<VAR>ι : Type u_1<VAR>Fintype ι<VAR>I : BoxIntegral.Box ι<VAR>c₁ c₂ : ℝ≥0<VAR>r₁ r₂ : (ι → ℝ) → ↑(Set.Ioi 0)<VAR>π₁ π₂ : BoxIntegral.TaggedPrepartition I<VAR>l : BoxIntegral.IntegrationParams<VAR>h₁ : l.MemBaseSet I c₁ r₁ π₁<VAR>h₂ : l.MemBaseSet I c₂ r₂ π₂<VAR>hU : π₁.iUnion = π₂.iUnion<GOAL>∃ π, π.iUnion = ↑I \ π₁.iUnion ∧ (l.bDistortion = true → π.distortion ≤ c₁) ∧ (l.bDistortion = true → π.distortion ≤ c₂)
<VAR>ι : Type u_1<VAR>Fintype ι<VAR>I : BoxIntegral.Box ι<VAR>c : ℝ≥0<VAR>r₁ r₂ : (ι → ℝ) → ↑(Set.Ioi 0)<VAR>π₁ : BoxIntegral.TaggedPrepartition I<VAR>l : BoxIntegral.IntegrationParams<VAR>hπ₁ : l.MemBaseSet I c r₁ π₁<VAR>hle : ∀ x ∈ BoxIntegral.Box.Icc I, r₂ x ≤ r₁ x<VAR>π₂ : BoxIntegral.Prepartition I<VAR>hU : π₂.iUnion = ↑I \ π₁.iUnion<VAR>hc : l.bDistortion = true → π₂.distortion ≤ c<GOAL>l.MemBaseSet I c r₁ (π₁.unionComplToSubordinate π₂ hU r₂)
<VAR>ι : Type u_1<VAR>Fintype ι<VAR>I : BoxIntegral.Box ι<VAR>c : ℝ≥0<VAR>r : (ι → ℝ) → ↑(Set.Ioi 0)<VAR>π : BoxIntegral.TaggedPrepartition I<VAR>l : BoxIntegral.IntegrationParams<VAR>hπ : l.MemBaseSet I c r π<VAR>p : BoxIntegral.Box ι → Prop<GOAL>l.MemBaseSet I c r (π.filter p)
<VAR>ι : Type u_1<VAR>Fintype ι<VAR>I : BoxIntegral.Box ι<VAR>c : ℝ≥0<VAR>r : (ι → ℝ) → ↑(Set.Ioi 0)<VAR>l : BoxIntegral.IntegrationParams<VAR>π : BoxIntegral.Prepartition I<VAR>πi : (J : BoxIntegral.Box ι) → BoxIntegral.TaggedPrepartition J<VAR>h : ∀ J ∈ π, l.MemBaseSet J c r (πi J)<VAR>hp : ∀ J ∈ π, (πi J).IsPartition<VAR>hc : l.bDistortion = true → π.compl.distortion ≤ c<GOAL>l.MemBaseSet I c r (π.biUnionTagged πi)
<VAR>l₁ l₂ : BoxIntegral.IntegrationParams<VAR>ι : Type u_2<VAR>r : (ι → ℝ) → ↑(Set.Ioi 0)<VAR>h : l₁ ≤ l₂<VAR>hr : l₂.RCond r<GOAL>l₁.RCond r
<VAR>l : BoxIntegral.IntegrationParams<VAR>ι : Type u_2<VAR>r₁ r₂ : (ι → ℝ) → ↑(Set.Ioi 0)<VAR>h₁ : l.RCond r₁<VAR>h₂ : l.RCond r₂<GOAL>l.RCond fun x => min (r₁ x) (r₂ x)
<VAR>ι : Type u_1<VAR>Fintype ι<VAR>c₁ c₂ : ℝ≥0<VAR>l₁ l₂ : BoxIntegral.IntegrationParams<VAR>I : BoxIntegral.Box ι<VAR>h : l₁ ≤ l₂<VAR>hc : c₁ ≤ c₂<GOAL>l₁.toFilterDistortion I c₁ ≤ l₂.toFilterDistortion I c₂
<VAR>ι : Type u_1<VAR>Fintype ι<VAR>I : BoxIntegral.Box ι<VAR>l₁ l₂ : BoxIntegral.IntegrationParams<VAR>h : l₁ ≤ l₂<GOAL>l₁.toFilter I ≤ l₂.toFilter I
<VAR>ι : Type u_1<VAR>Fintype ι<VAR>I : BoxIntegral.Box ι<VAR>l₁ l₂ : BoxIntegral.IntegrationParams<VAR>h : l₁ ≤ l₂<VAR>π₀ : BoxIntegral.Prepartition I<GOAL>l₁.toFilteriUnion I π₀ ≤ l₂.toFilteriUnion I π₀
<VAR>ι : Type u_1<VAR>Fintype ι<VAR>I : BoxIntegral.Box ι<VAR>l : BoxIntegral.IntegrationParams<VAR>π₁ π₂ : BoxIntegral.Prepartition I<VAR>h : π₁.iUnion = π₂.iUnion<GOAL>l.toFilteriUnion I π₁ = l.toFilteriUnion I π₂
<VAR>ι : Type u_1<VAR>Fintype ι<VAR>l : BoxIntegral.IntegrationParams<VAR>I : BoxIntegral.Box ι<VAR>c : ℝ≥0<GOAL>(l.toFilterDistortion I c).HasBasis l.RCond fun r => {π | l.MemBaseSet I c r π}
<VAR>ι : Type u_1<VAR>Fintype ι<VAR>l : BoxIntegral.IntegrationParams<VAR>I : BoxIntegral.Box ι<VAR>c : ℝ≥0<VAR>π₀ : BoxIntegral.Prepartition I<GOAL>(l.toFilterDistortioniUnion I c π₀).HasBasis l.RCond fun r => {π | l.MemBaseSet I c r π ∧ π.iUnion = π₀.iUnion}
<VAR>ι : Type u_1<VAR>Fintype ι<VAR>l : BoxIntegral.IntegrationParams<VAR>I : BoxIntegral.Box ι<VAR>π₀ : BoxIntegral.Prepartition I<GOAL>(l.toFilteriUnion I π₀).HasBasis (fun r => ∀ (c : ℝ≥0), l.RCond (r c)) fun r => {π | ∃ c, l.MemBaseSet I c (r c) π ∧ π.iUnion = π₀.iUnion}
<VAR>ι : Type u_1<VAR>Fintype ι<VAR>l : BoxIntegral.IntegrationParams<VAR>I : BoxIntegral.Box ι<GOAL>(l.toFilteriUnion I ⊤).HasBasis (fun r => ∀ (c : ℝ≥0), l.RCond (r c)) fun r => {π | ∃ c, l.MemBaseSet I c (r c) π ∧ π.IsPartition}
<VAR>ι : Type u_1<VAR>Fintype ι<VAR>l : BoxIntegral.IntegrationParams<VAR>I : BoxIntegral.Box ι<GOAL>(l.toFilter I).HasBasis (fun r => ∀ (c : ℝ≥0), l.RCond (r c)) fun r => {π | ∃ c, l.MemBaseSet I c (r c) π}
<VAR>ι : Type u_1<VAR>Fintype ι<VAR>I J : BoxIntegral.Box ι<VAR>l : BoxIntegral.IntegrationParams<VAR>h : I ≤ J<GOAL>Filter.Tendsto (⇑(BoxIntegral.TaggedPrepartition.embedBox I J h)) (l.toFilteriUnion I ⊤) (l.toFilteriUnion J (BoxIntegral.Prepartition.single J I h))
<VAR>ι : Type u_1<VAR>Fintype ι<VAR>I : BoxIntegral.Box ι<VAR>c : ℝ≥0<VAR>l : BoxIntegral.IntegrationParams<VAR>π₀ : BoxIntegral.Prepartition I<VAR>hc₁ : π₀.distortion ≤ c<VAR>hc₂ : π₀.compl.distortion ≤ c<VAR>r : (ι → ℝ) → ↑(Set.Ioi 0)<GOAL>∃ π, l.MemBaseSet I c r π ∧ π.toPrepartition ≤ π₀ ∧ π.iUnion = π₀.iUnion
<VAR>ι : Type u_1<VAR>Fintype ι<VAR>c : ℝ≥0<VAR>l : BoxIntegral.IntegrationParams<VAR>I : BoxIntegral.Box ι<VAR>hc : I.distortion ≤ c<VAR>r : (ι → ℝ) → ↑(Set.Ioi 0)<GOAL>∃ π, l.MemBaseSet I c r π ∧ π.IsPartition
<VAR>ι : Type u_1<VAR>Fintype ι<VAR>c : ℝ≥0<VAR>l : BoxIntegral.IntegrationParams<VAR>I : BoxIntegral.Box ι<VAR>π₀ : BoxIntegral.Prepartition I<VAR>hc₁ : π₀.distortion ≤ c<VAR>hc₂ : π₀.compl.distortion ≤ c<GOAL>(l.toFilterDistortioniUnion I c π₀).NeBot
<VAR>ι : Type u_1<VAR>Fintype ι<VAR>l : BoxIntegral.IntegrationParams<VAR>I : BoxIntegral.Box ι<GOAL>∀ᶠ (π : BoxIntegral.TaggedPrepartition I) in l.toFilteriUnion I ⊤, π.IsPartition
<VAR>ι : Type u_1<VAR>I : BoxIntegral.Box ι<VAR>i : ι<VAR>x : ℝ<GOAL>↑(I.splitLower i x) = ↑I ∩ {y | y i ≤ x}
<VAR>ι : Type u_1<VAR>I : BoxIntegral.Box ι<VAR>i : ι<VAR>x : ℝ<GOAL>I.splitLower i x ≤ ↑I
<VAR>ι : Type u_1<VAR>I : BoxIntegral.Box ι<VAR>i : ι<VAR>x : ℝ<GOAL>I.splitLower i x = ⊥ ↔ x ≤ I.lower i
<VAR>ι : Type u_1<VAR>I : BoxIntegral.Box ι<VAR>i : ι<VAR>x : ℝ<GOAL>I.splitLower i x = ↑I ↔ I.upper i ≤ x
<VAR>ι : Type u_1<VAR>I : BoxIntegral.Box ι<VAR>DecidableEq ι<VAR>i : ι<VAR>x : ℝ<VAR>h : x ∈ Set.Ioo (I.lower i) (I.upper i)<VAR>h' : ∀ (j : ι), I.lower j < Function.update I.upper i x j := ⋯<GOAL>I.splitLower i x = ↑{ lower := I.lower, upper := Function.update I.upper i x, lower_lt_upper := h' }
<VAR>ι : Type u_1<VAR>I : BoxIntegral.Box ι<VAR>i : ι<VAR>x : ℝ<GOAL>↑(I.splitUpper i x) = ↑I ∩ {y | x < y i}
<VAR>ι : Type u_1<VAR>I : BoxIntegral.Box ι<VAR>i : ι<VAR>x : ℝ<GOAL>I.splitUpper i x ≤ ↑I
<VAR>ι : Type u_1<VAR>I : BoxIntegral.Box ι<VAR>i : ι<VAR>x : ℝ<GOAL>I.splitUpper i x = ⊥ ↔ I.upper i ≤ x
<VAR>ι : Type u_1<VAR>I : BoxIntegral.Box ι<VAR>i : ι<VAR>x : ℝ<GOAL>I.splitUpper i x = ↑I ↔ x ≤ I.lower i
<VAR>ι : Type u_1<VAR>I : BoxIntegral.Box ι<VAR>DecidableEq ι<VAR>i : ι<VAR>x : ℝ<VAR>h : x ∈ Set.Ioo (I.lower i) (I.upper i)<VAR>h' : ∀ (j : ι), Function.update I.lower i x j < I.upper j := ⋯<GOAL>I.splitUpper i x = ↑{ lower := Function.update I.lower i x, upper := I.upper, lower_lt_upper := h' }
<VAR>ι : Type u_1<VAR>I : BoxIntegral.Box ι<VAR>i : ι<VAR>x : ℝ<GOAL>Disjoint (I.splitLower i x) (I.splitUpper i x)
<VAR>ι : Type u_1<VAR>I : BoxIntegral.Box ι<VAR>i : ι<VAR>x : ℝ<GOAL>I.splitLower i x ≠ I.splitUpper i x
<VAR>ι : Type u_1<VAR>I J : BoxIntegral.Box ι<VAR>i : ι<VAR>x : ℝ<GOAL>J ∈ BoxIntegral.Prepartition.split I i x ↔ ↑J = I.splitLower i x ∨ ↑J = I.splitUpper i x
<VAR>ι : Type u_1<VAR>I J : BoxIntegral.Box ι<VAR>i : ι<VAR>x : ℝ<GOAL>J ∈ BoxIntegral.Prepartition.split I i x ↔ ↑J = ↑I ∩ {y | y i ≤ x} ∨ ↑J = ↑I ∩ {y | x < y i}
<VAR>ι : Type u_1<VAR>I : BoxIntegral.Box ι<VAR>i : ι<VAR>x : ℝ<GOAL>(BoxIntegral.Prepartition.split I i x).iUnion = ↑I
<VAR>ι : Type u_1<VAR>I : BoxIntegral.Box ι<VAR>i : ι<VAR>x : ℝ<GOAL>(BoxIntegral.Prepartition.split I i x).IsPartition
<VAR>ι : Type u_1<VAR>M : Type u_3<VAR>AddCommMonoid M<VAR>I : BoxIntegral.Box ι<VAR>i : ι<VAR>x : ℝ<VAR>f : BoxIntegral.Box ι → M<GOAL>∑ J ∈ (BoxIntegral.Prepartition.split I i x).boxes, f J = Option.elim' 0 f (I.splitLower i x) + Option.elim' 0 f (I.splitUpper i x)
<VAR>ι : Type u_1<VAR>I : BoxIntegral.Box ι<VAR>i : ι<VAR>x : ℝ<VAR>h : x ∉ Set.Ioo (I.lower i) (I.upper i)<GOAL>BoxIntegral.Prepartition.split I i x = ⊤
<VAR>ι : Type u_1<VAR>I J : BoxIntegral.Box ι<VAR>i : ι<VAR>x : ℝ<VAR>y : ι → ℝ<VAR>h₁ : J ∈ BoxIntegral.Prepartition.split I i x<VAR>h₂ : y ∈ J<VAR>h₃ : y i ≤ x<GOAL>↑J = ↑I ∩ {y | y i ≤ x}
<VAR>ι : Type u_1<VAR>I J : BoxIntegral.Box ι<VAR>i : ι<VAR>x : ℝ<VAR>y : ι → ℝ<VAR>h₁ : J ∈ BoxIntegral.Prepartition.split I i x<VAR>h₂ : y ∈ J<VAR>h₃ : x < y i<GOAL>↑J = ↑I ∩ {y | x < y i}
<VAR>ι : Type u_1<VAR>I J : BoxIntegral.Box ι<VAR>h : I ≤ J<VAR>i : ι<VAR>x : ℝ<GOAL>(BoxIntegral.Prepartition.split J i x).restrict I = BoxIntegral.Prepartition.split I i x
<VAR>ι : Type u_1<VAR>I : BoxIntegral.Box ι<VAR>π : BoxIntegral.Prepartition I<VAR>i : ι<VAR>x : ℝ<GOAL>π ⊓ BoxIntegral.Prepartition.split I i x = π.biUnion fun J => BoxIntegral.Prepartition.split J i x
<VAR>ι : Type u_1<VAR>I : BoxIntegral.Box ι<GOAL>BoxIntegral.Prepartition.splitMany I ∅ = ⊤
<VAR>ι : Type u_1<VAR>I : BoxIntegral.Box ι<VAR>s : Finset (ι × ℝ)<VAR>p : ι × ℝ<GOAL>BoxIntegral.Prepartition.splitMany I (insert p s) = BoxIntegral.Prepartition.splitMany I s ⊓ BoxIntegral.Prepartition.split I p.1 p.2
<VAR>ι : Type u_1<VAR>I : BoxIntegral.Box ι<VAR>s : Finset (ι × ℝ)<VAR>p : ι × ℝ<VAR>hp : p ∈ s<GOAL>BoxIntegral.Prepartition.splitMany I s ≤ BoxIntegral.Prepartition.split I p.1 p.2
<VAR>ι : Type u_1<VAR>I : BoxIntegral.Box ι<VAR>s : Finset (ι × ℝ)<GOAL>(BoxIntegral.Prepartition.splitMany I s).IsPartition
<VAR>ι : Type u_1<VAR>I : BoxIntegral.Box ι<VAR>s : Finset (ι × ℝ)<GOAL>(BoxIntegral.Prepartition.splitMany I s).iUnion = ↑I
<VAR>ι : Type u_1<VAR>I : BoxIntegral.Box ι<VAR>π : BoxIntegral.Prepartition I<VAR>s : Finset (ι × ℝ)<GOAL>π ⊓ BoxIntegral.Prepartition.splitMany I s = π.biUnion fun J => BoxIntegral.Prepartition.splitMany J s
<VAR>ι : Type u_1<VAR>I J Js : BoxIntegral.Box ι<VAR>s : Finset (ι × ℝ)<VAR>H : ∀ (i : ι), {(i, J.lower i), (i, J.upper i)} ⊆ s<VAR>HJs : Js ∈ BoxIntegral.Prepartition.splitMany I s<VAR>Hn : ¬Disjoint ↑J ↑Js<GOAL>Js ≤ J
<VAR>ι : Type u_1<VAR>Finite ι<VAR>s : Finset (BoxIntegral.Box ι)<GOAL>∀ᶠ (t : Finset (ι × ℝ)) in Filter.atTop, ∀ (I J : BoxIntegral.Box ι), J ∈ s → ∀ J' ∈ BoxIntegral.Prepartition.splitMany I t, ¬Disjoint ↑J ↑J' → J' ≤ J
<VAR>ι : Type u_1<VAR>I : BoxIntegral.Box ι<VAR>Finite ι<VAR>π : BoxIntegral.Prepartition I<GOAL>∀ᶠ (t : Finset (ι × ℝ)) in Filter.atTop, π ⊓ BoxIntegral.Prepartition.splitMany I t = (BoxIntegral.Prepartition.splitMany I t).filter fun J => ↑J ⊆ π.iUnion
<VAR>ι : Type u_1<VAR>I : BoxIntegral.Box ι<VAR>Finite ι<VAR>s : Set (BoxIntegral.Prepartition I)<VAR>hs : s.Finite<GOAL>∃ t, ∀ π ∈ s, π ⊓ BoxIntegral.Prepartition.splitMany I t = (BoxIntegral.Prepartition.splitMany I t).filter fun J => ↑J ⊆ π.iUnion
<VAR>ι : Type u_1<VAR>Finite ι<VAR>I : BoxIntegral.Box ι<VAR>π : BoxIntegral.Prepartition I<VAR>h : π.IsPartition<GOAL>∃ s, BoxIntegral.Prepartition.splitMany I s ≤ π
<VAR>ι : Type u_1<VAR>I : BoxIntegral.Box ι<VAR>Finite ι<VAR>π : BoxIntegral.Prepartition I<GOAL>∃ π', π'.iUnion = ↑I \ π.iUnion
<VAR>ι : Type u_1<VAR>I : BoxIntegral.Box ι<VAR>Finite ι<VAR>π : BoxIntegral.Prepartition I<GOAL>π.compl.iUnion = ↑I \ π.iUnion
<VAR>ι : Type u_1<VAR>I : BoxIntegral.Box ι<VAR>Finite ι<VAR>π₁ π₂ : BoxIntegral.Prepartition I<VAR>h : π₁.iUnion = π₂.iUnion<GOAL>π₁.compl = π₂.compl
<VAR>ι : Type u_1<VAR>I : BoxIntegral.Box ι<VAR>Finite ι<VAR>π : BoxIntegral.Prepartition I<VAR>h : π.IsPartition<GOAL>π.compl = ⊥
<VAR>ι : Type u_1<VAR>I : BoxIntegral.Box ι<VAR>Finite ι<GOAL>⊤.compl = ⊥
<GOAL>Filter.Tendsto (fun n => (↑n)⁻¹) Filter.atTop (𝓝 0)
<VAR>C : ℝ<GOAL>Filter.Tendsto (fun n => C / ↑n) Filter.atTop (𝓝 0)
<GOAL>Filter.Tendsto (fun n => 1 / ↑n) Filter.atTop (𝓝 0)
<VAR>C : ℝ≥0<GOAL>Filter.Tendsto (fun n => C / ↑n) Filter.atTop (𝓝 0)
<VAR>C : EReal<VAR>h : C ≠ ⊥<VAR>h' : C ≠ ⊤<GOAL>Filter.Tendsto (fun n => C / ↑n) Filter.atTop (𝓝 0)
<GOAL>Filter.Tendsto (fun n => 1 / (↑n + 1)) Filter.atTop (𝓝 0)
<VAR>𝕜 : Type u_4<VAR>Semiring 𝕜<VAR>Algebra ℝ≥0 𝕜<VAR>TopologicalSpace 𝕜<VAR>ContinuousSMul ℝ≥0 𝕜<GOAL>Filter.Tendsto (⇑(algebraMap ℝ≥0 𝕜) ∘ fun n => (↑n)⁻¹) Filter.atTop (𝓝 0)
<VAR>𝕜 : Type u_4<VAR>Semiring 𝕜<VAR>Algebra ℝ 𝕜<VAR>TopologicalSpace 𝕜<VAR>ContinuousSMul ℝ 𝕜<GOAL>Filter.Tendsto (⇑(algebraMap ℝ 𝕜) ∘ fun n => (↑n)⁻¹) Filter.atTop (𝓝 0)
<VAR>𝕜 : Type u_4<VAR>DivisionRing 𝕜<VAR>TopologicalSpace 𝕜<VAR>CharZero 𝕜<VAR>Algebra ℝ 𝕜<VAR>ContinuousSMul ℝ 𝕜<VAR>TopologicalDivisionRing 𝕜<VAR>x : 𝕜<GOAL>Filter.Tendsto (fun n => ↑n / (↑n + x)) Filter.atTop (𝓝 1)
<VAR>α : Type u_1<VAR>LinearOrderedSemiring α<VAR>Archimedean α<VAR>r : α<VAR>h : 0 < r<GOAL>Filter.Tendsto (fun n => (r + 1) ^ n) Filter.atTop Filter.atTop
<VAR>α : Type u_1<VAR>LinearOrderedRing α<VAR>Archimedean α<VAR>r : α<VAR>h : 1 < r<GOAL>Filter.Tendsto (fun n => r ^ n) Filter.atTop Filter.atTop
<VAR>m : ℕ<VAR>h : 1 < m<GOAL>Filter.Tendsto (fun n => m ^ n) Filter.atTop Filter.atTop
<VAR>𝕜 : Type u_4<VAR>LinearOrderedField 𝕜<VAR>Archimedean 𝕜<VAR>TopologicalSpace 𝕜<VAR>OrderTopology 𝕜<VAR>r : 𝕜<VAR>h₁ : 0 ≤ r<VAR>h₂ : r < 1<GOAL>Filter.Tendsto (fun n => r ^ n) Filter.atTop (𝓝 0)
<VAR>𝕜 : Type u_4<VAR>LinearOrderedField 𝕜<VAR>Archimedean 𝕜<VAR>TopologicalSpace 𝕜<VAR>OrderTopology 𝕜<VAR>r : 𝕜<GOAL>Filter.Tendsto (fun n => r ^ n) Filter.atTop (𝓝 0) ↔ |r| < 1
<VAR>𝕜 : Type u_4<VAR>LinearOrderedField 𝕜<VAR>Archimedean 𝕜<VAR>TopologicalSpace 𝕜<VAR>OrderTopology 𝕜<VAR>r : 𝕜<VAR>h₁ : 0 < r<VAR>h₂ : r < 1<GOAL>Filter.Tendsto (fun n => r ^ n) Filter.atTop (𝓝[>] 0)
<VAR>α : Type u_4<VAR>PseudoMetricSpace α<VAR>r : ℝ<VAR>h₀ : 0 < r<VAR>h₁ : r < 1<GOAL>(uniformity α).HasBasis (fun x => True) fun k => {p | dist p.1 p.2 < r ^ k}
<VAR>u : ℕ → ℝ<VAR>c : ℝ<VAR>hc : 0 ≤ c<VAR>n : ℕ<VAR>hn : 0 < n<VAR>h : ∀ k < n, c * u k < u (k + 1)<GOAL>c ^ n * u 0 < u n
<VAR>u : ℕ → ℝ<VAR>c : ℝ<VAR>hc : 0 ≤ c<VAR>n : ℕ<VAR>h : ∀ k < n, c * u k ≤ u (k + 1)<GOAL>c ^ n * u 0 ≤ u n
<VAR>u : ℕ → ℝ<VAR>c : ℝ<VAR>hc : 0 ≤ c<VAR>n : ℕ<VAR>hn : 0 < n<VAR>h : ∀ k < n, u (k + 1) < c * u k<GOAL>u n < c ^ n * u 0
<VAR>u : ℕ → ℝ<VAR>c : ℝ<VAR>hc : 0 ≤ c<VAR>n : ℕ<VAR>h : ∀ k < n, u (k + 1) ≤ c * u k<GOAL>u n ≤ c ^ n * u 0
<VAR>v : ℕ → ℝ<VAR>c : ℝ<VAR>h₀ : 0 < v 0<VAR>hc : 1 < c<VAR>hu : ∀ (n : ℕ), c * v n ≤ v (n + 1)<GOAL>Filter.Tendsto v Filter.atTop Filter.atTop
<VAR>r : ℝ≥0<VAR>hr : r < 1<GOAL>Filter.Tendsto (fun n => r ^ n) Filter.atTop (𝓝 0)
<VAR>r : ℝ≥0<GOAL>Filter.Tendsto (fun n => r ^ n) Filter.atTop (𝓝 0) ↔ r < 1
<VAR>r : ℝ≥0∞<VAR>hr : r < 1<GOAL>Filter.Tendsto (fun n => r ^ n) Filter.atTop (𝓝 0)
<VAR>r : ℝ≥0∞<GOAL>Filter.Tendsto (fun n => r ^ n) Filter.atTop (𝓝 0) ↔ r < 1
<VAR>r : ℝ<VAR>h₁ : 0 ≤ r<VAR>h₂ : r < 1<GOAL>HasSum (fun n => r ^ n) (1 - r)⁻¹
<VAR>r : ℝ<VAR>h₁ : 0 ≤ r<VAR>h₂ : r < 1<GOAL>Summable fun n => r ^ n
<VAR>r : ℝ<VAR>h₁ : 0 ≤ r<VAR>h₂ : r < 1<GOAL>∑' (n : ℕ), r ^ n = (1 - r)⁻¹
<GOAL>HasSum (fun n => (1 / 2) ^ n) 2
<VAR>ι : Type u_4<VAR>Encodable ι<GOAL>Summable fun i => (1 / 2) ^ Encodable.encode i
<GOAL>∑' (n : ℕ), (1 / 2) ^ n = 2
<VAR>n : ℕ<GOAL>∑ i ∈ Finset.range n, (1 / 2) ^ i ≤ 2
<GOAL>∑' (n : ℕ), 2⁻¹ ^ n = 2
<VAR>n : ℕ<GOAL>(∑' (i : ℕ), if n ≤ i then 2⁻¹ ^ i else 0) = 2 * 2⁻¹ ^ n
<VAR>a : ℝ<GOAL>HasSum (fun n => a / 2 / 2 ^ n) a
<VAR>a : ℝ<GOAL>Summable fun n => a / 2 / 2 ^ n
<VAR>a : ℝ<GOAL>∑' (n : ℕ), a / 2 / 2 ^ n = a
<VAR>r : ℝ≥0<VAR>hr : r < 1<GOAL>HasSum (fun n => r ^ n) (1 - r)⁻¹
<VAR>r : ℝ≥0<VAR>hr : r < 1<GOAL>Summable fun n => r ^ n
<VAR>r : ℝ≥0<VAR>hr : r < 1<GOAL>∑' (n : ℕ), r ^ n = (1 - r)⁻¹
<VAR>r : ℝ≥0∞<GOAL>∑' (n : ℕ), r ^ n = (1 - r)⁻¹
<VAR>r : ℝ≥0∞<GOAL>∑' (n : ℕ), r ^ (n + 1) = r * (1 - r)⁻¹
<VAR>α : Type u_1<VAR>PseudoEMetricSpace α<VAR>r C : ℝ≥0∞<VAR>hr : r < 1<VAR>hC : C ≠ ⊤<VAR>f : ℕ → α<VAR>hu : ∀ (n : ℕ), edist (f n) (f (n + 1)) ≤ C * r ^ n<GOAL>CauchySeq f
<VAR>α : Type u_1<VAR>PseudoEMetricSpace α<VAR>r C : ℝ≥0∞<VAR>f : ℕ → α<VAR>hu : ∀ (n : ℕ), edist (f n) (f (n + 1)) ≤ C * r ^ n<VAR>a : α<VAR>ha : Filter.Tendsto f Filter.atTop (𝓝 a)<VAR>n : ℕ<GOAL>edist (f n) a ≤ C * r ^ n / (1 - r)
<VAR>α : Type u_1<VAR>PseudoEMetricSpace α<VAR>r C : ℝ≥0∞<VAR>f : ℕ → α<VAR>hu : ∀ (n : ℕ), edist (f n) (f (n + 1)) ≤ C * r ^ n<VAR>a : α<VAR>ha : Filter.Tendsto f Filter.atTop (𝓝 a)<GOAL>edist (f 0) a ≤ C / (1 - r)
<VAR>α : Type u_1<VAR>PseudoEMetricSpace α<VAR>C : ℝ≥0∞<VAR>hC : C ≠ ⊤<VAR>f : ℕ → α<VAR>hu : ∀ (n : ℕ), edist (f n) (f (n + 1)) ≤ C / 2 ^ n<GOAL>CauchySeq f
<VAR>α : Type u_1<VAR>PseudoEMetricSpace α<VAR>C : ℝ≥0∞<VAR>f : ℕ → α<VAR>hu : ∀ (n : ℕ), edist (f n) (f (n + 1)) ≤ C / 2 ^ n<VAR>a : α<VAR>ha : Filter.Tendsto f Filter.atTop (𝓝 a)<VAR>n : ℕ<GOAL>edist (f n) a ≤ 2 * C / 2 ^ n
<VAR>α : Type u_1<VAR>PseudoEMetricSpace α<VAR>C : ℝ≥0∞<VAR>f : ℕ → α<VAR>hu : ∀ (n : ℕ), edist (f n) (f (n + 1)) ≤ C / 2 ^ n<VAR>a : α<VAR>ha : Filter.Tendsto f Filter.atTop (𝓝 a)<GOAL>edist (f 0) a ≤ 2 * C
<VAR>α : Type u_1<VAR>PseudoMetricSpace α<VAR>r C : ℝ<VAR>hr : r < 1<VAR>f : ℕ → α<VAR>hu : ∀ (n : ℕ), dist (f n) (f (n + 1)) ≤ C * r ^ n<GOAL>HasSum (fun n => C * r ^ n) (C / (1 - r))
<VAR>α : Type u_1<VAR>PseudoMetricSpace α<VAR>r C : ℝ<VAR>hr : r < 1<VAR>f : ℕ → α<VAR>hu : ∀ (n : ℕ), dist (f n) (f (n + 1)) ≤ C * r ^ n<GOAL>CauchySeq f
<VAR>α : Type u_1<VAR>PseudoMetricSpace α<VAR>r C : ℝ<VAR>hr : r < 1<VAR>f : ℕ → α<VAR>hu : ∀ (n : ℕ), dist (f n) (f (n + 1)) ≤ C * r ^ n<VAR>a : α<VAR>ha : Filter.Tendsto f Filter.atTop (𝓝 a)<GOAL>dist (f 0) a ≤ C / (1 - r)
<VAR>α : Type u_1<VAR>PseudoMetricSpace α<VAR>r C : ℝ<VAR>hr : r < 1<VAR>f : ℕ → α<VAR>hu : ∀ (n : ℕ), dist (f n) (f (n + 1)) ≤ C * r ^ n<VAR>a : α<VAR>ha : Filter.Tendsto f Filter.atTop (𝓝 a)<VAR>n : ℕ<GOAL>dist (f n) a ≤ C * r ^ n / (1 - r)
<VAR>α : Type u_1<VAR>PseudoMetricSpace α<VAR>C : ℝ<VAR>f : ℕ → α<VAR>hu₂ : ∀ (n : ℕ), dist (f n) (f (n + 1)) ≤ C / 2 / 2 ^ n<GOAL>CauchySeq f
<VAR>α : Type u_1<VAR>PseudoMetricSpace α<VAR>C : ℝ<VAR>f : ℕ → α<VAR>hu₂ : ∀ (n : ℕ), dist (f n) (f (n + 1)) ≤ C / 2 / 2 ^ n<VAR>a : α<VAR>ha : Filter.Tendsto f Filter.atTop (𝓝 a)<GOAL>dist (f 0) a ≤ C
<VAR>α : Type u_1<VAR>PseudoMetricSpace α<VAR>C : ℝ<VAR>f : ℕ → α<VAR>hu₂ : ∀ (n : ℕ), dist (f n) (f (n + 1)) ≤ C / 2 / 2 ^ n<VAR>a : α<VAR>ha : Filter.Tendsto f Filter.atTop (𝓝 a)<VAR>n : ℕ<GOAL>dist (f n) a ≤ C / 2 ^ n