ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>F : Type u<VAR>E : Type v<VAR>inst✝⁵ : Field F<VAR>inst✝⁴ : Field E<VAR>inst✝³ : Algebra F E<VAR>K : Type w<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra F K<VAR>inst✝ : IsAlgClosure F E<VAR>H : IsPurelyInseparable F E<VAR>this : IsAlgClosed E<GOAL>IsSepClosed F
<VAR>R : Type u<VAR>S : Type v<VAR>a b c d : R<VAR>n m : ℕ<VAR>inst✝ : Semiring R<VAR>p✝ p q : R[X]<VAR>ι : Type u_1<VAR>h : p.support.card ≤ 1<GOAL>(monomial p.natDegree) p.leadingCoeff = p
<VAR>X : Type u_1<VAR>Y : Sort u_2<VAR>A : Type ?u.5630<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace A<VAR>f : X → Y<VAR>x x' : X<VAR>x✝ : f x = f x'<GOAL>(x ≠ x' → ∃ s₁ s₂, IsOpen s₁ ∧ IsOpen s₂ ∧ x ∈ s₁ ∧ x' ∈ s₂ ∧ Disjoint s₁ s₂) ↔ x ≠ x' → Disjoint (𝓝 x) (𝓝 x')
<VAR>R : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝¹¹ : CommRing R<VAR>inst✝¹⁰ : AddCommGroup E<VAR>inst✝⁹ : AddCommGroup F<VAR>inst✝⁸ : Module R E<VAR>inst✝⁷ : Module R F<VAR>inst✝⁶ : TopologicalSpace E<VAR>inst✝⁵ : TopologicalSpace F<VAR>inst✝⁴ : ContinuousAdd E<VAR>inst✝³ : ContinuousAdd F<VAR>inst✝² : TopologicalSpace R<VAR>inst✝¹ : ContinuousSMul R E<VAR>inst✝ : ContinuousSMul R F<VAR>f : E →ₗ.[R] F<VAR>hf : LinearMap.ker f.toFun = ⊥<VAR>hf' : f.IsClosable<VAR>hcf : LinearMap.ker f.closure.toFun = ⊥<GOAL>f.inverse.closure = f.closure.inverse
<VAR>R : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝¹¹ : CommRing R<VAR>inst✝¹⁰ : AddCommGroup E<VAR>inst✝⁹ : AddCommGroup F<VAR>inst✝⁸ : Module R E<VAR>inst✝⁷ : Module R F<VAR>inst✝⁶ : TopologicalSpace E<VAR>inst✝⁵ : TopologicalSpace F<VAR>inst✝⁴ : ContinuousAdd E<VAR>inst✝³ : ContinuousAdd F<VAR>inst✝² : TopologicalSpace R<VAR>inst✝¹ : ContinuousSMul R E<VAR>inst✝ : ContinuousSMul R F<VAR>f : E →ₗ.[R] F<VAR>hf : LinearMap.ker f.toFun = ⊥<VAR>hf' : f.IsClosable<VAR>hcf : LinearMap.ker f.closure.toFun = ⊥<GOAL>f.inverse.closure.graph = f.closure.inverse.graph
<VAR>l : Type u_1<VAR>m : Type u<VAR>n : Type u'<VAR>α : Type v<VAR>inst✝² : Fintype n<VAR>inst✝¹ : DecidableEq n<VAR>inst✝ : CommRing α<VAR>A✝ B : Matrix n n α<VAR>A : (Matrix n n α)ˣ<VAR>this : Invertible ↑A := A.invertible<GOAL>↑A⁻¹ = (↑A)⁻¹
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Sort w<VAR>γ : Type x<VAR>s t : Set α<VAR>hs : s.Infinite<VAR>ht : t.Finite<GOAL>∃ a ∈ s, a ∉ t
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Sort w<VAR>γ : Type x<VAR>s t : Set α<VAR>hs : s.Infinite<VAR>ht : t.Finite<VAR>h : ∀ a ∈ s, a ∈ t<GOAL>False
<GOAL>(fun τ => jacobiTheta τ - 1) =O[comap im atTop] fun τ => rexp (-π * τ.im)
<GOAL>∃ c a, ∀ b ≥ a, ∀ (a : ℂ), a.im = b → ‖jacobiTheta a - 1‖ ≤ c * ‖rexp (-π * a.im)‖
<VAR>y : ℝ<VAR>hy : y ≥ 1<VAR>τ : ℂ<VAR>hτ : τ.im = y<GOAL>2 / (1 - rexp (-π * τ.im)) * rexp (-π * τ.im) ≤ 2 / (1 - rexp (-π)) * ‖rexp (-π * τ.im)‖
<VAR>y : ℝ<VAR>hy : y ≥ 1<VAR>τ : ℂ<VAR>hτ : τ.im = y<GOAL>2 / (1 - rexp (-π * τ.im)) * rexp (-π * τ.im) ≤ 2 / (1 - rexp (-π)) * rexp (-π * τ.im)
<VAR>y : ℝ<VAR>hy : y ≥ 1<VAR>τ : ℂ<VAR>hτ : τ.im = y<GOAL>2 / (1 - rexp (-π * τ.im)) ≤ 2 / (1 - rexp (-π))
<VAR>y : ℝ<VAR>hy : y ≥ 1<VAR>τ : ℂ<VAR>hτ : τ.im = y<GOAL>π ≤ π * τ.im
<VAR>y : ℝ<VAR>hy : y ≥ 1<VAR>τ : ℂ<VAR>hτ : τ.im = y<GOAL>0 < 1 - rexp (-π * τ.im)
<VAR>y : ℝ<VAR>hy : y ≥ 1<VAR>τ : ℂ<VAR>hτ : τ.im = y<GOAL>0 < 1 - rexp (-π)
<VAR>p : ℕ<VAR>R : Type u_1<VAR>hp : Fact (Nat.Prime p)<VAR>inst✝ : CommRing R<VAR>x : 𝕎 R<VAR>n : ℕ<GOAL>(-x).coeff n = peval (wittNeg p n) ![x.coeff]
<VAR>n✝ b m d n : ℕ<VAR>IH : ∀ m < n + 1, ∀ {d : ℕ}, d ∈ (b + 2).digits m → d < b + 2<VAR>hd : d ∈ (b + 2).digits (n + 1)<GOAL>d < b + 2
<VAR>n✝ b m d n : ℕ<VAR>IH : ∀ m < n + 1, ∀ {d : ℕ}, d ∈ (b + 2).digits m → d < b + 2<VAR>hd : d ∈ (n + 1) % (b + 2) :: (b + 2).digits ((n + 1) / (b + 2))<GOAL>d < b + 2
<VAR>α : Type u_1<VAR>inst✝¹ : LinearOrder α<VAR>inst✝ : Ring α<VAR>a : α<GOAL>Odd |a| ↔ Odd a
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>s t✝ : Set X<VAR>t : Set Y<VAR>hs : IsCompact s<VAR>ht : IsCompact t<GOAL>IsCompact (s ×ˢ t)
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>s t✝ : Set X<VAR>t : Set Y<VAR>hs : ∀ (f : Ultrafilter X), s ∈ f → ∃ x ∈ s, ↑f ≤ 𝓝 x<VAR>ht : ∀ (f : Ultrafilter Y), t ∈ f → ∃ x ∈ t, ↑f ≤ 𝓝 x<GOAL>∀ (f : Ultrafilter (X × Y)), s ×ˢ t ∈ f → ∃ x ∈ s ×ˢ t, ↑f ≤ 𝓝 x
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>s t✝ : Set X<VAR>t : Set Y<VAR>hs : ∀ (f : Ultrafilter X), s ∈ f → ∃ x ∈ s, ↑f ≤ 𝓝 x<VAR>ht : ∀ (f : Ultrafilter Y), t ∈ f → ∃ x ∈ t, ↑f ≤ 𝓝 x<VAR>f : Ultrafilter (X × Y)<VAR>hfs : s ×ˢ t ∈ f<GOAL>∃ x ∈ s ×ˢ t, ↑f ≤ 𝓝 x
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>s t✝ : Set X<VAR>t : Set Y<VAR>hs : ∀ (f : Ultrafilter X), s ∈ f → ∃ x ∈ s, ↑f ≤ 𝓝 x<VAR>ht : ∀ (f : Ultrafilter Y), t ∈ f → ∃ x ∈ t, ↑f ≤ 𝓝 x<VAR>f : Ultrafilter (X × Y)<VAR>hfs : s ×ˢ t ∈ f<VAR>x : X<VAR>sx : x ∈ s<VAR>hx : map Prod.fst ↑f ≤ 𝓝 x<GOAL>∃ x ∈ s ×ˢ t, ↑f ≤ 𝓝 x
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>s t✝ : Set X<VAR>t : Set Y<VAR>hs : ∀ (f : Ultrafilter X), s ∈ f → ∃ x ∈ s, ↑f ≤ 𝓝 x<VAR>ht : ∀ (f : Ultrafilter Y), t ∈ f → ∃ x ∈ t, ↑f ≤ 𝓝 x<VAR>f : Ultrafilter (X × Y)<VAR>hfs : s ×ˢ t ∈ f<VAR>x : X<VAR>sx : x ∈ s<VAR>hx : map Prod.fst ↑f ≤ 𝓝 x<VAR>y : Y<VAR>ty : y ∈ t<VAR>hy : map Prod.snd ↑f ≤ 𝓝 y<GOAL>∃ x ∈ s ×ˢ t, ↑f ≤ 𝓝 x
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>s t✝ : Set X<VAR>t : Set Y<VAR>hs : ∀ (f : Ultrafilter X), s ∈ f → ∃ x ∈ s, ↑f ≤ 𝓝 x<VAR>ht : ∀ (f : Ultrafilter Y), t ∈ f → ∃ x ∈ t, ↑f ≤ 𝓝 x<VAR>f : Ultrafilter (X × Y)<VAR>hfs : s ×ˢ t ∈ f<VAR>x : X<VAR>sx : x ∈ s<VAR>hx : ↑f ≤ comap Prod.fst (𝓝 x)<VAR>y : Y<VAR>ty : y ∈ t<VAR>hy : ↑f ≤ comap Prod.snd (𝓝 y)<GOAL>∃ x ∈ s ×ˢ t, ↑f ≤ 𝓝 x
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>s t✝ : Set X<VAR>t : Set Y<VAR>hs : ∀ (f : Ultrafilter X), s ∈ f → ∃ x ∈ s, ↑f ≤ 𝓝 x<VAR>ht : ∀ (f : Ultrafilter Y), t ∈ f → ∃ x ∈ t, ↑f ≤ 𝓝 x<VAR>f : Ultrafilter (X × Y)<VAR>hfs : s ×ˢ t ∈ f<VAR>x : X<VAR>sx : x ∈ s<VAR>hx : ↑f ≤ comap Prod.fst (𝓝 x)<VAR>y : Y<VAR>ty : y ∈ t<VAR>hy : ↑f ≤ comap Prod.snd (𝓝 y)<GOAL>↑f ≤ 𝓝 (x, y)
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>s t✝ : Set X<VAR>t : Set Y<VAR>hs : ∀ (f : Ultrafilter X), s ∈ f → ∃ x ∈ s, ↑f ≤ 𝓝 x<VAR>ht : ∀ (f : Ultrafilter Y), t ∈ f → ∃ x ∈ t, ↑f ≤ 𝓝 x<VAR>f : Ultrafilter (X × Y)<VAR>hfs : s ×ˢ t ∈ f<VAR>x : X<VAR>sx : x ∈ s<VAR>hx : ↑f ≤ comap Prod.fst (𝓝 x)<VAR>y : Y<VAR>ty : y ∈ t<VAR>hy : ↑f ≤ comap Prod.snd (𝓝 y)<GOAL>↑f ≤ 𝓝 x ×ˢ 𝓝 y
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>G : Type u_6<VAR>k : Type u_7<VAR>R : Type u_8<VAR>inst✝¹ : Fintype ι<VAR>inst✝ : OrderedCommMonoid M<VAR>f : ι → M<VAR>hf : f ≤ 1<GOAL>(∀ i ∈ Finset.univ, f i = 1) ↔ f = 1
<VAR>a b c d m n✝ k : ℕ<VAR>p q : ℕ → Prop<VAR>n : ℕ<VAR>motive : (m : ℕ) → n ≤ m → Sort u_1<VAR>refl : motive n ⋯<VAR>le_succ_of_le : ⦃k : ℕ⦄ → (h : n ≤ k) → motive k h → motive (k + 1) ⋯<VAR>h1 : n ≤ m<VAR>h2 : n ≤ m + 1<GOAL>leRec refl le_succ_of_le h2 = le_succ_of_le h1 (leRec refl le_succ_of_le h1)
<VAR>θ : Angle<GOAL>θ.cos ^ 2 + θ.sin ^ 2 = 1
<VAR>x✝ : ℝ<GOAL>(↑x✝).cos ^ 2 + (↑x✝).sin ^ 2 = 1
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : LinearOrderedField α<VAR>a b c d : α<VAR>n : ℤ<GOAL>0 < a / b ↔ 0 < a ∧ 0 < b ∨ a < 0 ∧ b < 0
<VAR>R : Type u_1<VAR>M M₁ M₂ M₃ : Type u<VAR>M' : Type v<VAR>inst✝¹¹ : Ring R<VAR>inst✝¹⁰ : AddCommGroup M<VAR>inst✝⁹ : AddCommGroup M₁<VAR>inst✝⁸ : AddCommGroup M₂<VAR>inst✝⁷ : AddCommGroup M₃<VAR>inst✝⁶ : AddCommGroup M'<VAR>inst✝⁵ : Module R M<VAR>inst✝⁴ : Module R M₁<VAR>inst✝³ : Module R M₂<VAR>inst✝² : Module R M₃<VAR>inst✝¹ : Module R M'<VAR>inst✝ : HasRankNullity.{u, u_1} R<GOAL>Nontrivial R
<VAR>R : Type u_1<VAR>M M₁ M₂ M₃ : Type u<VAR>M' : Type v<VAR>inst✝¹¹ : Ring R<VAR>inst✝¹⁰ : AddCommGroup M<VAR>inst✝⁹ : AddCommGroup M₁<VAR>inst✝⁸ : AddCommGroup M₂<VAR>inst✝⁷ : AddCommGroup M₃<VAR>inst✝⁶ : AddCommGroup M'<VAR>inst✝⁵ : Module R M<VAR>inst✝⁴ : Module R M₁<VAR>inst✝³ : Module R M₂<VAR>inst✝² : Module R M₃<VAR>inst✝¹ : Module R M'<VAR>inst✝ : HasRankNullity.{u, u_1} R<VAR>H : Subsingleton R<GOAL>False
<VAR>R : Type u_1<VAR>M M₁ M₂ M₃ : Type u<VAR>M' : Type v<VAR>inst✝¹¹ : Ring R<VAR>inst✝¹⁰ : AddCommGroup M<VAR>inst✝⁹ : AddCommGroup M₁<VAR>inst✝⁸ : AddCommGroup M₂<VAR>inst✝⁷ : AddCommGroup M₃<VAR>inst✝⁶ : AddCommGroup M'<VAR>inst✝⁵ : Module R M<VAR>inst✝⁴ : Module R M₁<VAR>inst✝³ : Module R M₂<VAR>inst✝² : Module R M₃<VAR>inst✝¹ : Module R M'<VAR>inst✝ : HasRankNullity.{u, u_1} R<VAR>H : Subsingleton R<VAR>this : Module.rank R (PUnit.{u + 1} ⧸ ⊥) + Module.rank R ↥⊥ = Module.rank R PUnit.{u + 1}<GOAL>False
<VAR>α : Type u_1<VAR>inst✝ : Group α<VAR>s : Subgroup α<VAR>g : α<GOAL>Quotient.out' ↑g = g * ↑⟨g⁻¹ * Quotient.out' ↑g, ⋯⟩
<VAR>Ω : Type u_1<VAR>inst✝⁶ : MeasureSpace Ω<VAR>inst✝⁵ : IsProbabilityMeasure ℙ<VAR>E : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : CompleteSpace E<VAR>inst✝¹ : MeasurableSpace E<VAR>inst✝ : BorelSpace E<VAR>X : ℕ → Ω → E<VAR>hint : Integrable (X 0) ℙ<VAR>h' : StronglyMeasurable (X 0)<VAR>hindep : Pairwise fun i j => IndepFun (X i) (X j) ℙ<VAR>hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) ℙ ℙ<VAR>s : Set E := Set.range (X 0) ∪ {0}<VAR>zero_s : 0 ∈ s<GOAL>∀ᵐ (ω : Ω), Tendsto (fun n => (↑n)⁻¹ • ∑ i ∈ Finset.range n, X i ω) atTop (𝓝 (∫ (a : Ω), X 0 a))
<VAR>Ω : Type u_1<VAR>inst✝⁶ : MeasureSpace Ω<VAR>inst✝⁵ : IsProbabilityMeasure ℙ<VAR>E : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : CompleteSpace E<VAR>inst✝¹ : MeasurableSpace E<VAR>inst✝ : BorelSpace E<VAR>X : ℕ → Ω → E<VAR>hint : Integrable (X 0) ℙ<VAR>h' : StronglyMeasurable (X 0)<VAR>hindep : Pairwise fun i j => IndepFun (X i) (X j) ℙ<VAR>hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) ℙ ℙ<VAR>s : Set E := Set.range (X 0) ∪ {0}<VAR>zero_s : 0 ∈ s<VAR>this : SeparableSpace ↑s<GOAL>∀ᵐ (ω : Ω), Tendsto (fun n => (↑n)⁻¹ • ∑ i ∈ Finset.range n, X i ω) atTop (𝓝 (∫ (a : Ω), X 0 a))
<VAR>Ω : Type u_1<VAR>inst✝⁶ : MeasureSpace Ω<VAR>inst✝⁵ : IsProbabilityMeasure ℙ<VAR>E : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : CompleteSpace E<VAR>inst✝¹ : MeasurableSpace E<VAR>inst✝ : BorelSpace E<VAR>X : ℕ → Ω → E<VAR>hint : Integrable (X 0) ℙ<VAR>h' : StronglyMeasurable (X 0)<VAR>hindep : Pairwise fun i j => IndepFun (X i) (X j) ℙ<VAR>hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) ℙ ℙ<VAR>s : Set E := Set.range (X 0) ∪ {0}<VAR>zero_s : 0 ∈ s<VAR>this✝ : SeparableSpace ↑s<VAR>this : Nonempty ↑s<VAR>φ : ℕ → SimpleFunc E E := SimpleFunc.nearestPt fun k => Nat.casesOn k 0 (Subtype.val ∘ denseSeq ↑s)<VAR>Y : ℕ → ℕ → Ω → E := fun k i => ↑(φ k) ∘ X i<GOAL>∀ᵐ (ω : Ω), Tendsto (fun n => (↑n)⁻¹ • ∑ i ∈ Finset.range n, X i ω) atTop (𝓝 (∫ (a : Ω), X 0 a))
<VAR>Ω : Type u_1<VAR>inst✝⁶ : MeasureSpace Ω<VAR>inst✝⁵ : IsProbabilityMeasure ℙ<VAR>E : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : CompleteSpace E<VAR>inst✝¹ : MeasurableSpace E<VAR>inst✝ : BorelSpace E<VAR>X : ℕ → Ω → E<VAR>hint : Integrable (X 0) ℙ<VAR>h' : StronglyMeasurable (X 0)<VAR>hindep : Pairwise fun i j => IndepFun (X i) (X j) ℙ<VAR>hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) ℙ ℙ<VAR>s : Set E := Set.range (X 0) ∪ {0}<VAR>zero_s : 0 ∈ s<VAR>this✝ : SeparableSpace ↑s<VAR>this : Nonempty ↑s<VAR>φ : ℕ → SimpleFunc E E := SimpleFunc.nearestPt fun k => Nat.casesOn k 0 (Subtype.val ∘ denseSeq ↑s)<VAR>Y : ℕ → ℕ → Ω → E := fun k i => ↑(φ k) ∘ X i<VAR>A : ∀ᵐ (ω : Ω), ∀ (k : ℕ), Tendsto (fun n => (↑n)⁻¹ • ∑ i ∈ Finset.range n, Y k i ω) atTop (𝓝 (∫ (a : Ω), Y k 0 a))<GOAL>∀ᵐ (ω : Ω), Tendsto (fun n => (↑n)⁻¹ • ∑ i ∈ Finset.range n, X i ω) atTop (𝓝 (∫ (a : Ω), X 0 a))
<VAR>Ω : Type u_1<VAR>inst✝⁶ : MeasureSpace Ω<VAR>inst✝⁵ : IsProbabilityMeasure ℙ<VAR>E : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : CompleteSpace E<VAR>inst✝¹ : MeasurableSpace E<VAR>inst✝ : BorelSpace E<VAR>X : ℕ → Ω → E<VAR>hint : Integrable (X 0) ℙ<VAR>h' : StronglyMeasurable (X 0)<VAR>hindep : Pairwise fun i j => IndepFun (X i) (X j) ℙ<VAR>hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) ℙ ℙ<VAR>s : Set E := Set.range (X 0) ∪ {0}<VAR>zero_s : 0 ∈ s<VAR>this✝ : SeparableSpace ↑s<VAR>this : Nonempty ↑s<VAR>φ : ℕ → SimpleFunc E E := SimpleFunc.nearestPt fun k => Nat.casesOn k 0 (Subtype.val ∘ denseSeq ↑s)<VAR>Y : ℕ → ℕ → Ω → E := fun k i => ↑(φ k) ∘ X i<VAR>A : ∀ᵐ (ω : Ω), ∀ (k : ℕ), Tendsto (fun n => (↑n)⁻¹ • ∑ i ∈ Finset.range n, Y k i ω) atTop (𝓝 (∫ (a : Ω), Y k 0 a))<VAR>B : ∀ᵐ (ω : Ω), ∀ (k : ℕ), Tendsto (fun n => (∑ i ∈ Finset.range n, ‖(X i - Y k i) ω‖) / ↑n) atTop (𝓝 (∫ (a : Ω), (fun ω => ‖(X 0 - Y k 0) ω‖) a))<GOAL>∀ᵐ (ω : Ω), Tendsto (fun n => (↑n)⁻¹ • ∑ i ∈ Finset.range n, X i ω) atTop (𝓝 (∫ (a : Ω), X 0 a))
<VAR>Ω : Type u_1<VAR>inst✝⁶ : MeasureSpace Ω<VAR>inst✝⁵ : IsProbabilityMeasure ℙ<VAR>E : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : CompleteSpace E<VAR>inst✝¹ : MeasurableSpace E<VAR>inst✝ : BorelSpace E<VAR>X : ℕ → Ω → E<VAR>hint : Integrable (X 0) ℙ<VAR>h' : StronglyMeasurable (X 0)<VAR>hindep : Pairwise fun i j => IndepFun (X i) (X j) ℙ<VAR>hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) ℙ ℙ<VAR>s : Set E := Set.range (X 0) ∪ {0}<VAR>zero_s : 0 ∈ s<VAR>this✝ : SeparableSpace ↑s<VAR>this : Nonempty ↑s<VAR>φ : ℕ → SimpleFunc E E := SimpleFunc.nearestPt fun k => Nat.casesOn k 0 (Subtype.val ∘ denseSeq ↑s)<VAR>Y : ℕ → ℕ → Ω → E := fun k i => ↑(φ k) ∘ X i<VAR>A : ∀ᵐ (ω : Ω), ∀ (k : ℕ), Tendsto (fun n => (↑n)⁻¹ • ∑ i ∈ Finset.range n, Y k i ω) atTop (𝓝 (∫ (a : Ω), Y k 0 a))<VAR>B : ∀ᵐ (ω : Ω), ∀ (k : ℕ), Tendsto (fun n => (∑ i ∈ Finset.range n, ‖(X i - Y k i) ω‖) / ↑n) atTop (𝓝 (∫ (a : Ω), (fun ω => ‖(X 0 - Y k 0) ω‖) a))<VAR>ω : Ω<VAR>hω : ∀ (k : ℕ), Tendsto (fun n => (↑n)⁻¹ • ∑ i ∈ Finset.range n, Y k i ω) atTop (𝓝 (∫ (a : Ω), Y k 0 a))<VAR>h'ω : ∀ (k : ℕ), Tendsto (fun n => (∑ i ∈ Finset.range n, ‖(X i - Y k i) ω‖) / ↑n) atTop (𝓝 (∫ (a : Ω), ‖(X 0 - Y k 0) a‖))<GOAL>Tendsto (fun n => (↑n)⁻¹ • ∑ i ∈ Finset.range n, X i ω) atTop (𝓝 (∫ (a : Ω), X 0 a))
<VAR>Ω : Type u_1<VAR>inst✝⁶ : MeasureSpace Ω<VAR>inst✝⁵ : IsProbabilityMeasure ℙ<VAR>E : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : CompleteSpace E<VAR>inst✝¹ : MeasurableSpace E<VAR>inst✝ : BorelSpace E<VAR>X : ℕ → Ω → E<VAR>hint : Integrable (X 0) ℙ<VAR>h' : StronglyMeasurable (X 0)<VAR>hindep : Pairwise fun i j => IndepFun (X i) (X j) ℙ<VAR>hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) ℙ ℙ<VAR>s : Set E := Set.range (X 0) ∪ {0}<VAR>zero_s : 0 ∈ s<VAR>this✝ : SeparableSpace ↑s<VAR>this : Nonempty ↑s<VAR>φ : ℕ → SimpleFunc E E := SimpleFunc.nearestPt fun k => Nat.casesOn k 0 (Subtype.val ∘ denseSeq ↑s)<VAR>Y : ℕ → ℕ → Ω → E := fun k i => ↑(φ k) ∘ X i<VAR>A : ∀ᵐ (ω : Ω), ∀ (k : ℕ), Tendsto (fun n => (↑n)⁻¹ • ∑ i ∈ Finset.range n, Y k i ω) atTop (𝓝 (∫ (a : Ω), Y k 0 a))<VAR>B : ∀ᵐ (ω : Ω), ∀ (k : ℕ), Tendsto (fun n => (∑ i ∈ Finset.range n, ‖(X i - Y k i) ω‖) / ↑n) atTop (𝓝 (∫ (a : Ω), (fun ω => ‖(X 0 - Y k 0) ω‖) a))<VAR>ω : Ω<VAR>hω : ∀ (k : ℕ), Tendsto (fun n => (↑n)⁻¹ • ∑ i ∈ Finset.range n, Y k i ω) atTop (𝓝 (∫ (a : Ω), Y k 0 a))<VAR>h'ω : ∀ (k : ℕ), Tendsto (fun n => (∑ i ∈ Finset.range n, ‖(X i - Y k i) ω‖) / ↑n) atTop (𝓝 (∫ (a : Ω), ‖(X 0 - Y k 0) a‖))<GOAL>(∀ a' < 0, ∀ᶠ (b : ℕ) in atTop, a' < ‖(↑b)⁻¹ • ∑ i ∈ Finset.range b, X i ω - ∫ (a : Ω), X 0 a‖) ∧ ∀ a' > 0, ∀ᶠ (b : ℕ) in atTop, ‖(↑b)⁻¹ • ∑ i ∈ Finset.range b, X i ω - ∫ (a : Ω), X 0 a‖ < a'
<VAR>Ω : Type u_1<VAR>inst✝⁶ : MeasureSpace Ω<VAR>inst✝⁵ : IsProbabilityMeasure ℙ<VAR>E : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : CompleteSpace E<VAR>inst✝¹ : MeasurableSpace E<VAR>inst✝ : BorelSpace E<VAR>X : ℕ → Ω → E<VAR>hint : Integrable (X 0) ℙ<VAR>h' : StronglyMeasurable (X 0)<VAR>hindep : Pairwise fun i j => IndepFun (X i) (X j) ℙ<VAR>hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) ℙ ℙ<VAR>s : Set E := Set.range (X 0) ∪ {0}<VAR>zero_s : 0 ∈ s<VAR>this✝ : SeparableSpace ↑s<VAR>this : Nonempty ↑s<VAR>φ : ℕ → SimpleFunc E E := SimpleFunc.nearestPt fun k => Nat.casesOn k 0 (Subtype.val ∘ denseSeq ↑s)<VAR>Y : ℕ → ℕ → Ω → E := fun k i => ↑(φ k) ∘ X i<VAR>A : ∀ᵐ (ω : Ω), ∀ (k : ℕ), Tendsto (fun n => (↑n)⁻¹ • ∑ i ∈ Finset.range n, Y k i ω) atTop (𝓝 (∫ (a : Ω), Y k 0 a))<VAR>B : ∀ᵐ (ω : Ω), ∀ (k : ℕ), Tendsto (fun n => (∑ i ∈ Finset.range n, ‖(X i - Y k i) ω‖) / ↑n) atTop (𝓝 (∫ (a : Ω), (fun ω => ‖(X 0 - Y k 0) ω‖) a))<VAR>ω : Ω<VAR>hω : ∀ (k : ℕ), Tendsto (fun n => (↑n)⁻¹ • ∑ i ∈ Finset.range n, Y k i ω) atTop (𝓝 (∫ (a : Ω), Y k 0 a))<VAR>h'ω : ∀ (k : ℕ), Tendsto (fun n => (∑ i ∈ Finset.range n, ‖(X i - Y k i) ω‖) / ↑n) atTop (𝓝 (∫ (a : Ω), ‖(X 0 - Y k 0) a‖))<GOAL>∀ a' > 0, ∀ᶠ (b : ℕ) in atTop, ‖(↑b)⁻¹ • ∑ i ∈ Finset.range b, X i ω - ∫ (a : Ω), X 0 a‖ < a'
<VAR>Ω : Type u_1<VAR>inst✝⁶ : MeasureSpace Ω<VAR>inst✝⁵ : IsProbabilityMeasure ℙ<VAR>E : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : CompleteSpace E<VAR>inst✝¹ : MeasurableSpace E<VAR>inst✝ : BorelSpace E<VAR>X : ℕ → Ω → E<VAR>hint : Integrable (X 0) ℙ<VAR>h' : StronglyMeasurable (X 0)<VAR>hindep : Pairwise fun i j => IndepFun (X i) (X j) ℙ<VAR>hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) ℙ ℙ<VAR>s : Set E := Set.range (X 0) ∪ {0}<VAR>zero_s : 0 ∈ s<VAR>this✝ : SeparableSpace ↑s<VAR>this : Nonempty ↑s<VAR>φ : ℕ → SimpleFunc E E := SimpleFunc.nearestPt fun k => Nat.casesOn k 0 (Subtype.val ∘ denseSeq ↑s)<VAR>Y : ℕ → ℕ → Ω → E := fun k i => ↑(φ k) ∘ X i<VAR>A : ∀ᵐ (ω : Ω), ∀ (k : ℕ), Tendsto (fun n => (↑n)⁻¹ • ∑ i ∈ Finset.range n, Y k i ω) atTop (𝓝 (∫ (a : Ω), Y k 0 a))<VAR>B : ∀ᵐ (ω : Ω), ∀ (k : ℕ), Tendsto (fun n => (∑ i ∈ Finset.range n, ‖(X i - Y k i) ω‖) / ↑n) atTop (𝓝 (∫ (a : Ω), (fun ω => ‖(X 0 - Y k 0) ω‖) a))<VAR>ω : Ω<VAR>hω : ∀ (k : ℕ), Tendsto (fun n => (↑n)⁻¹ • ∑ i ∈ Finset.range n, Y k i ω) atTop (𝓝 (∫ (a : Ω), Y k 0 a))<VAR>h'ω : ∀ (k : ℕ), Tendsto (fun n => (∑ i ∈ Finset.range n, ‖(X i - Y k i) ω‖) / ↑n) atTop (𝓝 (∫ (a : Ω), ‖(X 0 - Y k 0) a‖))<VAR>ε : ℝ<VAR>εpos : 0 < ε<VAR>δ : ℝ<VAR>δpos : 0 < δ<VAR>hδ : δ + δ + δ < ε<GOAL>∀ᶠ (b : ℕ) in atTop, ‖(↑b)⁻¹ • ∑ i ∈ Finset.range b, X i ω - ∫ (a : Ω), X 0 a‖ < ε
<VAR>Ω : Type u_1<VAR>inst✝⁶ : MeasureSpace Ω<VAR>inst✝⁵ : IsProbabilityMeasure ℙ<VAR>E : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : CompleteSpace E<VAR>inst✝¹ : MeasurableSpace E<VAR>inst✝ : BorelSpace E<VAR>X : ℕ → Ω → E<VAR>hint : Integrable (X 0) ℙ<VAR>h' : StronglyMeasurable (X 0)<VAR>hindep : Pairwise fun i j => IndepFun (X i) (X j) ℙ<VAR>hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) ℙ ℙ<VAR>s : Set E := Set.range (X 0) ∪ {0}<VAR>zero_s : 0 ∈ s<VAR>this✝ : SeparableSpace ↑s<VAR>this : Nonempty ↑s<VAR>φ : ℕ → SimpleFunc E E := SimpleFunc.nearestPt fun k => Nat.casesOn k 0 (Subtype.val ∘ denseSeq ↑s)<VAR>Y : ℕ → ℕ → Ω → E := fun k i => ↑(φ k) ∘ X i<VAR>A : ∀ᵐ (ω : Ω), ∀ (k : ℕ), Tendsto (fun n => (↑n)⁻¹ • ∑ i ∈ Finset.range n, Y k i ω) atTop (𝓝 (∫ (a : Ω), Y k 0 a))<VAR>B : ∀ᵐ (ω : Ω), ∀ (k : ℕ), Tendsto (fun n => (∑ i ∈ Finset.range n, ‖(X i - Y k i) ω‖) / ↑n) atTop (𝓝 (∫ (a : Ω), (fun ω => ‖(X 0 - Y k 0) ω‖) a))<VAR>ω : Ω<VAR>hω : ∀ (k : ℕ), Tendsto (fun n => (↑n)⁻¹ • ∑ i ∈ Finset.range n, Y k i ω) atTop (𝓝 (∫ (a : Ω), Y k 0 a))<VAR>h'ω : ∀ (k : ℕ), Tendsto (fun n => (∑ i ∈ Finset.range n, ‖(X i - Y k i) ω‖) / ↑n) atTop (𝓝 (∫ (a : Ω), ‖(X 0 - Y k 0) a‖))<VAR>ε : ℝ<VAR>εpos : 0 < ε<VAR>δ : ℝ<VAR>δpos : 0 < δ<VAR>hδ : δ + δ + δ < ε<VAR>k : ℕ<VAR>hk : ∫ (ω : Ω), ‖(X 0 - Y k 0) ω‖ < δ<GOAL>∀ᶠ (b : ℕ) in atTop, ‖(↑b)⁻¹ • ∑ i ∈ Finset.range b, X i ω - ∫ (a : Ω), X 0 a‖ < ε
<VAR>Ω : Type u_1<VAR>inst✝⁶ : MeasureSpace Ω<VAR>inst✝⁵ : IsProbabilityMeasure ℙ<VAR>E : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : CompleteSpace E<VAR>inst✝¹ : MeasurableSpace E<VAR>inst✝ : BorelSpace E<VAR>X : ℕ → Ω → E<VAR>hint : Integrable (X 0) ℙ<VAR>h' : StronglyMeasurable (X 0)<VAR>hindep : Pairwise fun i j => IndepFun (X i) (X j) ℙ<VAR>hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) ℙ ℙ<VAR>s : Set E := Set.range (X 0) ∪ {0}<VAR>zero_s : 0 ∈ s<VAR>this✝¹ : SeparableSpace ↑s<VAR>this✝ : Nonempty ↑s<VAR>φ : ℕ → SimpleFunc E E := SimpleFunc.nearestPt fun k => Nat.casesOn k 0 (Subtype.val ∘ denseSeq ↑s)<VAR>Y : ℕ → ℕ → Ω → E := fun k i => ↑(φ k) ∘ X i<VAR>A : ∀ᵐ (ω : Ω), ∀ (k : ℕ), Tendsto (fun n => (↑n)⁻¹ • ∑ i ∈ Finset.range n, Y k i ω) atTop (𝓝 (∫ (a : Ω), Y k 0 a))<VAR>B : ∀ᵐ (ω : Ω), ∀ (k : ℕ), Tendsto (fun n => (∑ i ∈ Finset.range n, ‖(X i - Y k i) ω‖) / ↑n) atTop (𝓝 (∫ (a : Ω), (fun ω => ‖(X 0 - Y k 0) ω‖) a))<VAR>ω : Ω<VAR>hω : ∀ (k : ℕ), Tendsto (fun n => (↑n)⁻¹ • ∑ i ∈ Finset.range n, Y k i ω) atTop (𝓝 (∫ (a : Ω), Y k 0 a))<VAR>h'ω : ∀ (k : ℕ), Tendsto (fun n => (∑ i ∈ Finset.range n, ‖(X i - Y k i) ω‖) / ↑n) atTop (𝓝 (∫ (a : Ω), ‖(X 0 - Y k 0) a‖))<VAR>ε : ℝ<VAR>εpos : 0 < ε<VAR>δ : ℝ<VAR>δpos : 0 < δ<VAR>hδ : δ + δ + δ < ε<VAR>k : ℕ<VAR>hk : ∫ (ω : Ω), ‖(X 0 - Y k 0) ω‖ < δ<VAR>this : ‖(∫ (a : Ω), Y k 0 a) - ∫ (a : Ω), X 0 a‖ < δ<GOAL>∀ᶠ (b : ℕ) in atTop, ‖(↑b)⁻¹ • ∑ i ∈ Finset.range b, X i ω - ∫ (a : Ω), X 0 a‖ < ε
<VAR>Ω : Type u_1<VAR>inst✝⁶ : MeasureSpace Ω<VAR>inst✝⁵ : IsProbabilityMeasure ℙ<VAR>E : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : CompleteSpace E<VAR>inst✝¹ : MeasurableSpace E<VAR>inst✝ : BorelSpace E<VAR>X : ℕ → Ω → E<VAR>hint : Integrable (X 0) ℙ<VAR>h' : StronglyMeasurable (X 0)<VAR>hindep : Pairwise fun i j => IndepFun (X i) (X j) ℙ<VAR>hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) ℙ ℙ<VAR>s : Set E := Set.range (X 0) ∪ {0}<VAR>zero_s : 0 ∈ s<VAR>this✝¹ : SeparableSpace ↑s<VAR>this✝ : Nonempty ↑s<VAR>φ : ℕ → SimpleFunc E E := SimpleFunc.nearestPt fun k => Nat.casesOn k 0 (Subtype.val ∘ denseSeq ↑s)<VAR>Y : ℕ → ℕ → Ω → E := fun k i => ↑(φ k) ∘ X i<VAR>A : ∀ᵐ (ω : Ω), ∀ (k : ℕ), Tendsto (fun n => (↑n)⁻¹ • ∑ i ∈ Finset.range n, Y k i ω) atTop (𝓝 (∫ (a : Ω), Y k 0 a))<VAR>B : ∀ᵐ (ω : Ω), ∀ (k : ℕ), Tendsto (fun n => (∑ i ∈ Finset.range n, ‖(X i - Y k i) ω‖) / ↑n) atTop (𝓝 (∫ (a : Ω), (fun ω => ‖(X 0 - Y k 0) ω‖) a))<VAR>ω : Ω<VAR>hω : ∀ (k : ℕ), Tendsto (fun n => (↑n)⁻¹ • ∑ i ∈ Finset.range n, Y k i ω) atTop (𝓝 (∫ (a : Ω), Y k 0 a))<VAR>h'ω : ∀ (k : ℕ), Tendsto (fun n => (∑ i ∈ Finset.range n, ‖(X i - Y k i) ω‖) / ↑n) atTop (𝓝 (∫ (a : Ω), ‖(X 0 - Y k 0) a‖))<VAR>ε : ℝ<VAR>εpos : 0 < ε<VAR>δ : ℝ<VAR>δpos : 0 < δ<VAR>hδ : δ + δ + δ < ε<VAR>k : ℕ<VAR>hk : ∫ (ω : Ω), ‖(X 0 - Y k 0) ω‖ < δ<VAR>this : ‖(∫ (a : Ω), Y k 0 a) - ∫ (a : Ω), X 0 a‖ < δ<VAR>I : ∀ᶠ (n : ℕ) in atTop, (∑ i ∈ Finset.range n, ‖(X i - Y k i) ω‖) / ↑n < δ<GOAL>∀ᶠ (b : ℕ) in atTop, ‖(↑b)⁻¹ • ∑ i ∈ Finset.range b, X i ω - ∫ (a : Ω), X 0 a‖ < ε