ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>M : Submonoid R<VAR>S : Type u_2<VAR>CommSemiring S<VAR>Algebra R S<VAR>IsLocalization M S<VAR>ι : Type u_4<VAR>s : Finset ι<VAR>f : ι → S<GOAL>∃ b, ∀ i ∈ s, IsLocalization.IsInteger R (↑b • f i)
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>M : Submonoid R<VAR>S : Type u_2<VAR>CommSemiring S<VAR>Algebra R S<VAR>IsLocalization M S<VAR>ι : Type u_4<VAR>Finite ι<VAR>f : ι → S<GOAL>∃ b, ∀ (i : ι), IsLocalization.IsInteger R (↑b • f i)
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>M : Submonoid R<VAR>S : Type u_2<VAR>CommSemiring S<VAR>Algebra R S<VAR>IsLocalization M S<VAR>s : Finset S<GOAL>∃ b, ∀ a ∈ s, IsLocalization.IsInteger R (↑b • a)
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>M : Submonoid R<VAR>S : Type u_2<VAR>CommSemiring S<VAR>Algebra R S<VAR>IsLocalization M S<VAR>ι : Type u_4<VAR>s : Finset ι<VAR>f : ι → S<VAR>i : { x // x ∈ s }<GOAL>(algebraMap R S) (IsLocalization.integerMultiple M s f i) = IsLocalization.commonDenom M s f • f ↑i
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>M : Submonoid R<VAR>S : Type u_2<VAR>CommSemiring S<VAR>Algebra R S<VAR>IsLocalization M S<VAR>DecidableEq R<VAR>s : Finset S<GOAL>⇑(algebraMap R S) '' ↑(IsLocalization.finsetIntegerMultiple M s) = IsLocalization.commonDenomOfFinset M s • ↑s
<VAR>R : Type u<VAR>CommSemiring R<VAR>A : Type u<VAR>Semiring A<VAR>Algebra R A<GOAL>Algebra.FormallySmooth R A ↔ ∀ ⦃B : Type u⦄ [inst : CommRing B] [inst_1 : Algebra R B] (I : Ideal B), I ^ 2 = ⊥ → Function.Surjective (Ideal.Quotient.mkₐ R I).comp
<VAR>R : Type u<VAR>CommSemiring R<VAR>A : Type u<VAR>Semiring A<VAR>Algebra R A<VAR>self : Algebra.FormallySmooth R A<VAR>B : Type u<VAR>CommRing B<VAR>Algebra R B<VAR>I : Ideal B<GOAL>I ^ 2 = ⊥ → Function.Surjective (Ideal.Quotient.mkₐ R I).comp
<VAR>R : Type u<VAR>CommSemiring R<VAR>A : Type u<VAR>Semiring A<VAR>Algebra R A<VAR>B : Type u<VAR>CommRing B<VAR>_RB : Algebra R B<VAR>Algebra.FormallySmooth R A<VAR>I : Ideal B<VAR>hI : IsNilpotent I<VAR>g : A →ₐ[R] B ⧸ I<GOAL>∃ f, (Ideal.Quotient.mkₐ R I).comp f = g
<VAR>R : Type u<VAR>CommSemiring R<VAR>A : Type u<VAR>Semiring A<VAR>Algebra R A<VAR>B : Type u<VAR>CommRing B<VAR>Algebra R B<VAR>Algebra.FormallySmooth R A<VAR>I : Ideal B<VAR>hI : IsNilpotent I<VAR>g : A →ₐ[R] B ⧸ I<GOAL>(Ideal.Quotient.mkₐ R I).comp (Algebra.FormallySmooth.lift I hI g) = g
<VAR>R : Type u<VAR>CommSemiring R<VAR>A : Type u<VAR>Semiring A<VAR>Algebra R A<VAR>B : Type u<VAR>CommRing B<VAR>Algebra R B<VAR>Algebra.FormallySmooth R A<VAR>I : Ideal B<VAR>hI : IsNilpotent I<VAR>g : A →ₐ[R] B ⧸ I<VAR>x : A<GOAL>(Ideal.Quotient.mk I) ((Algebra.FormallySmooth.lift I hI g) x) = g x
<VAR>R : Type u<VAR>CommSemiring R<VAR>A : Type u<VAR>Semiring A<VAR>Algebra R A<VAR>B : Type u<VAR>CommRing B<VAR>Algebra R B<VAR>C : Type u<VAR>CommRing C<VAR>Algebra R C<VAR>Algebra.FormallySmooth R A<VAR>f : A →ₐ[R] C<VAR>g : B →ₐ[R] C<VAR>hg : Function.Surjective ⇑g<VAR>hg' : IsNilpotent (RingHom.ker ↑g)<VAR>x : A<GOAL>g ((Algebra.FormallySmooth.liftOfSurjective f g hg hg') x) = f x
<VAR>R : Type u<VAR>CommSemiring R<VAR>A : Type u<VAR>Semiring A<VAR>Algebra R A<VAR>B : Type u<VAR>CommRing B<VAR>Algebra R B<VAR>C : Type u<VAR>CommRing C<VAR>Algebra R C<VAR>Algebra.FormallySmooth R A<VAR>f : A →ₐ[R] C<VAR>g : B →ₐ[R] C<VAR>hg : Function.Surjective ⇑g<VAR>hg' : IsNilpotent (RingHom.ker ↑g)<GOAL>g.comp (Algebra.FormallySmooth.liftOfSurjective f g hg hg') = f
<VAR>R : Type u<VAR>CommSemiring R<VAR>A B : Type u<VAR>Semiring A<VAR>Algebra R A<VAR>Semiring B<VAR>Algebra R B<VAR>Algebra.FormallySmooth R A<VAR>e : A ≃ₐ[R] B<GOAL>Algebra.FormallySmooth R B
<VAR>R : Type u<VAR>CommSemiring R<VAR>A : Type u<VAR>CommSemiring A<VAR>Algebra R A<VAR>B : Type u<VAR>Semiring B<VAR>Algebra R B<VAR>Algebra A B<VAR>IsScalarTower R A B<VAR>Algebra.FormallySmooth R A<VAR>Algebra.FormallySmooth A B<GOAL>Algebra.FormallySmooth R B
<VAR>R : Type u<VAR>CommRing R<VAR>P A : Type u<VAR>CommRing A<VAR>Algebra R A<VAR>CommRing P<VAR>Algebra R P<VAR>f : P →ₐ[R] A<VAR>Algebra.FormallySmooth R P<VAR>g : A →ₐ[R] P ⧸ RingHom.ker f.toRingHom ^ 2<VAR>hg : f.kerSquareLift.comp g = AlgHom.id R A<GOAL>Algebra.FormallySmooth R A
<VAR>R : Type u<VAR>CommRing R<VAR>P A : Type u<VAR>CommRing A<VAR>Algebra R A<VAR>CommRing P<VAR>Algebra R P<VAR>f : P →ₐ[R] A<VAR>hf : Function.Surjective ⇑f<VAR>Algebra.FormallySmooth R P<GOAL>Algebra.FormallySmooth R A ↔ ∃ g, f.kerSquareLift.comp g = AlgHom.id R A
<VAR>R Rₘ : Type u<VAR>CommRing R<VAR>CommRing Rₘ<VAR>M : Submonoid R<VAR>Algebra R Rₘ<VAR>IsLocalization M Rₘ<GOAL>Algebra.FormallySmooth R Rₘ
<VAR>R Rₘ Sₘ : Type u<VAR>CommRing R<VAR>CommRing Rₘ<VAR>CommRing Sₘ<VAR>M : Submonoid R<VAR>Algebra R Sₘ<VAR>Algebra R Rₘ<VAR>Algebra Rₘ Sₘ<VAR>IsScalarTower R Rₘ Sₘ<VAR>IsLocalization M Rₘ<VAR>Algebra.FormallySmooth R Sₘ<GOAL>Algebra.FormallySmooth Rₘ Sₘ
<VAR>R S Rₘ Sₘ : Type u<VAR>CommRing R<VAR>CommRing S<VAR>CommRing Rₘ<VAR>CommRing Sₘ<VAR>M : Submonoid R<VAR>Algebra R S<VAR>Algebra R Sₘ<VAR>Algebra S Sₘ<VAR>Algebra R Rₘ<VAR>Algebra Rₘ Sₘ<VAR>IsScalarTower R Rₘ Sₘ<VAR>IsScalarTower R S Sₘ<VAR>IsLocalization M Rₘ<VAR>IsLocalization (Submonoid.map (algebraMap R S) M) Sₘ<VAR>Algebra.FormallySmooth R S<GOAL>Algebra.FormallySmooth Rₘ Sₘ
<VAR>R : Type u<VAR>CommSemiring R<VAR>A : Type u<VAR>Semiring A<VAR>Algebra R A<VAR>self : Algebra.Smooth R A<GOAL>Algebra.FormallySmooth R A
<VAR>R : Type u<VAR>CommSemiring R<VAR>A : Type u<VAR>Semiring A<VAR>Algebra R A<VAR>self : Algebra.Smooth R A<GOAL>Algebra.FinitePresentation R A
<VAR>R : Type u<VAR>CommRing R<VAR>A B : Type u<VAR>CommRing A<VAR>Algebra R A<VAR>CommRing B<VAR>Algebra R B<VAR>Algebra.Smooth R A<VAR>e : A ≃ₐ[R] B<GOAL>Algebra.Smooth R B
<VAR>R : Type u<VAR>CommRing R<VAR>A : Type u<VAR>CommRing A<VAR>Algebra R A<VAR>r : R<VAR>IsLocalization.Away r A<GOAL>Algebra.Smooth R A
<VAR>R : Type u<VAR>CommRing R<VAR>A B : Type u<VAR>CommRing A<VAR>Algebra R A<VAR>CommRing B<VAR>Algebra R B<VAR>Algebra A B<VAR>IsScalarTower R A B<VAR>Algebra.Smooth R A<VAR>Algebra.Smooth A B<GOAL>Algebra.Smooth R B
<VAR>α : Type u_1<VAR>Fintype α<VAR>Nonempty α<VAR>T : ℕ → ℝ<VAR>g : ℝ → ℝ<VAR>a b : α → ℝ<VAR>r : α → ℕ → ℕ<VAR>self : AkraBazziRecurrence T g a b r<VAR>i : α<GOAL>(fun n => ↑(r i n) - b i * ↑n) =o[Filter.atTop] fun n => ↑n / Real.log ↑n ^ 2
<VAR>α : Type u_1<VAR>Fintype α<VAR>Nonempty α<VAR>T : ℕ → ℝ<VAR>g : ℝ → ℝ<VAR>a b : α → ℝ<VAR>r : α → ℕ → ℕ<VAR>self : AkraBazziRecurrence T g a b r<VAR>i : α<VAR>n : ℕ<GOAL>self.n₀ ≤ n → r i n < n
<VAR>α : Type u_1<VAR>Fintype α<VAR>Nonempty α<VAR>T : ℕ → ℝ<VAR>g : ℝ → ℝ<VAR>a b : α → ℝ<VAR>r : α → ℕ → ℕ<VAR>self : AkraBazziRecurrence T g a b r<VAR>i : α<GOAL>0 < a i
<VAR>α : Type u_1<VAR>Fintype α<VAR>Nonempty α<VAR>T : ℕ → ℝ<VAR>g : ℝ → ℝ<VAR>a b : α → ℝ<VAR>r : α → ℕ → ℕ<VAR>self : AkraBazziRecurrence T g a b r<VAR>i : α<GOAL>0 < b i
<VAR>α : Type u_1<VAR>Fintype α<VAR>Nonempty α<VAR>T : ℕ → ℝ<VAR>g : ℝ → ℝ<VAR>a b : α → ℝ<VAR>r : α → ℕ → ℕ<VAR>self : AkraBazziRecurrence T g a b r<GOAL>0 < self.n₀
<VAR>α : Type u_1<VAR>Fintype α<VAR>Nonempty α<VAR>T : ℕ → ℝ<VAR>g : ℝ → ℝ<VAR>a b : α → ℝ<VAR>r : α → ℕ → ℕ<VAR>self : AkraBazziRecurrence T g a b r<VAR>i : α<GOAL>b i < 1
<VAR>α : Type u_1<VAR>Fintype α<VAR>Nonempty α<VAR>T : ℕ → ℝ<VAR>g : ℝ → ℝ<VAR>a b : α → ℝ<VAR>r : α → ℕ → ℕ<VAR>self : AkraBazziRecurrence T g a b r<VAR>n : ℕ<VAR>hn : n < self.n₀<GOAL>0 < T n
<VAR>α : Type u_1<VAR>Fintype α<VAR>Nonempty α<VAR>T : ℕ → ℝ<VAR>g : ℝ → ℝ<VAR>a b : α → ℝ<VAR>r : α → ℕ → ℕ<VAR>self : AkraBazziRecurrence T g a b r<VAR>x : ℝ<GOAL>x ≥ 0 → 0 ≤ g x
<VAR>α : Type u_1<VAR>Fintype α<VAR>Nonempty α<VAR>T : ℕ → ℝ<VAR>g : ℝ → ℝ<VAR>a b : α → ℝ<VAR>r : α → ℕ → ℕ<VAR>self : AkraBazziRecurrence T g a b r<GOAL>AkraBazziRecurrence.GrowsPolynomially g
<VAR>α : Type u_1<VAR>Fintype α<VAR>Nonempty α<VAR>T : ℕ → ℝ<VAR>g : ℝ → ℝ<VAR>a b : α → ℝ<VAR>r : α → ℕ → ℕ<VAR>self : AkraBazziRecurrence T g a b r<VAR>n : ℕ<VAR>hn₀ : self.n₀ ≤ n<GOAL>T n = ∑ i : α, a i * T (r i n) + g ↑n
<VAR>α : Type u_1<VAR>Finite α<VAR>Nonempty α<VAR>b : α → ℝ<VAR>i : α<GOAL>b (AkraBazziRecurrence.min_bi b) ≤ b i
<VAR>α : Type u_1<VAR>Finite α<VAR>Nonempty α<VAR>b : α → ℝ<VAR>i : α<GOAL>b i ≤ b (AkraBazziRecurrence.max_bi b)
<VAR>α : Type u_1<VAR>Fintype α<VAR>Nonempty α<VAR>T : ℕ → ℝ<VAR>g : ℝ → ℝ<VAR>a b : α → ℝ<VAR>r : α → ℕ → ℕ<VAR>R : AkraBazziRecurrence T g a b r<GOAL>∀ᶠ (n : ℕ) in Filter.atTop, ∀ (i : α), ‖↑(r i n) - b i * ↑n‖ ≤ ↑n / Real.log ↑n ^ 2
<GOAL>(fun n => ↑n / Real.log ↑n ^ 2) =o[Filter.atTop] fun n => ↑n
<VAR>α : Type u_1<VAR>Fintype α<VAR>Nonempty α<VAR>T : ℕ → ℝ<VAR>g : ℝ → ℝ<VAR>a b : α → ℝ<VAR>r : α → ℕ → ℕ<VAR>R : AkraBazziRecurrence T g a b r<GOAL>∀ᶠ (n : ℕ) in Filter.atTop, ∀ (i : α), b i * ↑n - ↑n / Real.log ↑n ^ 2 ≤ ↑(r i n)
<VAR>α : Type u_1<VAR>Fintype α<VAR>Nonempty α<VAR>T : ℕ → ℝ<VAR>g : ℝ → ℝ<VAR>a b : α → ℝ<VAR>r : α → ℕ → ℕ<VAR>R : AkraBazziRecurrence T g a b r<GOAL>∀ᶠ (n : ℕ) in Filter.atTop, ∀ (i : α), ↑(r i n) ≤ b i * ↑n + ↑n / Real.log ↑n ^ 2
<VAR>α : Type u_1<VAR>Fintype α<VAR>Nonempty α<VAR>T : ℕ → ℝ<VAR>g : ℝ → ℝ<VAR>a b : α → ℝ<VAR>r : α → ℕ → ℕ<VAR>R : AkraBazziRecurrence T g a b r<GOAL>∀ᶠ (n : ℕ) in Filter.atTop, ∀ (i : α), r i n < n
<VAR>α : Type u_1<VAR>Fintype α<VAR>Nonempty α<VAR>T : ℕ → ℝ<VAR>g : ℝ → ℝ<VAR>a b : α → ℝ<VAR>r : α → ℕ → ℕ<VAR>R : AkraBazziRecurrence T g a b r<GOAL>∀ᶠ (n : ℕ) in Filter.atTop, ∀ (i : α), b (AkraBazziRecurrence.min_bi b) / 2 * ↑n ≤ ↑(r i n)
<VAR>α : Type u_1<VAR>Fintype α<VAR>Nonempty α<VAR>T : ℕ → ℝ<VAR>g : ℝ → ℝ<VAR>a b : α → ℝ<VAR>r : α → ℕ → ℕ<VAR>R : AkraBazziRecurrence T g a b r<GOAL>b (AkraBazziRecurrence.min_bi b) / 2 < 1
<VAR>α : Type u_1<VAR>Fintype α<VAR>Nonempty α<VAR>T : ℕ → ℝ<VAR>g : ℝ → ℝ<VAR>a b : α → ℝ<VAR>r : α → ℕ → ℕ<VAR>R : AkraBazziRecurrence T g a b r<GOAL>0 < b (AkraBazziRecurrence.min_bi b) / 2
<VAR>α : Type u_1<VAR>Fintype α<VAR>Nonempty α<VAR>T : ℕ → ℝ<VAR>g : ℝ → ℝ<VAR>a b : α → ℝ<VAR>r : α → ℕ → ℕ<VAR>R : AkraBazziRecurrence T g a b r<GOAL>∃ c ∈ Set.Ioo 0 1, ∀ᶠ (n : ℕ) in Filter.atTop, ∀ (i : α), c * ↑n ≤ ↑(r i n)
<VAR>α : Type u_1<VAR>Fintype α<VAR>Nonempty α<VAR>T : ℕ → ℝ<VAR>g : ℝ → ℝ<VAR>a b : α → ℝ<VAR>r : α → ℕ → ℕ<VAR>R : AkraBazziRecurrence T g a b r<VAR>C : ℝ<GOAL>∀ᶠ (n : ℕ) in Filter.atTop, ∀ (i : α), C ≤ ↑(r i n)
<VAR>α : Type u_1<VAR>Fintype α<VAR>Nonempty α<VAR>T : ℕ → ℝ<VAR>g : ℝ → ℝ<VAR>a b : α → ℝ<VAR>r : α → ℕ → ℕ<VAR>R : AkraBazziRecurrence T g a b r<VAR>i : α<GOAL>Filter.Tendsto (r i) Filter.atTop Filter.atTop
<VAR>α : Type u_1<VAR>Fintype α<VAR>Nonempty α<VAR>T : ℕ → ℝ<VAR>g : ℝ → ℝ<VAR>a b : α → ℝ<VAR>r : α → ℕ → ℕ<VAR>R : AkraBazziRecurrence T g a b r<VAR>i : α<GOAL>Filter.Tendsto (fun n => ↑(r i n)) Filter.atTop Filter.atTop
<VAR>α : Type u_1<VAR>Fintype α<VAR>Nonempty α<VAR>T : ℕ → ℝ<VAR>g : ℝ → ℝ<VAR>a b : α → ℝ<VAR>r : α → ℕ → ℕ<VAR>R : AkraBazziRecurrence T g a b r<GOAL>∃ c ∈ Set.Ioo 0 1, ∀ᶠ (n : ℕ) in Filter.atTop, ∀ (i : α), ↑(r i n) ≤ c * ↑n
<VAR>α : Type u_1<VAR>Fintype α<VAR>Nonempty α<VAR>T : ℕ → ℝ<VAR>g : ℝ → ℝ<VAR>a b : α → ℝ<VAR>r : α → ℕ → ℕ<VAR>R : AkraBazziRecurrence T g a b r<GOAL>∀ᶠ (n : ℕ) in Filter.atTop, ∀ (i : α), 0 < r i n
<VAR>α : Type u_1<VAR>Fintype α<VAR>Nonempty α<VAR>T : ℕ → ℝ<VAR>g : ℝ → ℝ<VAR>a b : α → ℝ<VAR>r : α → ℕ → ℕ<VAR>R : AkraBazziRecurrence T g a b r<GOAL>∀ᶠ (n : ℕ) in Filter.atTop, ∀ (i : α), 0 < Real.log (b i * ↑n)
<VAR>α : Type u_1<VAR>Fintype α<VAR>Nonempty α<VAR>T : ℕ → ℝ<VAR>g : ℝ → ℝ<VAR>a b : α → ℝ<VAR>r : α → ℕ → ℕ<VAR>R : AkraBazziRecurrence T g a b r<VAR>n : ℕ<GOAL>0 < T n
<VAR>α : Type u_1<VAR>Fintype α<VAR>Nonempty α<VAR>T : ℕ → ℝ<VAR>g : ℝ → ℝ<VAR>a b : α → ℝ<VAR>r : α → ℕ → ℕ<VAR>R : AkraBazziRecurrence T g a b r<VAR>n : ℕ<GOAL>0 ≤ T n
<VAR>x : ℝ<VAR>hx : rexp 1 ≤ x<GOAL>1 + AkraBazziRecurrence.smoothingFn x ≤ 2
<GOAL>AkraBazziRecurrence.smoothingFn =o[Filter.atTop] fun x => 1
<GOAL>(fun x => 1 + AkraBazziRecurrence.smoothingFn x) ~[Filter.atTop] fun x => 1
<GOAL>(fun x => 1 - AkraBazziRecurrence.smoothingFn x) ~[Filter.atTop] fun x => 1
<GOAL>AkraBazziRecurrence.GrowsPolynomially fun x => 1 - AkraBazziRecurrence.smoothingFn x
<GOAL>AkraBazziRecurrence.GrowsPolynomially fun x => 1 + AkraBazziRecurrence.smoothingFn x
<VAR>c : ℝ<VAR>hc : c < 1<GOAL>∀ᶠ (x : ℝ) in Filter.atTop, c < 1 - AkraBazziRecurrence.smoothingFn x
<VAR>c : ℝ<VAR>hc : c < 1<GOAL>∀ᶠ (n : ℕ) in Filter.atTop, c < 1 - AkraBazziRecurrence.smoothingFn ↑n
<GOAL>∀ᶠ (x : ℝ) in Filter.atTop, 0 < 1 - AkraBazziRecurrence.smoothingFn x
<GOAL>∀ᶠ (n : ℕ) in Filter.atTop, 0 < 1 - AkraBazziRecurrence.smoothingFn ↑n
<GOAL>∀ᶠ (n : ℕ) in Filter.atTop, 0 ≤ 1 - AkraBazziRecurrence.smoothingFn ↑n
<VAR>α : Type u_1<VAR>Fintype α<VAR>Nonempty α<VAR>T : ℕ → ℝ<VAR>g : ℝ → ℝ<VAR>a b : α → ℝ<VAR>r : α → ℕ → ℕ<VAR>R : AkraBazziRecurrence T g a b r<GOAL>∀ᶠ (n : ℕ) in Filter.atTop, ∀ (i : α), 0 < 1 - AkraBazziRecurrence.smoothingFn ↑(r i n)
<VAR>x : ℝ<VAR>hx : 1 < x<GOAL>DifferentiableAt ℝ AkraBazziRecurrence.smoothingFn x
<VAR>x : ℝ<VAR>hx : 1 < x<GOAL>DifferentiableAt ℝ (fun z => 1 - AkraBazziRecurrence.smoothingFn z) x
<GOAL>DifferentiableOn ℝ (fun z => 1 - AkraBazziRecurrence.smoothingFn z) (Set.Ioi 1)
<VAR>x : ℝ<VAR>hx : 1 < x<GOAL>DifferentiableAt ℝ (fun z => 1 + AkraBazziRecurrence.smoothingFn z) x
<GOAL>DifferentiableOn ℝ (fun z => 1 + AkraBazziRecurrence.smoothingFn z) (Set.Ioi 1)
<VAR>x : ℝ<VAR>hx : 1 < x<GOAL>deriv AkraBazziRecurrence.smoothingFn x = -x⁻¹ / Real.log x ^ 2
<GOAL>deriv AkraBazziRecurrence.smoothingFn =o[Filter.atTop] fun x => x⁻¹
<GOAL>(deriv fun x => 1 - AkraBazziRecurrence.smoothingFn x) =ᶠ[Filter.atTop] fun x => x⁻¹ / Real.log x ^ 2
<GOAL>(deriv fun x => 1 + AkraBazziRecurrence.smoothingFn x) =ᶠ[Filter.atTop] fun x => -x⁻¹ / Real.log x ^ 2
<GOAL>(deriv fun x => 1 - AkraBazziRecurrence.smoothingFn x) =o[Filter.atTop] fun x => x⁻¹
<GOAL>(deriv fun x => 1 + AkraBazziRecurrence.smoothingFn x) =o[Filter.atTop] fun x => x⁻¹
<GOAL>∀ᶠ (n : ℕ) in Filter.atTop, 0 < 1 + AkraBazziRecurrence.smoothingFn ↑n
<VAR>α : Type u_1<VAR>Fintype α<VAR>Nonempty α<VAR>T : ℕ → ℝ<VAR>g : ℝ → ℝ<VAR>a b : α → ℝ<VAR>r : α → ℕ → ℕ<VAR>R : AkraBazziRecurrence T g a b r<GOAL>∀ᶠ (n : ℕ) in Filter.atTop, ∀ (i : α), 0 < 1 + AkraBazziRecurrence.smoothingFn ↑(r i n)
<GOAL>∀ᶠ (n : ℕ) in Filter.atTop, 0 ≤ 1 + AkraBazziRecurrence.smoothingFn ↑n
<GOAL>StrictAntiOn AkraBazziRecurrence.smoothingFn (Set.Ioi 1)
<GOAL>StrictMonoOn (fun x => 1 - AkraBazziRecurrence.smoothingFn x) (Set.Ioi 1)
<GOAL>StrictAntiOn (fun x => 1 + AkraBazziRecurrence.smoothingFn x) (Set.Ioi 1)
<VAR>α : Type u_1<VAR>Fintype α<VAR>Nonempty α<VAR>T : ℕ → ℝ<VAR>g : ℝ → ℝ<VAR>a b : α → ℝ<VAR>r : α → ℕ → ℕ<VAR>R : AkraBazziRecurrence T g a b r<VAR>i : α<GOAL>(fun n => AkraBazziRecurrence.smoothingFn (b i * ↑n) - AkraBazziRecurrence.smoothingFn ↑n) ~[Filter.atTop] fun n => -Real.log (b i) / Real.log ↑n ^ 2
<VAR>α : Type u_1<VAR>Fintype α<VAR>Nonempty α<VAR>T : ℕ → ℝ<VAR>g : ℝ → ℝ<VAR>a b : α → ℝ<VAR>r : α → ℕ → ℕ<VAR>R : AkraBazziRecurrence T g a b r<VAR>i : α<GOAL>(fun n => AkraBazziRecurrence.smoothingFn (b i * ↑n) - AkraBazziRecurrence.smoothingFn ↑n) =Θ[Filter.atTop] fun n => 1 / Real.log ↑n ^ 2
<VAR>α : Type u_1<VAR>Fintype α<VAR>Nonempty α<VAR>T : ℕ → ℝ<VAR>g : ℝ → ℝ<VAR>a b : α → ℝ<VAR>r : α → ℕ → ℕ<VAR>R : AkraBazziRecurrence T g a b r<GOAL>Continuous fun p => ∑ i : α, a i * b i ^ p
<VAR>α : Type u_1<VAR>Fintype α<VAR>Nonempty α<VAR>T : ℕ → ℝ<VAR>g : ℝ → ℝ<VAR>a b : α → ℝ<VAR>r : α → ℕ → ℕ<VAR>R : AkraBazziRecurrence T g a b r<GOAL>StrictAnti fun p => ∑ i : α, a i * b i ^ p
<VAR>α : Type u_1<VAR>Fintype α<VAR>Nonempty α<VAR>T : ℕ → ℝ<VAR>g : ℝ → ℝ<VAR>a b : α → ℝ<VAR>r : α → ℕ → ℕ<VAR>R : AkraBazziRecurrence T g a b r<GOAL>Filter.Tendsto (fun p => ∑ i : α, a i * b i ^ p) Filter.atTop (𝓝 0)
<VAR>α : Type u_1<VAR>Fintype α<VAR>Nonempty α<VAR>T : ℕ → ℝ<VAR>g : ℝ → ℝ<VAR>a b : α → ℝ<VAR>r : α → ℕ → ℕ<VAR>R : AkraBazziRecurrence T g a b r<GOAL>Filter.Tendsto (fun p => ∑ i : α, a i * b i ^ p) Filter.atBot Filter.atTop
<VAR>α : Type u_1<VAR>Fintype α<VAR>Nonempty α<VAR>T : ℕ → ℝ<VAR>g : ℝ → ℝ<VAR>a b : α → ℝ<VAR>r : α → ℕ → ℕ<VAR>R : AkraBazziRecurrence T g a b r<GOAL>1 ∈ Set.range fun p => ∑ i : α, a i * b i ^ p
<VAR>α : Type u_1<VAR>Fintype α<VAR>Nonempty α<VAR>T : ℕ → ℝ<VAR>g : ℝ → ℝ<VAR>a b : α → ℝ<VAR>r : α → ℕ → ℕ<VAR>R : AkraBazziRecurrence T g a b r<GOAL>Function.Injective fun p => ∑ i : α, a i * b i ^ p
<VAR>α : Type u_2<VAR>Fintype α<VAR>a b : α → ℝ<GOAL>AkraBazziRecurrence.p a b = Function.invFun (fun p => ∑ i : α, a i * b i ^ p) 1
<VAR>α : Type u_1<VAR>Fintype α<VAR>Nonempty α<VAR>T : ℕ → ℝ<VAR>g : ℝ → ℝ<VAR>a b : α → ℝ<VAR>r : α → ℕ → ℕ<VAR>R : AkraBazziRecurrence T g a b r<GOAL>∑ i : α, a i * b i ^ AkraBazziRecurrence.p a b = 1
<VAR>p : ℝ<VAR>g : ℝ → ℝ<VAR>n₀ n : ℕ<GOAL>AkraBazziRecurrence.sumTransform p g n₀ n = ↑n ^ p * ∑ u ∈ Finset.Ico n₀ n, g ↑u / ↑u ^ (p + 1)
<VAR>α : Type u_1<VAR>Fintype α<VAR>g : ℝ → ℝ<VAR>a b : α → ℝ<VAR>n : ℕ<GOAL>AkraBazziRecurrence.asympBound g a b n = ↑n ^ AkraBazziRecurrence.p a b + AkraBazziRecurrence.sumTransform (AkraBazziRecurrence.p a b) g 0 n
<VAR>α : Type u_1<VAR>Fintype α<VAR>g : ℝ → ℝ<VAR>a b : α → ℝ<VAR>n : ℕ<GOAL>AkraBazziRecurrence.asympBound g a b n = ↑n ^ AkraBazziRecurrence.p a b * (1 + ∑ u ∈ Finset.range n, g ↑u / ↑u ^ (AkraBazziRecurrence.p a b + 1))
<VAR>α : Type u_1<VAR>Fintype α<VAR>Nonempty α<VAR>T : ℕ → ℝ<VAR>g : ℝ → ℝ<VAR>a b : α → ℝ<VAR>r : α → ℕ → ℕ<VAR>R : AkraBazziRecurrence T g a b r<VAR>n : ℕ<VAR>hn : 0 < n<GOAL>0 < AkraBazziRecurrence.asympBound g a b n
<VAR>α : Type u_1<VAR>Fintype α<VAR>Nonempty α<VAR>T : ℕ → ℝ<VAR>g : ℝ → ℝ<VAR>a b : α → ℝ<VAR>r : α → ℕ → ℕ<VAR>R : AkraBazziRecurrence T g a b r<GOAL>∀ᶠ (n : ℕ) in Filter.atTop, 0 < AkraBazziRecurrence.asympBound g a b n
<VAR>α : Type u_1<VAR>Fintype α<VAR>Nonempty α<VAR>T : ℕ → ℝ<VAR>g : ℝ → ℝ<VAR>a b : α → ℝ<VAR>r : α → ℕ → ℕ<VAR>R : AkraBazziRecurrence T g a b r<GOAL>∀ᶠ (n : ℕ) in Filter.atTop, ∀ (i : α), 0 < AkraBazziRecurrence.asympBound g a b (r i n)
<VAR>α : Type u_1<VAR>Fintype α<VAR>Nonempty α<VAR>T : ℕ → ℝ<VAR>g : ℝ → ℝ<VAR>a b : α → ℝ<VAR>r : α → ℕ → ℕ<VAR>R : AkraBazziRecurrence T g a b r<GOAL>∃ c > 0, ∀ᶠ (n : ℕ) in Filter.atTop, ∀ (i : α), AkraBazziRecurrence.sumTransform (AkraBazziRecurrence.p a b) g (r i n) n ≤ c * g ↑n
<VAR>α : Type u_1<VAR>Fintype α<VAR>Nonempty α<VAR>T : ℕ → ℝ<VAR>g : ℝ → ℝ<VAR>a b : α → ℝ<VAR>r : α → ℕ → ℕ<VAR>R : AkraBazziRecurrence T g a b r<GOAL>∃ c > 0, ∀ᶠ (n : ℕ) in Filter.atTop, ∀ (i : α), c * g ↑n ≤ AkraBazziRecurrence.sumTransform (AkraBazziRecurrence.p a b) g (r i n) n
<VAR>α : Type u_1<VAR>Fintype α<VAR>Nonempty α<VAR>T : ℕ → ℝ<VAR>g : ℝ → ℝ<VAR>a b : α → ℝ<VAR>r : α → ℕ → ℕ<VAR>R : AkraBazziRecurrence T g a b r<VAR>q : ℝ → ℝ<VAR>hq_diff : DifferentiableOn ℝ q (Set.Ioi 1)<VAR>hq_poly : AkraBazziRecurrence.GrowsPolynomially fun x => ‖deriv q x‖<VAR>i : α<GOAL>(fun n => q ↑(r i n) - q (b i * ↑n)) =O[Filter.atTop] fun n => deriv q ↑n * (↑(r i n) - b i * ↑n)
<VAR>p : ℝ<GOAL>(deriv fun z => z ^ p * (1 - AkraBazziRecurrence.smoothingFn z)) =ᶠ[Filter.atTop] fun z => p * z ^ (p - 1) * (1 - AkraBazziRecurrence.smoothingFn z) + z ^ (p - 1) / Real.log z ^ 2
<VAR>p : ℝ<GOAL>(deriv fun z => z ^ p * (1 + AkraBazziRecurrence.smoothingFn z)) =ᶠ[Filter.atTop] fun z => p * z ^ (p - 1) * (1 + AkraBazziRecurrence.smoothingFn z) - z ^ (p - 1) / Real.log z ^ 2
<VAR>p : ℝ<VAR>hp : p ≠ 0<GOAL>(deriv fun z => z ^ p * (1 - AkraBazziRecurrence.smoothingFn z)) ~[Filter.atTop] fun z => p * z ^ (p - 1)
<VAR>p : ℝ<VAR>hp : p ≠ 0<GOAL>(deriv fun z => z ^ p * (1 + AkraBazziRecurrence.smoothingFn z)) ~[Filter.atTop] fun z => p * z ^ (p - 1)
<VAR>p : ℝ<VAR>hp : p ≠ 0<GOAL>(fun x => ‖deriv (fun z => z ^ p * (1 - AkraBazziRecurrence.smoothingFn z)) x‖) =Θ[Filter.atTop] fun z => z ^ (p - 1)
<VAR>p : ℝ<VAR>hp : p ≠ 0<GOAL>(fun x => ‖deriv (fun z => z ^ p * (1 + AkraBazziRecurrence.smoothingFn z)) x‖) =Θ[Filter.atTop] fun z => z ^ (p - 1)
<VAR>p : ℝ<GOAL>AkraBazziRecurrence.GrowsPolynomially fun x => ‖deriv (fun z => z ^ p * (1 - AkraBazziRecurrence.smoothingFn z)) x‖
<VAR>p : ℝ<GOAL>AkraBazziRecurrence.GrowsPolynomially fun x => ‖deriv (fun z => z ^ p * (1 + AkraBazziRecurrence.smoothingFn z)) x‖
<VAR>α : Type u_1<VAR>Fintype α<VAR>Nonempty α<VAR>T : ℕ → ℝ<VAR>g : ℝ → ℝ<VAR>a b : α → ℝ<VAR>r : α → ℕ → ℕ<VAR>R : AkraBazziRecurrence T g a b r<GOAL>∀ᶠ (n : ℕ) in Filter.atTop, ∀ (i : α), ↑(r i n) ^ AkraBazziRecurrence.p a b * (1 - AkraBazziRecurrence.smoothingFn ↑(r i n)) ≤ b i ^ AkraBazziRecurrence.p a b * ↑n ^ AkraBazziRecurrence.p a b * (1 - AkraBazziRecurrence.smoothingFn ↑n)
<VAR>α : Type u_1<VAR>Fintype α<VAR>Nonempty α<VAR>T : ℕ → ℝ<VAR>g : ℝ → ℝ<VAR>a b : α → ℝ<VAR>r : α → ℕ → ℕ<VAR>R : AkraBazziRecurrence T g a b r<GOAL>∀ᶠ (n : ℕ) in Filter.atTop, ∀ (i : α), b i ^ AkraBazziRecurrence.p a b * ↑n ^ AkraBazziRecurrence.p a b * (1 + AkraBazziRecurrence.smoothingFn ↑n) ≤ ↑(r i n) ^ AkraBazziRecurrence.p a b * (1 + AkraBazziRecurrence.smoothingFn ↑(r i n))
<VAR>α : Type u_1<VAR>Fintype α<VAR>Nonempty α<VAR>T : ℕ → ℝ<VAR>g : ℝ → ℝ<VAR>a b : α → ℝ<VAR>r : α → ℕ → ℕ<VAR>R : AkraBazziRecurrence T g a b r<VAR>n : ℕ<VAR>hn : 0 < n<GOAL>(Finset.Ico ⌊b (AkraBazziRecurrence.min_bi b) / 2 * ↑n⌋₊ n).Nonempty
<VAR>α : Type u_1<VAR>Fintype α<VAR>Nonempty α<VAR>T : ℕ → ℝ<VAR>g : ℝ → ℝ<VAR>a b : α → ℝ<VAR>r : α → ℕ → ℕ<VAR>R : AkraBazziRecurrence T g a b r<GOAL>T =O[Filter.atTop] fun n => (1 - AkraBazziRecurrence.smoothingFn ↑n) * AkraBazziRecurrence.asympBound g a b n
<VAR>α : Type u_1<VAR>Fintype α<VAR>Nonempty α<VAR>T : ℕ → ℝ<VAR>g : ℝ → ℝ<VAR>a b : α → ℝ<VAR>r : α → ℕ → ℕ<VAR>R : AkraBazziRecurrence T g a b r<GOAL>(fun n => (1 + AkraBazziRecurrence.smoothingFn ↑n) * AkraBazziRecurrence.asympBound g a b n) =O[Filter.atTop] T
<VAR>α : Type u_1<VAR>Fintype α<VAR>Nonempty α<VAR>T : ℕ → ℝ<VAR>g : ℝ → ℝ<VAR>a b : α → ℝ<VAR>r : α → ℕ → ℕ<VAR>R : AkraBazziRecurrence T g a b r<GOAL>T =O[Filter.atTop] AkraBazziRecurrence.asympBound g a b
<VAR>α : Type u_1<VAR>Fintype α<VAR>Nonempty α<VAR>T : ℕ → ℝ<VAR>g : ℝ → ℝ<VAR>a b : α → ℝ<VAR>r : α → ℕ → ℕ<VAR>R : AkraBazziRecurrence T g a b r<GOAL>AkraBazziRecurrence.asympBound g a b =O[Filter.atTop] T
<VAR>α : Type u_1<VAR>Fintype α<VAR>Nonempty α<VAR>T : ℕ → ℝ<VAR>g : ℝ → ℝ<VAR>a b : α → ℝ<VAR>r : α → ℕ → ℕ<VAR>R : AkraBazziRecurrence T g a b r<GOAL>T =Θ[Filter.atTop] AkraBazziRecurrence.asympBound g a b
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<GOAL>((Polynomial.cyclotomic p ℤ).comp (Polynomial.X + 1)).IsEisensteinAt (Submodule.span ℤ {↑p})
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>n : ℕ<GOAL>((Polynomial.cyclotomic (p ^ (n + 1)) ℤ).comp (Polynomial.X + 1)).IsEisensteinAt (Submodule.span ℤ {↑p})
<VAR>R : Type u<VAR>K : Type v<VAR>L : Type z<VAR>p : R<VAR>CommRing R<VAR>Field K<VAR>Field L<VAR>Algebra K L<VAR>Algebra R L<VAR>Algebra R K<VAR>IsScalarTower R K L<VAR>Algebra.IsSeparable K L<VAR>IsDomain R<VAR>IsFractionRing R K<VAR>IsIntegrallyClosed R<VAR>B : PowerBasis K L<VAR>hp : Prime p<VAR>hBint : IsIntegral R B.gen<VAR>z : L<VAR>Q : R[X]<VAR>hQ : (Polynomial.aeval B.gen) Q = p • z<VAR>hzint : IsIntegral R z<VAR>hei : (minpoly R B.gen).IsEisensteinAt (Submodule.span R {p})<GOAL>p ∣ Q.coeff 0
<VAR>A : Type u_1<VAR>B : Type u_2<VAR>CommSemiring A<VAR>CommRing B<VAR>Algebra A B<VAR>NoZeroSMulDivisors A B<VAR>Q : A[X]<VAR>p : A<VAR>x z : B<VAR>hp : p ≠ 0<VAR>hQ : ∀ i ∈ Finset.range (Q.natDegree + 1), p ∣ Q.coeff i<VAR>hz : (Polynomial.aeval x) Q = p • z<GOAL>z ∈ Algebra.adjoin A {x}
<VAR>R : Type u<VAR>K : Type v<VAR>L : Type z<VAR>p : R<VAR>CommRing R<VAR>Field K<VAR>Field L<VAR>Algebra K L<VAR>Algebra R L<VAR>Algebra R K<VAR>IsScalarTower R K L<VAR>Algebra.IsSeparable K L<VAR>IsDomain R<VAR>IsFractionRing R K<VAR>IsIntegrallyClosed R<VAR>B : PowerBasis K L<VAR>hp : Prime p<VAR>hBint : IsIntegral R B.gen<VAR>z : L<VAR>hzint : IsIntegral R z<VAR>hz : p • z ∈ Algebra.adjoin R {B.gen}<VAR>hei : (minpoly R B.gen).IsEisensteinAt (Submodule.span R {p})<GOAL>z ∈ Algebra.adjoin R {B.gen}
<VAR>R : Type u<VAR>K : Type v<VAR>L : Type z<VAR>p : R<VAR>CommRing R<VAR>Field K<VAR>Field L<VAR>Algebra K L<VAR>Algebra R L<VAR>Algebra R K<VAR>IsScalarTower R K L<VAR>Algebra.IsSeparable K L<VAR>IsDomain R<VAR>IsFractionRing R K<VAR>IsIntegrallyClosed R<VAR>B : PowerBasis K L<VAR>hp : Prime p<VAR>hBint : IsIntegral R B.gen<VAR>n : ℕ<VAR>z : L<VAR>hzint : IsIntegral R z<VAR>hz : p ^ n • z ∈ Algebra.adjoin R {B.gen}<VAR>hei : (minpoly R B.gen).IsEisensteinAt (Submodule.span R {p})<GOAL>z ∈ Algebra.adjoin R {B.gen}