ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>γ : Type u_4<VAR>mγ : MeasurableSpace γ<VAR>s : Set (β × γ)<VAR>κ : Kernel α β<VAR>inst✝¹ : IsSFiniteKernel κ<VAR>η : Kernel (α × β) γ<VAR>inst✝ : IsSFiniteKernel η<VAR>a : α<VAR>hs : MeasurableSet s<GOAL>((κ ⊗ₖ η) a) s = ∑' (n : ℕ) (m : ℕ), ((κ.seq n ⊗ₖ η.seq m) a) s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>γ : Type u_4<VAR>mγ : MeasurableSpace γ<VAR>s : Set (β × γ)<VAR>κ : Kernel α β<VAR>inst✝¹ : IsSFiniteKernel κ<VAR>η : Kernel (α × β) γ<VAR>inst✝ : IsSFiniteKernel η<VAR>a : α<VAR>hs : MeasurableSet s<GOAL>κ.compProdFun η a s = ∑' (n : ℕ) (m : ℕ), (κ.seq n).compProdFun (η.seq m) a s
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝ : Category.{v₂, u₂} D<VAR>F : C ⥤ D<VAR>G : D ⥤ C<VAR>adj : F ⊣ G<VAR>X' X : C<VAR>Y Y' : D<VAR>x✝ : C<GOAL>F.map (adj.unit.app x✝) ≫ adj.counit.app (F.obj x✝) = 𝟙 (F.obj x✝)
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝ : Category.{v₂, u₂} D<VAR>F : C ⥤ D<VAR>G : D ⥤ C<VAR>adj : F ⊣ G<VAR>X' X : C<VAR>Y Y' : D<VAR>x✝ : C<GOAL>adj.unit.app x✝ = adj.unit.app x✝ ≫ G.map (𝟙 (F.obj x✝))
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>f : ℝ → E<VAR>s : Set ℝ<VAR>x₀ x : ℝ<VAR>k : ℕ<VAR>hk : taylorWithinEval f k s x₀ x = ∑ k ∈ Finset.range (k + 1), ((↑k !)⁻¹ * (x - x₀) ^ k) • iteratedDerivWithin k f s x₀<GOAL>taylorWithinEval f (k + 1) s x₀ x = ∑ k ∈ Finset.range (k + 1 + 1), ((↑k !)⁻¹ * (x - x₀) ^ k) • iteratedDerivWithin k f s x₀
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>f : ℝ → E<VAR>s : Set ℝ<VAR>x₀ x : ℝ<VAR>k : ℕ<VAR>hk : taylorWithinEval f k s x₀ x = ∑ k ∈ Finset.range (k + 1), ((↑k !)⁻¹ * (x - x₀) ^ k) • iteratedDerivWithin k f s x₀<GOAL>∑ k ∈ Finset.range (k + 1), ((↑k !)⁻¹ * (x - x₀) ^ k) • iteratedDerivWithin k f s x₀ + (((↑k + 1) * ↑k !)⁻¹ * (x - x₀) ^ (k + 1)) • iteratedDerivWithin (k + 1) f s x₀ = ∑ x_1 ∈ Finset.range (k + 1), ((↑x_1 !)⁻¹ * (x - x₀) ^ x_1) • iteratedDerivWithin x_1 f s x₀ + ((↑(k + 1)!)⁻¹ * (x - x₀) ^ (k + 1)) • iteratedDerivWithin (k + 1) f s x₀
<VAR>x : EReal<VAR>h : 0 < x<GOAL>⊤ * x = ⊤
<VAR>x : EReal<VAR>h : 0 < x<GOAL>x * ⊤ = ⊤
<VAR>R✝ : Type uR<VAR>inst✝⁴ : Semiring R✝<VAR>S : Type uS<VAR>inst✝³ : CommSemiring S<VAR>T : Type uT<VAR>A : Type uA<VAR>inst✝² : Semiring A<VAR>inst✝¹ : Algebra S A<VAR>r✝ : R✝ → R✝ → Prop<VAR>R : Type uR<VAR>inst✝ : Ring R<VAR>r : R → R → Prop<VAR>a : R<GOAL>RingQuot.neg r { toQuot := Quot.mk (Rel r) a } = { toQuot := Quot.mk (Rel r) (-a) }
<VAR>R✝ : Type uR<VAR>inst✝⁴ : Semiring R✝<VAR>S : Type uS<VAR>inst✝³ : CommSemiring S<VAR>T : Type uT<VAR>A : Type uA<VAR>inst✝² : Semiring A<VAR>inst✝¹ : Algebra S A<VAR>r✝ : R✝ → R✝ → Prop<VAR>R : Type uR<VAR>inst✝ : Ring R<VAR>r : R → R → Prop<VAR>a : R<GOAL>(match { toQuot := Quot.mk (Rel r) a } with | { toQuot := a } => { toQuot := Quot.map (fun a => -a) ⋯ a }) = { toQuot := Quot.mk (Rel r) (-a) }
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ ν ν' : Measure α<VAR>inst✝² : SigmaFinite μ<VAR>inst✝¹ : SigmaFinite ν<VAR>inst✝ : SigmaFinite ν'<VAR>hμν' : μ ⟂ₘ ν'<VAR>hνν' : ν ⟂ₘ ν'<GOAL>μ.rnDeriv (ν + ν') =ᶠ[ae ν] μ.rnDeriv ν
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ ν ν' : Measure α<VAR>inst✝² : SigmaFinite μ<VAR>inst✝¹ : SigmaFinite ν<VAR>inst✝ : SigmaFinite ν'<VAR>hμν' : μ ⟂ₘ ν'<VAR>hνν' : ν ⟂ₘ ν'<VAR>h_ac : ν ≪ ν + ν'<GOAL>μ.rnDeriv (ν + ν') =ᶠ[ae ν] μ.rnDeriv ν
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ ν ν' : Measure α<VAR>inst✝² : SigmaFinite μ<VAR>inst✝¹ : SigmaFinite ν<VAR>inst✝ : SigmaFinite ν'<VAR>hμν' : μ ⟂ₘ ν'<VAR>hνν' : ν ⟂ₘ ν'<VAR>h_ac : ν ≪ ν + ν'<GOAL>(μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)).rnDeriv (ν + ν') =ᶠ[ae ν] (μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)).rnDeriv ν
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ ν ν' : Measure α<VAR>inst✝² : SigmaFinite μ<VAR>inst✝¹ : SigmaFinite ν<VAR>inst✝ : SigmaFinite ν'<VAR>hμν' : μ ⟂ₘ ν'<VAR>hνν' : ν ⟂ₘ ν'<VAR>h_ac : ν ≪ ν + ν'<VAR>h₁ : (μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)).rnDeriv (ν + ν') =ᶠ[ae (ν + ν')] (μ.singularPart ν).rnDeriv (ν + ν') + (ν.withDensity (μ.rnDeriv ν)).rnDeriv (ν + ν')<GOAL>(μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)).rnDeriv (ν + ν') =ᶠ[ae ν] (μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)).rnDeriv ν
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ ν ν' : Measure α<VAR>inst✝² : SigmaFinite μ<VAR>inst✝¹ : SigmaFinite ν<VAR>inst✝ : SigmaFinite ν'<VAR>hμν' : μ ⟂ₘ ν'<VAR>hνν' : ν ⟂ₘ ν'<VAR>h_ac : ν ≪ ν + ν'<VAR>h₁ : (μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)).rnDeriv (ν + ν') =ᶠ[ae (ν + ν')] (μ.singularPart ν).rnDeriv (ν + ν') + (ν.withDensity (μ.rnDeriv ν)).rnDeriv (ν + ν')<VAR>h₂ : (μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)).rnDeriv ν =ᶠ[ae ν] (μ.singularPart ν).rnDeriv ν + (ν.withDensity (μ.rnDeriv ν)).rnDeriv ν<GOAL>(μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)).rnDeriv (ν + ν') =ᶠ[ae ν] (μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)).rnDeriv ν
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ ν ν' : Measure α<VAR>inst✝² : SigmaFinite μ<VAR>inst✝¹ : SigmaFinite ν<VAR>inst✝ : SigmaFinite ν'<VAR>hμν' : μ ⟂ₘ ν'<VAR>hνν' : ν ⟂ₘ ν'<VAR>h_ac : ν ≪ ν + ν'<VAR>h₁ : (μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)).rnDeriv (ν + ν') =ᶠ[ae (ν + ν')] (μ.singularPart ν).rnDeriv (ν + ν') + (ν.withDensity (μ.rnDeriv ν)).rnDeriv (ν + ν')<VAR>h₂ : (μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)).rnDeriv ν =ᶠ[ae ν] (μ.singularPart ν).rnDeriv ν + (ν.withDensity (μ.rnDeriv ν)).rnDeriv ν<GOAL>(μ.singularPart ν).rnDeriv (ν + ν') + (ν.withDensity (μ.rnDeriv ν)).rnDeriv (ν + ν') =ᶠ[ae ν] (μ.singularPart ν).rnDeriv ν + (ν.withDensity (μ.rnDeriv ν)).rnDeriv ν
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ ν ν' : Measure α<VAR>inst✝² : SigmaFinite μ<VAR>inst✝¹ : SigmaFinite ν<VAR>inst✝ : SigmaFinite ν'<VAR>hμν' : μ ⟂ₘ ν'<VAR>hνν' : ν ⟂ₘ ν'<VAR>h_ac : ν ≪ ν + ν'<VAR>h₁ : (μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)).rnDeriv (ν + ν') =ᶠ[ae (ν + ν')] (μ.singularPart ν).rnDeriv (ν + ν') + (ν.withDensity (μ.rnDeriv ν)).rnDeriv (ν + ν')<VAR>h₂ : (μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)).rnDeriv ν =ᶠ[ae ν] (μ.singularPart ν).rnDeriv ν + (ν.withDensity (μ.rnDeriv ν)).rnDeriv ν<VAR>h₃ : (ν.withDensity (μ.rnDeriv ν)).rnDeriv (ν + ν') =ᶠ[ae ν] (ν.withDensity (μ.rnDeriv ν)).rnDeriv ν<GOAL>(μ.singularPart ν).rnDeriv (ν + ν') + (ν.withDensity (μ.rnDeriv ν)).rnDeriv (ν + ν') =ᶠ[ae ν] (μ.singularPart ν).rnDeriv ν + (ν.withDensity (μ.rnDeriv ν)).rnDeriv ν
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ ν ν' : Measure α<VAR>inst✝² : SigmaFinite μ<VAR>inst✝¹ : SigmaFinite ν<VAR>inst✝ : SigmaFinite ν'<VAR>hμν' : μ ⟂ₘ ν'<VAR>hνν' : ν ⟂ₘ ν'<VAR>h_ac : ν ≪ ν + ν'<VAR>h₁ : (μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)).rnDeriv (ν + ν') =ᶠ[ae (ν + ν')] (μ.singularPart ν).rnDeriv (ν + ν') + (ν.withDensity (μ.rnDeriv ν)).rnDeriv (ν + ν')<VAR>h₂ : (μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)).rnDeriv ν =ᶠ[ae ν] (μ.singularPart ν).rnDeriv ν + (ν.withDensity (μ.rnDeriv ν)).rnDeriv ν<VAR>h₃ : (ν.withDensity (μ.rnDeriv ν)).rnDeriv (ν + ν') =ᶠ[ae ν] (ν.withDensity (μ.rnDeriv ν)).rnDeriv ν<VAR>h₄ : (μ.singularPart ν).rnDeriv (ν + ν') =ᶠ[ae ν] 0<GOAL>(μ.singularPart ν).rnDeriv (ν + ν') + (ν.withDensity (μ.rnDeriv ν)).rnDeriv (ν + ν') =ᶠ[ae ν] (μ.singularPart ν).rnDeriv ν + (ν.withDensity (μ.rnDeriv ν)).rnDeriv ν
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ ν ν' : Measure α<VAR>inst✝² : SigmaFinite μ<VAR>inst✝¹ : SigmaFinite ν<VAR>inst✝ : SigmaFinite ν'<VAR>hμν' : μ ⟂ₘ ν'<VAR>hνν' : ν ⟂ₘ ν'<VAR>h_ac : ν ≪ ν + ν'<VAR>h₁ : (μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)).rnDeriv (ν + ν') =ᶠ[ae (ν + ν')] (μ.singularPart ν).rnDeriv (ν + ν') + (ν.withDensity (μ.rnDeriv ν)).rnDeriv (ν + ν')<VAR>h₂ : (μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)).rnDeriv ν =ᶠ[ae ν] (μ.singularPart ν).rnDeriv ν + (ν.withDensity (μ.rnDeriv ν)).rnDeriv ν<VAR>h₃ : (ν.withDensity (μ.rnDeriv ν)).rnDeriv (ν + ν') =ᶠ[ae ν] (ν.withDensity (μ.rnDeriv ν)).rnDeriv ν<VAR>h₄ : (μ.singularPart ν).rnDeriv (ν + ν') =ᶠ[ae ν] 0<VAR>h₅ : (μ.singularPart ν).rnDeriv ν =ᶠ[ae ν] 0<GOAL>(μ.singularPart ν).rnDeriv (ν + ν') + (ν.withDensity (μ.rnDeriv ν)).rnDeriv (ν + ν') =ᶠ[ae ν] (μ.singularPart ν).rnDeriv ν + (ν.withDensity (μ.rnDeriv ν)).rnDeriv ν
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ ν ν' : Measure α<VAR>inst✝² : SigmaFinite μ<VAR>inst✝¹ : SigmaFinite ν<VAR>inst✝ : SigmaFinite ν'<VAR>hμν' : μ ⟂ₘ ν'<VAR>hνν' : ν ⟂ₘ ν'<VAR>h_ac : ν ≪ ν + ν'<VAR>h₁ : (μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)).rnDeriv (ν + ν') =ᶠ[ae (ν + ν')] (μ.singularPart ν).rnDeriv (ν + ν') + (ν.withDensity (μ.rnDeriv ν)).rnDeriv (ν + ν')<VAR>h₂ : (μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)).rnDeriv ν =ᶠ[ae ν] (μ.singularPart ν).rnDeriv ν + (ν.withDensity (μ.rnDeriv ν)).rnDeriv ν<VAR>h₃ : (ν.withDensity (μ.rnDeriv ν)).rnDeriv (ν + ν') =ᶠ[ae ν] (ν.withDensity (μ.rnDeriv ν)).rnDeriv ν<VAR>h₄ : (μ.singularPart ν).rnDeriv (ν + ν') =ᶠ[ae ν] 0<VAR>h₅ : (μ.singularPart ν).rnDeriv ν =ᶠ[ae ν] 0<VAR>x : α<VAR>hx₃ : (ν.withDensity (μ.rnDeriv ν)).rnDeriv (ν + ν') x = (ν.withDensity (μ.rnDeriv ν)).rnDeriv ν x<VAR>hx₄ : (μ.singularPart ν).rnDeriv (ν + ν') x = 0 x<VAR>hx₅ : (μ.singularPart ν).rnDeriv ν x = 0 x<GOAL>((μ.singularPart ν).rnDeriv (ν + ν') + (ν.withDensity (μ.rnDeriv ν)).rnDeriv (ν + ν')) x = ((μ.singularPart ν).rnDeriv ν + (ν.withDensity (μ.rnDeriv ν)).rnDeriv ν) x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ ν ν' : Measure α<VAR>inst✝² : SigmaFinite μ<VAR>inst✝¹ : SigmaFinite ν<VAR>inst✝ : SigmaFinite ν'<VAR>hμν' : μ ⟂ₘ ν'<VAR>hνν' : ν ⟂ₘ ν'<VAR>h_ac : ν ≪ ν + ν'<VAR>h₁ : (μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)).rnDeriv (ν + ν') =ᶠ[ae (ν + ν')] (μ.singularPart ν).rnDeriv (ν + ν') + (ν.withDensity (μ.rnDeriv ν)).rnDeriv (ν + ν')<VAR>h₂ : (μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)).rnDeriv ν =ᶠ[ae ν] (μ.singularPart ν).rnDeriv ν + (ν.withDensity (μ.rnDeriv ν)).rnDeriv ν<VAR>h₃ : (ν.withDensity (μ.rnDeriv ν)).rnDeriv (ν + ν') =ᶠ[ae ν] (ν.withDensity (μ.rnDeriv ν)).rnDeriv ν<VAR>h₄ : (μ.singularPart ν).rnDeriv (ν + ν') =ᶠ[ae ν] 0<VAR>h₅ : (μ.singularPart ν).rnDeriv ν =ᶠ[ae ν] 0<VAR>x : α<VAR>hx₃ : (ν.withDensity (μ.rnDeriv ν)).rnDeriv (ν + ν') x = (ν.withDensity (μ.rnDeriv ν)).rnDeriv ν x<VAR>hx₄ : (μ.singularPart ν).rnDeriv (ν + ν') x = 0 x<VAR>hx₅ : (μ.singularPart ν).rnDeriv ν x = 0 x<GOAL>(μ.singularPart ν).rnDeriv (ν + ν') x + (ν.withDensity (μ.rnDeriv ν)).rnDeriv (ν + ν') x = (μ.singularPart ν).rnDeriv ν x + (ν.withDensity (μ.rnDeriv ν)).rnDeriv ν x
<VAR>f : ℕ → ℂ<VAR>x : ℝ<VAR>s : ℂ<VAR>hs : x < s.re<VAR>h : f =O[atTop] fun n => ↑n ^ (x - 1)<GOAL>LSeriesSummable f s
<VAR>f : ℕ → ℂ<VAR>x : ℝ<VAR>s : ℂ<VAR>hs : x < s.re<VAR>h : f =O[atTop] fun n => ↑n ^ (x - 1)<VAR>C : ℝ<VAR>hC : ∀ᶠ (x_1 : ℕ) in atTop, ‖f x_1‖ ≤ C * ‖↑x_1 ^ (x - 1)‖<GOAL>LSeriesSummable f s
<VAR>f : ℕ → ℂ<VAR>x : ℝ<VAR>s : ℂ<VAR>hs : x < s.re<VAR>h : f =O[atTop] fun n => ↑n ^ (x - 1)<VAR>C : ℝ<VAR>hC : ∀ᶠ (x_1 : ℕ) in atTop, ‖f x_1‖ ≤ C * ‖↑x_1 ^ (x - 1)‖<VAR>m : ℕ<VAR>hm : ∀ b ≥ m, ‖f b‖ ≤ C * ‖↑b ^ (x - 1)‖<GOAL>LSeriesSummable f s
<VAR>f : ℕ → ℂ<VAR>x : ℝ<VAR>s : ℂ<VAR>hs : x < s.re<VAR>h : f =O[atTop] fun n => ↑n ^ (x - 1)<VAR>C : ℝ<VAR>hC : ∀ᶠ (x_1 : ℕ) in atTop, ‖f x_1‖ ≤ C * ‖↑x_1 ^ (x - 1)‖<VAR>m : ℕ<VAR>hm : ∀ b ≥ m, ‖f b‖ ≤ C * ‖↑b ^ (x - 1)‖<VAR>C' : ℝ := max C ((insert 0 (image (fun n => ‖f n‖ / ↑n ^ (x - 1)) (range m))).max' ⋯)<GOAL>LSeriesSummable f s
<VAR>f : ℕ → ℂ<VAR>x : ℝ<VAR>s : ℂ<VAR>hs : x < s.re<VAR>h : f =O[atTop] fun n => ↑n ^ (x - 1)<VAR>C : ℝ<VAR>hC : ∀ᶠ (x_1 : ℕ) in atTop, ‖f x_1‖ ≤ C * ‖↑x_1 ^ (x - 1)‖<VAR>m : ℕ<VAR>hm : ∀ b ≥ m, ‖f b‖ ≤ C * ‖↑b ^ (x - 1)‖<VAR>C' : ℝ := max C ((insert 0 (image (fun n => ‖f n‖ / ↑n ^ (x - 1)) (range m))).max' ⋯)<VAR>hC'₀ : 0 ≤ C'<GOAL>LSeriesSummable f s
<VAR>f : ℕ → ℂ<VAR>x : ℝ<VAR>s : ℂ<VAR>hs : x < s.re<VAR>h : f =O[atTop] fun n => ↑n ^ (x - 1)<VAR>C : ℝ<VAR>hC : ∀ᶠ (x_1 : ℕ) in atTop, ‖f x_1‖ ≤ C * ‖↑x_1 ^ (x - 1)‖<VAR>m : ℕ<VAR>hm : ∀ b ≥ m, ‖f b‖ ≤ C * ‖↑b ^ (x - 1)‖<VAR>C' : ℝ := max C ((insert 0 (image (fun n => ‖f n‖ / ↑n ^ (x - 1)) (range m))).max' ⋯)<VAR>hC'₀ : 0 ≤ C'<VAR>hCC' : C ≤ C'<GOAL>LSeriesSummable f s
<VAR>f : ℕ → ℂ<VAR>x : ℝ<VAR>s : ℂ<VAR>hs : x < s.re<VAR>h : f =O[atTop] fun n => ↑n ^ (x - 1)<VAR>C : ℝ<VAR>hC : ∀ᶠ (x_1 : ℕ) in atTop, ‖f x_1‖ ≤ C * ‖↑x_1 ^ (x - 1)‖<VAR>m : ℕ<VAR>hm : ∀ b ≥ m, ‖f b‖ ≤ C * ‖↑b ^ (x - 1)‖<VAR>C' : ℝ := max C ((insert 0 (image (fun n => ‖f n‖ / ↑n ^ (x - 1)) (range m))).max' ⋯)<VAR>hC'₀ : 0 ≤ C'<VAR>hCC' : C ≤ C'<VAR>n : ℕ<VAR>hn₀ : n ≠ 0<GOAL>‖f n‖ ≤ C' * ↑n ^ (x - 1)
<VAR>f : ℕ → ℂ<VAR>x : ℝ<VAR>s : ℂ<VAR>hs : x < s.re<VAR>h : f =O[atTop] fun n => ↑n ^ (x - 1)<VAR>C : ℝ<VAR>hC : ∀ᶠ (x_1 : ℕ) in atTop, ‖f x_1‖ ≤ C * ‖↑x_1 ^ (x - 1)‖<VAR>m : ℕ<VAR>hm : ∀ b ≥ m, ‖f b‖ ≤ C * ‖↑b ^ (x - 1)‖<VAR>C' : ℝ := max C ((insert 0 (image (fun n => ‖f n‖ / ↑n ^ (x - 1)) (range m))).max' ⋯)<VAR>hC'₀ : 0 ≤ C'<VAR>hCC' : C ≤ C'<VAR>n : ℕ<VAR>hn₀ : n ≠ 0<VAR>hn : m ≤ n<GOAL>‖f n‖ ≤ C' * ↑n ^ (x - 1)
<VAR>f : ℕ → ℂ<VAR>x : ℝ<VAR>s : ℂ<VAR>hs : x < s.re<VAR>h : f =O[atTop] fun n => ↑n ^ (x - 1)<VAR>C : ℝ<VAR>hC : ∀ᶠ (x_1 : ℕ) in atTop, ‖f x_1‖ ≤ C * ‖↑x_1 ^ (x - 1)‖<VAR>m : ℕ<VAR>hm : ∀ b ≥ m, ‖f b‖ ≤ C * ‖↑b ^ (x - 1)‖<VAR>C' : ℝ := max C ((insert 0 (image (fun n => ‖f n‖ / ↑n ^ (x - 1)) (range m))).max' ⋯)<VAR>hC'₀ : 0 ≤ C'<VAR>hCC' : C ≤ C'<VAR>n : ℕ<VAR>hn₀ : n ≠ 0<VAR>hn : n < m<GOAL>‖f n‖ ≤ C' * ↑n ^ (x - 1)
<VAR>R : Type w₁<VAR>A : Type w₂<VAR>B : Type w₃<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : CommRing A<VAR>inst✝⁶ : Algebra R A<VAR>inst✝⁵ : CommRing B<VAR>inst✝⁴ : Algebra R B<VAR>inst✝³ : Algebra A B<VAR>inst✝² : IsScalarTower R A B<VAR>inst✝¹ : FinitePresentation R A<VAR>inst✝ hfpB : FinitePresentation A B<GOAL>FinitePresentation R B
<VAR>R : Type w₁<VAR>A : Type w₂<VAR>B : Type w₃<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : CommRing A<VAR>inst✝⁶ : Algebra R A<VAR>inst✝⁵ : CommRing B<VAR>inst✝⁴ : Algebra R B<VAR>inst✝³ : Algebra A B<VAR>inst✝² : IsScalarTower R A B<VAR>inst✝¹ : FinitePresentation R A<VAR>inst✝ hfpB : FinitePresentation A B<VAR>n : ℕ<VAR>I : Ideal (MvPolynomial (Fin n) A)<VAR>e : (MvPolynomial (Fin n) A ⧸ I) ≃ₐ[A] B<VAR>hfg : I.FG<GOAL>FinitePresentation R B
<VAR>R : Type w₁<VAR>A : Type w₂<VAR>B : Type w₃<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : CommRing A<VAR>inst✝⁶ : Algebra R A<VAR>inst✝⁵ : CommRing B<VAR>inst✝⁴ : Algebra R B<VAR>inst✝³ : Algebra A B<VAR>inst✝² : IsScalarTower R A B<VAR>inst✝¹ : FinitePresentation R A<VAR>inst✝ hfpB : FinitePresentation A B<VAR>n : ℕ<VAR>I : Ideal (MvPolynomial (Fin n) A)<VAR>e : (MvPolynomial (Fin n) A ⧸ I) ≃ₐ[A] B<VAR>hfg : I.FG<VAR>this : FinitePresentation R (MvPolynomial (Fin n) A ⧸ I) := FinitePresentation.quotient hfg<GOAL>FinitePresentation R B
<VAR>α : Type u<VAR>β : Type u_1<VAR>t : TopologicalSpace α<VAR>B✝ : Set (Set α)<VAR>s : Set α<VAR>B : Set (Set α)<VAR>hB : IsTopologicalBasis B<VAR>u : Set α<VAR>ou : IsOpen u<GOAL>u = ⋃ i, ↑i
<VAR>α : Type u<VAR>β : Type u_1<VAR>t : TopologicalSpace α<VAR>B✝ : Set (Set α)<VAR>s : Set α<VAR>B : Set (Set α)<VAR>hB : IsTopologicalBasis B<VAR>u : Set α<VAR>ou : IsOpen u<GOAL>u = ⋃₀ {s | s ∈ B ∧ s ⊆ u}
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝¹ : Ring R<VAR>inst✝ : Ring S<VAR>f : R →+* S<VAR>I : Type u_3<VAR>e : I → R<VAR>he : OrthogonalIdempotents e<VAR>J : Type u_4<VAR>i : J ↪ I<GOAL>OrthogonalIdempotents (e ∘ ⇑i)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝¹² : CommSemiring R<VAR>inst✝¹¹ : AddCommMonoid M<VAR>inst✝¹⁰ : Module R M<VAR>R₁ : Type u_3<VAR>M₁ : Type u_4<VAR>inst✝⁹ : CommRing R₁<VAR>inst✝⁸ : AddCommGroup M₁<VAR>inst✝⁷ : Module R₁ M₁<VAR>V : Type u_5<VAR>K : Type u_6<VAR>inst✝⁶ : Field K<VAR>inst✝⁵ : AddCommGroup V<VAR>inst✝⁴ : Module K V<VAR>B : BilinForm R M<VAR>B₁ : BilinForm R₁ M₁<VAR>R₄ : Type u_7<VAR>M₄ : Type u_8<VAR>inst✝³ : CommRing R₄<VAR>inst✝² : IsDomain R₄<VAR>inst✝¹ : AddCommGroup M₄<VAR>inst✝ : Module R₄ M₄<VAR>G : BilinForm R₄ M₄<VAR>x y : M₄<VAR>a : R₄<VAR>ha : a ≠ 0<GOAL>(G x) (a • y) = 0 ↔ (G x) y = 0
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝¹² : CommSemiring R<VAR>inst✝¹¹ : AddCommMonoid M<VAR>inst✝¹⁰ : Module R M<VAR>R₁ : Type u_3<VAR>M₁ : Type u_4<VAR>inst✝⁹ : CommRing R₁<VAR>inst✝⁸ : AddCommGroup M₁<VAR>inst✝⁷ : Module R₁ M₁<VAR>V : Type u_5<VAR>K : Type u_6<VAR>inst✝⁶ : Field K<VAR>inst✝⁵ : AddCommGroup V<VAR>inst✝⁴ : Module K V<VAR>B : BilinForm R M<VAR>B₁ : BilinForm R₁ M₁<VAR>R₄ : Type u_7<VAR>M₄ : Type u_8<VAR>inst✝³ : CommRing R₄<VAR>inst✝² : IsDomain R₄<VAR>inst✝¹ : AddCommGroup M₄<VAR>inst✝ : Module R₄ M₄<VAR>G : BilinForm R₄ M₄<VAR>x y : M₄<VAR>a : R₄<VAR>ha : a ≠ 0<GOAL>a • (G x) y = 0 ↔ (G x) y = 0
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : LinearOrderedSemiring α<VAR>inst✝ : FloorSemiring α<VAR>a✝ : α<VAR>n : ℕ<VAR>a b : α<VAR>ha : 0 ≤ a<VAR>hb : 0 ≤ b<VAR>x✝ : ℕ<GOAL>x✝ ∈ Nat.cast ⁻¹' Ioc a b ↔ x✝ ∈ Ioc ⌊a⌋₊ ⌊b⌋₊
<VAR>𝕜 : Type u_1<VAR>inst✝¹¹ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹⁰ : NormedAddCommGroup E<VAR>inst✝⁹ : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝⁸ : NormedAddCommGroup F<VAR>inst✝⁷ : NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>inst✝⁶ : NormedAddCommGroup G<VAR>inst✝⁵ : NormedSpace 𝕜 G<VAR>G' : Type u_5<VAR>inst✝⁴ : NormedAddCommGroup G'<VAR>inst✝³ : NormedSpace 𝕜 G'<VAR>f f₀ f₁ g : E → F<VAR>f' f₀' f₁' g' e : E →L[𝕜] F<VAR>x✝ : E<VAR>s t : Set E<VAR>L L₁ L₂ : Filter E<VAR>ι : Type u_6<VAR>inst✝² : Fintype ι<VAR>F' : ι → Type u_7<VAR>inst✝¹ : (i : ι) → NormedAddCommGroup (F' i)<VAR>inst✝ : (i : ι) → NormedSpace 𝕜 (F' i)<VAR>φ : (i : ι) → E → F' i<VAR>φ' : (i : ι) → E →L[𝕜] F' i<VAR>Φ : E → (i : ι) → F' i<VAR>Φ' : E →L[𝕜] (i : ι) → F' i<VAR>i : ι<VAR>x : (i : ι) → F' i<GOAL>DifferentiableAt 𝕜 (fun f => f i) x
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>P : StrongFEPair E<VAR>r : ℝ<GOAL>P.f =O[𝓝[>] 0] fun x => x ^ r
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>P : StrongFEPair E<VAR>r : ℝ<VAR>this : (fun x => P.f x - (P.ε * ↑(x ^ (-P.k))) • 0) =O[𝓝[>] 0] fun x => x ^ r<GOAL>P.f =O[𝓝[>] 0] fun x => x ^ r
<VAR>F : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝ : TopologicalSpace α<VAR>f : α →ᵇ ℝ<GOAL>abs ∘ ⇑f = toReal ∘ ⇑f.nnrealPart + toReal ∘ ⇑(-f).nnrealPart
<VAR>F : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝ : TopologicalSpace α<VAR>f : α →ᵇ ℝ<VAR>x : α<GOAL>(abs ∘ ⇑f) x = (toReal ∘ ⇑f.nnrealPart + toReal ∘ ⇑(-f).nnrealPart) x
<VAR>F : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝ : TopologicalSpace α<VAR>f : α →ᵇ ℝ<VAR>x : α<GOAL>|f x| = max (f x) 0 + max (-f x) 0
<VAR>ι : Sort u_1<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>a b c u v✝ w✝ : V<VAR>e : Sym2 V<VAR>s : Set (Sym2 V)<VAR>v w : V<GOAL>(fromEdgeSet G.edgeSet).Adj v w ↔ G.Adj v w
<VAR>𝕜 : Type u𝕜<VAR>G : Type uG<VAR>E : Type uE<VAR>E' : Type uE'<VAR>E'' : Type uE''<VAR>F : Type uF<VAR>F' : Type uF'<VAR>F'' : Type uF''<VAR>P : Type uP<VAR>inst✝¹² : NormedAddCommGroup E<VAR>inst✝¹¹ : NormedAddCommGroup E'<VAR>inst✝¹⁰ : NormedAddCommGroup E''<VAR>inst✝⁹ : NormedAddCommGroup F<VAR>f f' : G → E<VAR>g g' : G → E'<VAR>x x' : G<VAR>y✝ y' : E<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>inst✝⁷ : NormedSpace 𝕜 E<VAR>inst✝⁶ : NormedSpace 𝕜 E'<VAR>inst✝⁵ : NormedSpace 𝕜 E''<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>L : E →L[𝕜] E' →L[𝕜] F<VAR>inst✝³ : MeasurableSpace G<VAR>μ ν : Measure G<VAR>inst✝² : NormedSpace ℝ F<VAR>inst✝¹ : AddGroup G<VAR>inst✝ : SMulCommClass ℝ 𝕜 F<VAR>y : 𝕜<VAR>x✝ : G<GOAL>(f ⋆[L, μ] y • g) x✝ = (y • (f ⋆[L, μ] g)) x✝
<VAR>q : ℚ<VAR>x y : ℝ<VAR>h : Irrational x<GOAL>Irrational x⁻¹⁻¹
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>P : Type u_4<VAR>R : Type u_5<VAR>S : Type u_6<VAR>inst✝⁹ : Semiring R<VAR>inst✝⁸ : Semiring S<VAR>inst✝⁷ : AddCommMonoid M<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : AddCommMonoid N<VAR>inst✝⁴ : Module R N<VAR>inst✝³ : AddCommMonoid P<VAR>inst✝² : Module R P<VAR>α' : Type u_7<VAR>M' : Type u_8<VAR>inst✝¹ : AddCommMonoid M'<VAR>inst✝ : Module R M'<VAR>v✝ : α → M<VAR>v' : α' → M'<VAR>f : M →ₗ[R] M'<VAR>v : α → M<VAR>l : α →₀ R<GOAL>f ((Finsupp.total α M R v) l) = (Finsupp.total α M' R (⇑f ∘ v)) l
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>f : X →. Y<VAR>hf : ∀ {x : X} {y : Y}, y ∈ f x → PTendsto' f (𝓝 x) (𝓝 y)<VAR>s : Set Y<VAR>os : IsOpen s<GOAL>IsOpen (f.preimage s)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>f : X →. Y<VAR>hf : ∀ {x : X} {y : Y}, y ∈ f x → PTendsto' f (𝓝 x) (𝓝 y)<VAR>s : Set Y<VAR>os : IsOpen s<GOAL>∀ x ∈ f.preimage s, 𝓝 x ≤ 𝓟 (f.preimage s)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>f : X →. Y<VAR>hf : ∀ {x : X} {y : Y}, y ∈ f x → PTendsto' f (𝓝 x) (𝓝 y)<VAR>s : Set Y<VAR>os : IsOpen s<VAR>x : X<VAR>y : Y<VAR>ys : y ∈ s<VAR>fxy : y ∈ f x<VAR>t : Set X<GOAL>t ∈ 𝓟 (f.preimage s) → t ∈ 𝓝 x
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>f : X →. Y<VAR>hf : ∀ {x : X} {y : Y}, y ∈ f x → PTendsto' f (𝓝 x) (𝓝 y)<VAR>s : Set Y<VAR>os : IsOpen s<VAR>x : X<VAR>y : Y<VAR>ys : y ∈ s<VAR>fxy : y ∈ f x<VAR>t : Set X<GOAL>f.preimage s ⊆ t → t ∈ 𝓝 x
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>f : X →. Y<VAR>hf : ∀ {x : X} {y : Y}, y ∈ f x → PTendsto' f (𝓝 x) (𝓝 y)<VAR>s : Set Y<VAR>os : IsOpen s<VAR>x : X<VAR>y : Y<VAR>ys : y ∈ s<VAR>fxy : y ∈ f x<VAR>t : Set X<VAR>h : f.preimage s ⊆ t<GOAL>t ∈ 𝓝 x
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>f : X →. Y<VAR>hf : ∀ {x : X} {y : Y}, y ∈ f x → PTendsto' f (𝓝 x) (𝓝 y)<VAR>s : Set Y<VAR>os : IsOpen s<VAR>x : X<VAR>y : Y<VAR>ys : y ∈ s<VAR>fxy : y ∈ f x<VAR>t : Set X<VAR>h : f.preimage s ⊆ t<GOAL>f.preimage s ∈ 𝓝 x
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>f : X →. Y<VAR>hf : ∀ {x : X} {y : Y}, y ∈ f x → PTendsto' f (𝓝 x) (𝓝 y)<VAR>s : Set Y<VAR>os : IsOpen s<VAR>x : X<VAR>y : Y<VAR>ys : y ∈ s<VAR>fxy : y ∈ f x<VAR>t : Set X<VAR>h : f.preimage s ⊆ t<VAR>h' : ∀ s ∈ 𝓝 y, f.preimage s ∈ 𝓝 x<GOAL>f.preimage s ∈ 𝓝 x
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>f : X →. Y<VAR>hf : ∀ {x : X} {y : Y}, y ∈ f x → PTendsto' f (𝓝 x) (𝓝 y)<VAR>s : Set Y<VAR>os : IsOpen s<VAR>x : X<VAR>y : Y<VAR>ys : y ∈ s<VAR>fxy : y ∈ f x<VAR>t : Set X<VAR>h : f.preimage s ⊆ t<VAR>h' : ∀ s ∈ 𝓝 y, f.preimage s ∈ 𝓝 x<GOAL>s ∈ 𝓝 y
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>f : X →. Y<VAR>hf : ∀ {x : X} {y : Y}, y ∈ f x → PTendsto' f (𝓝 x) (𝓝 y)<VAR>s : Set Y<VAR>os : IsOpen s<VAR>x : X<VAR>y : Y<VAR>ys : y ∈ s<VAR>fxy : y ∈ f x<VAR>t : Set X<VAR>h : f.preimage s ⊆ t<VAR>h' : ∀ s ∈ 𝓝 y, f.preimage s ∈ 𝓝 x<GOAL>∃ t ⊆ s, IsOpen t ∧ y ∈ t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : Preorder α<VAR>inst✝² : AddCommSemigroup α<VAR>inst✝¹ : Sub α<VAR>inst✝ : OrderedSub α<VAR>a b c d : α<VAR>hb : AddLECancellable b<VAR>h : a + b ≤ c<GOAL>b + a ≤ c
<VAR>C : Type u<VAR>inst✝ : Groupoid C<VAR>S : Subgroupoid C<VAR>c : C<VAR>hc : c ∈ S.objs<VAR>d : C<VAR>hd : d ∈ S.objs<VAR>hcd : S.hom.obj ⟨c, hc⟩ = S.hom.obj ⟨d, hd⟩<GOAL>⟨c, hc⟩ = ⟨d, hd⟩
<VAR>C : Type u<VAR>inst✝ : Groupoid C<VAR>S : Subgroupoid C<VAR>c : C<VAR>hc : c ∈ S.objs<VAR>d : C<VAR>hd : d ∈ S.objs<VAR>hcd : S.hom.obj ⟨c, hc⟩ = S.hom.obj ⟨d, hd⟩<GOAL>c = d
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : MeasurableSpace α<VAR>inst✝ : CountablyGenerated α<VAR>s : Set α<VAR>hs : s ∈ countableGeneratingSet α<GOAL>MeasurableSet s
<VAR>α : Type u_1<VAR>inst✝³ : CancelCommMonoidWithZero α<VAR>inst✝² : UniqueFactorizationMonoid α<VAR>inst✝¹ : NormalizationMonoid α<VAR>inst✝ : DecidableEq α<VAR>n : α<GOAL>(factorization n).support = (normalizedFactors n).toFinset