awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.LSeries.AbstractFuncEq
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
P : WeakFEPair E
r C : ℝ
hC :
  ∀ᶠ (x : ℝ) in 𝓝 0,
    Membership.mem (γ := Set ℝ) (Ioi 0) x →
      Norm.norm.{u_1} (E := E) (((fun (x : ℝ) ↦ P.g x - P.g₀) ∘ fun (x : ℝ) ↦ x⁻¹) x) ≤
        C * Norm.norm (E := ℝ) (((fun (x : ℝ) ↦ x ^ (-(r + P.k))) ∘ fun (x : ℝ) ↦ x⁻¹) x)
x : ℝ
hx : 0 < x
h_nv2 : (↑(x ^ P.k) : ℂ) ≠ 0
h_nv : P.ε⁻¹ * (↑(x ^ P.k) : ℂ) ≠ 0
hC' :
  Norm.norm.{u_1} (E := E) (((fun (x : ℝ) ↦ P.g x - P.g₀) ∘ fun (x : ℝ) ↦ x⁻¹) x) ≤
    C * Norm.norm (E := ℝ) (((fun (x : ℝ) ↦ x ^ (-(r + P.k))) ∘ fun (x : ℝ) ↦ x⁻¹) x)
⊢ ‖(P.ε⁻¹ * (↑(x ^ P.k) : ℂ)) • P.f x - P.g₀‖ ≤ C * ‖(1 / x) ^ (-(r + P.k))‖

Tactic:
simp_rw [Function.comp_apply, ← one_div, P.h_feq' _ hx] at hC'

Premises used: WeakFEPair.h_feq', one_div, Function.comp_apply
-- Module: Mathlib.NumberTheory.LSeries.AbstractFuncEq
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
P : WeakFEPair E
r C : ℝ
hC :
  ∀ᶠ (x : ℝ) in 𝓝 0,
    Membership.mem (γ := Set ℝ) (Ioi 0) x →
      Norm.norm.{u_1} (E := E) (((fun (x : ℝ) ↦ P.g x - P.g₀) ∘ fun (x : ℝ) ↦ x⁻¹) x) ≤
        C * Norm.norm (E := ℝ) (((fun (x : ℝ) ↦ x ^ (-(r + P.k))) ∘ fun (x : ℝ) ↦ x⁻¹) x)
x : ℝ
hx : 0 < x
h_nv2 : (↑(x ^ P.k) : ℂ) ≠ 0
h_nv : P.ε⁻¹ * (↑(x ^ P.k) : ℂ) ≠ 0
hC' : ‖(P.ε⁻¹ * (↑(x ^ P.k) : ℂ)) • P.f x - P.g₀‖ ≤ C * ‖(1 / x) ^ (-(r + P.k))‖
⊢ ‖P.f x - (P.ε⁻¹ * (↑(x ^ P.k) : ℂ))⁻¹ • P.g₀‖ ≤ C * ‖(1 / x) ^ (-(r + P.k))‖ / ‖P.ε⁻¹ * (↑(x ^ P.k) : ℂ)‖

Tactic:
rw [← ((mul_inv_cancel₀ h_nv).symm ▸ one_smul ℂ P.g₀ :), mul_smul _ _ P.g₀, ← smul_sub, norm_smul,
    ← le_div_iff₀' (lt_of_le_of_ne (norm_nonneg _) (norm_ne_zero_iff.mpr h_nv).symm)] at hC'

Premises used: Iff.mpr, le_div_iff₀', norm_smul, Ne.symm, WeakFEPair.g₀, smul_sub, norm_ne_zero_iff, norm_nonneg, SemigroupAction.mul_smul, lt_of_le_of_ne
-- Module: Mathlib.NumberTheory.LSeries.AbstractFuncEq
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
P : WeakFEPair E
r C : ℝ
hC :
  ∀ᶠ (x : ℝ) in 𝓝 0,
    Membership.mem (γ := Set ℝ) (Ioi 0) x →
      Norm.norm.{u_1} (E := E) (((fun (x : ℝ) ↦ P.g x - P.g₀) ∘ fun (x : ℝ) ↦ x⁻¹) x) ≤
        C * Norm.norm (E := ℝ) (((fun (x : ℝ) ↦ x ^ (-(r + P.k))) ∘ fun (x : ℝ) ↦ x⁻¹) x)
x : ℝ
hx : 0 < x
h_nv2 : (↑(x ^ P.k) : ℂ) ≠ 0
h_nv : P.ε⁻¹ * (↑(x ^ P.k) : ℂ) ≠ 0
hC' : ‖P.f x - (P.ε⁻¹ * (↑(x ^ P.k) : ℂ))⁻¹ • P.g₀‖ ≤ C * ‖(1 / x) ^ (-(r + P.k))‖ / ‖P.ε⁻¹ * (↑(x ^ P.k) : ℂ)‖
⊢ ‖P.f x - (P.ε⁻¹ * (↑(x ^ P.k) : ℂ))⁻¹ • P.g₀‖ ≤ C * ‖(1 / x) ^ (-(r + P.k))‖ / ‖P.ε⁻¹ * (↑(x ^ P.k) : ℂ)‖

Tactic:
hC'
-- Module: Mathlib.NumberTheory.LSeries.AbstractFuncEq
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
P : WeakFEPair E
r C : ℝ
hC :
  ∀ᶠ (x : ℝ) in 𝓝 0,
    Membership.mem (γ := Set ℝ) (Ioi 0) x →
      Norm.norm.{u_1} (E := E) (((fun (x : ℝ) ↦ P.g x - P.g₀) ∘ fun (x : ℝ) ↦ x⁻¹) x) ≤
        C * Norm.norm (E := ℝ) (((fun (x : ℝ) ↦ x ^ (-(r + P.k))) ∘ fun (x : ℝ) ↦ x⁻¹) x)
x : ℝ
hx : 0 < x
h_nv2 : (↑(x ^ P.k) : ℂ) ≠ 0
h_nv : P.ε⁻¹ * (↑(x ^ P.k) : ℂ) ≠ 0
hC' : ‖P.f x - (P.ε⁻¹ * (↑(x ^ P.k) : ℂ))⁻¹ • P.g₀‖ ≤ C * ‖(1 / x) ^ (-(r + P.k))‖ / ‖P.ε⁻¹ * (↑(x ^ P.k) : ℂ)‖
h : ‖P.f x - (P.ε * (↑(x ^ (-P.k)) : ℂ)) • P.g₀‖ = ‖P.f x - (P.ε⁻¹ * (↑(x ^ P.k) : ℂ))⁻¹ • P.g₀‖
h₁ : ‖P.ε‖ * C * ‖x ^ r‖ = C * ‖(1 / x) ^ (-(r + P.k))‖ / ‖P.ε⁻¹ * (↑(x ^ P.k) : ℂ)‖
⊢ ‖P.f x - (P.ε * (↑(x ^ (-P.k)) : ℂ)) • P.g₀‖ ≤ ‖P.ε‖ * C * ‖x ^ r‖

Tactic:
convert! hC' using 1
-- Module: Mathlib.NumberTheory.LSeries.AbstractFuncEq
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
P : WeakFEPair E
r C : ℝ
hC :
  ∀ᶠ (x : ℝ) in 𝓝 0,
    Membership.mem (γ := Set ℝ) (Ioi 0) x →
      Norm.norm.{u_1} (E := E) (((fun (x : ℝ) ↦ P.g x - P.g₀) ∘ fun (x : ℝ) ↦ x⁻¹) x) ≤
        C * Norm.norm (E := ℝ) (((fun (x : ℝ) ↦ x ^ (-(r + P.k))) ∘ fun (x : ℝ) ↦ x⁻¹) x)
x : ℝ
hx : 0 < x
h_nv2 : (↑(x ^ P.k) : ℂ) ≠ 0
h_nv : P.ε⁻¹ * (↑(x ^ P.k) : ℂ) ≠ 0
hC' : ‖P.f x - (P.ε⁻¹ * (↑(x ^ P.k) : ℂ))⁻¹ • P.g₀‖ ≤ C * ‖(1 / x) ^ (-(r + P.k))‖ / ‖P.ε⁻¹ * (↑(x ^ P.k) : ℂ)‖
h : P.ε * (↑(x ^ (-P.k)) : ℂ) = (P.ε⁻¹ * (↑(x ^ P.k) : ℂ))⁻¹
⊢ ‖P.f x - (P.ε * (↑(x ^ (-P.k)) : ℂ)) • P.g₀‖ = ‖P.f x - (P.ε⁻¹ * (↑(x ^ P.k) : ℂ))⁻¹ • P.g₀‖

Tactic:
congr 3
-- Module: Mathlib.NumberTheory.LSeries.AbstractFuncEq
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
P : WeakFEPair E
r C : ℝ
hC :
  ∀ᶠ (x : ℝ) in 𝓝 0,
    Membership.mem (γ := Set ℝ) (Ioi 0) x →
      Norm.norm.{u_1} (E := E) (((fun (x : ℝ) ↦ P.g x - P.g₀) ∘ fun (x : ℝ) ↦ x⁻¹) x) ≤
        C * Norm.norm (E := ℝ) (((fun (x : ℝ) ↦ x ^ (-(r + P.k))) ∘ fun (x : ℝ) ↦ x⁻¹) x)
x : ℝ
hx : 0 < x
h_nv2 : (↑(x ^ P.k) : ℂ) ≠ 0
h_nv : P.ε⁻¹ * (↑(x ^ P.k) : ℂ) ≠ 0
hC' : ‖P.f x - (P.ε⁻¹ * (↑(x ^ P.k) : ℂ))⁻¹ • P.g₀‖ ≤ C * ‖(1 / x) ^ (-(r + P.k))‖ / ‖P.ε⁻¹ * (↑(x ^ P.k) : ℂ)‖
h : P.ε * (↑(x ^ P.k)⁻¹ : ℂ) = (P.ε⁻¹ * (↑(x ^ P.k) : ℂ))⁻¹
⊢ P.ε * (↑(x ^ (-P.k)) : ℂ) = (P.ε⁻¹ * (↑(x ^ P.k) : ℂ))⁻¹

Tactic:
rw [rpow_neg hx.le]

Premises used: LT.lt.le, Real.rpow_neg
-- Module: Mathlib.NumberTheory.LSeries.AbstractFuncEq
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
P : WeakFEPair E
r C : ℝ
hC :
  ∀ᶠ (x : ℝ) in 𝓝 0,
    Membership.mem (γ := Set ℝ) (Ioi 0) x →
      Norm.norm.{u_1} (E := E) (((fun (x : ℝ) ↦ P.g x - P.g₀) ∘ fun (x : ℝ) ↦ x⁻¹) x) ≤
        C * Norm.norm (E := ℝ) (((fun (x : ℝ) ↦ x ^ (-(r + P.k))) ∘ fun (x : ℝ) ↦ x⁻¹) x)
x : ℝ
hx : 0 < x
h_nv2 : (↑(x ^ P.k) : ℂ) ≠ 0
h_nv : P.ε⁻¹ * (↑(x ^ P.k) : ℂ) ≠ 0
hC' : ‖P.f x - (P.ε⁻¹ * (↑(x ^ P.k) : ℂ))⁻¹ • P.g₀‖ ≤ C * ‖(1 / x) ^ (-(r + P.k))‖ / ‖P.ε⁻¹ * (↑(x ^ P.k) : ℂ)‖
⊢ P.ε * (↑(x ^ P.k)⁻¹ : ℂ) = (P.ε⁻¹ * (↑(x ^ P.k) : ℂ))⁻¹

Tactic:
simp [field]
-- Module: Mathlib.NumberTheory.LSeries.AbstractFuncEq
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
P : WeakFEPair E
r C : ℝ
hC :
  ∀ᶠ (x : ℝ) in 𝓝 0,
    Membership.mem (γ := Set ℝ) (Ioi 0) x →
      Norm.norm.{u_1} (E := E) (((fun (x : ℝ) ↦ P.g x - P.g₀) ∘ fun (x : ℝ) ↦ x⁻¹) x) ≤
        C * Norm.norm (E := ℝ) (((fun (x : ℝ) ↦ x ^ (-(r + P.k))) ∘ fun (x : ℝ) ↦ x⁻¹) x)
x : ℝ
hx : 0 < x
h_nv2 : (↑(x ^ P.k) : ℂ) ≠ 0
h_nv : P.ε⁻¹ * (↑(x ^ P.k) : ℂ) ≠ 0
hC' : ‖P.f x - (P.ε⁻¹ * (↑(x ^ P.k) : ℂ))⁻¹ • P.g₀‖ ≤ C * ‖(1 / x) ^ (-(r + P.k))‖ / ‖P.ε⁻¹ * (↑(x ^ P.k) : ℂ)‖
h : ‖P.ε‖ * C * x ^ r = C * (x ^ r * x ^ P.k) / (‖P.ε‖⁻¹ * x ^ P.k)
⊢ ‖P.ε‖ * C * ‖x ^ r‖ = C * ‖(1 / x) ^ (-(r + P.k))‖ / ‖P.ε⁻¹ * (↑(x ^ P.k) : ℂ)‖

Tactic:
simp_rw [norm_mul, norm_real, one_div, inv_rpow hx.le, rpow_neg hx.le, inv_inv, norm_inv,
      norm_of_nonneg (rpow_pos_of_pos hx _).le, rpow_add hx]

Premises used: Real.rpow_pos_of_pos, Real.inv_rpow, LT.lt.le, norm_mul, Complex.norm_real, norm_inv, inv_inv, one_div, Real.rpow_add, Real.rpow_neg, Real.norm_of_nonneg
-- Module: Mathlib.NumberTheory.LSeries.AbstractFuncEq
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
P : WeakFEPair E
r C : ℝ
hC :
  ∀ᶠ (x : ℝ) in 𝓝 0,
    Membership.mem (γ := Set ℝ) (Ioi 0) x →
      Norm.norm.{u_1} (E := E) (((fun (x : ℝ) ↦ P.g x - P.g₀) ∘ fun (x : ℝ) ↦ x⁻¹) x) ≤
        C * Norm.norm (E := ℝ) (((fun (x : ℝ) ↦ x ^ (-(r + P.k))) ∘ fun (x : ℝ) ↦ x⁻¹) x)
x : ℝ
hx : 0 < x
h_nv2 : (↑(x ^ P.k) : ℂ) ≠ 0
h_nv : P.ε⁻¹ * (↑(x ^ P.k) : ℂ) ≠ 0
hC' : ‖P.f x - (P.ε⁻¹ * (↑(x ^ P.k) : ℂ))⁻¹ • P.g₀‖ ≤ C * ‖(1 / x) ^ (-(r + P.k))‖ / ‖P.ε⁻¹ * (↑(x ^ P.k) : ℂ)‖
⊢ ‖P.ε‖ * C * x ^ r = C * (x ^ r * x ^ P.k) / (‖P.ε‖⁻¹ * x ^ P.k)

Tactic:
field
-- Module: Mathlib.NumberTheory.LSeries.AbstractFuncEq
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
P : WeakFEPair E
simp_rw :
  IsBigO.{0, u_1, 0} (E := E) (F := ℝ) (𝓝[>] 0)
    (fun (x : ℝ) ↦ P.f x - (P.ε * (↑(x ^ (-P.k)) : ℂ)) • P.g₀ + ((P.ε * (↑(x ^ (-P.k)) : ℂ)) • P.g₀ - P.f₀))
    fun (x : ℝ) ↦ x ^ (-P.k)
⊢ IsBigO.{0, u_1, 0} (E := E) (F := ℝ) (𝓝[>] 0) (fun (x : ℝ) ↦ P.f x - P.f₀) fun (x : ℝ) ↦ x ^ (-P.k)

Tactic:
simp_rw [← fun x ↦ sub_add_sub_cancel (P.f x) ((P.ε * ↑(x ^ (-P.k))) • P.g₀) P.f₀]

Premises used: sub_add_sub_cancel, HMul.hMul, WeakFEPair.f, WeakFEPair.ε, WeakFEPair.g₀, WeakFEPair.f₀, Complex.ofReal, HPow.hPow, WeakFEPair.k, HSMul.hSMul, Neg.neg
-- Module: Mathlib.NumberTheory.LSeries.AbstractFuncEq
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
P : WeakFEPair E
⊢ IsBigO.{0, u_1, 0} (E := E) (F := ℝ) (𝓝[>] 0)
    (fun (x : ℝ) ↦ P.f x - (P.ε * (↑(x ^ (-P.k)) : ℂ)) • P.g₀ + ((P.ε * (↑(x ^ (-P.k)) : ℂ)) • P.g₀ - P.f₀))
    fun (x : ℝ) ↦ x ^ (-P.k)

Tactic:
(P.hf_zero _).add (IsBigO.sub ?_ ?_)

Premises used: Asymptotics.IsBigO.sub, Asymptotics.IsBigO.add, WeakFEPair.hf_zero
-- Module: Mathlib.NumberTheory.LSeries.AbstractFuncEq
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
P : WeakFEPair E
refine_1 :
  IsBigO.{0, u_1, 0} (E := E) (F := ℝ) (𝓝[>] 0) (fun (x : ℝ) ↦ (P.ε * (↑(x ^ (-P.k)) : ℂ)) • P.g₀) fun (x : ℝ) ↦
    x ^ (-P.k)
refine_2 : IsBigO.{0, u_1, 0} (E := E) (F := ℝ) (𝓝[>] 0) (fun (x : ℝ) ↦ P.f₀) fun (x : ℝ) ↦ x ^ (-P.k)
⊢ IsBigO.{0, u_1, 0} (E := E) (F := ℝ) (𝓝[>] 0)
    (fun (x : ℝ) ↦ P.f x - (P.ε * (↑(x ^ (-P.k)) : ℂ)) • P.g₀ + ((P.ε * (↑(x ^ (-P.k)) : ℂ)) • P.g₀ - P.f₀))
    fun (x : ℝ) ↦ x ^ (-P.k)

Tactic:
refine (P.hf_zero _).add (IsBigO.sub ?_ ?_)

Premises used: Asymptotics.IsBigO.sub, Asymptotics.IsBigO.add, WeakFEPair.hf_zero
-- Module: Mathlib.NumberTheory.LSeries.AbstractFuncEq
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
P : WeakFEPair E
refine_1 :
  IsBigO (E := ℝ) (F := ℝ) (𝓝[>] 0) (fun (x : ℝ) ↦ ‖(P.ε * (↑(x ^ (-P.k)) : ℂ)) • P.g₀‖) fun (x : ℝ) ↦ ‖x ^ (-P.k)‖
⊢ IsBigO.{0, u_1, 0} (E := E) (F := ℝ) (𝓝[>] 0) (fun (x : ℝ) ↦ (P.ε * (↑(x ^ (-P.k)) : ℂ)) • P.g₀) fun (x : ℝ) ↦
    x ^ (-P.k)

Tactic:
rw [← isBigO_norm_norm]

Premises used: Asymptotics.isBigO_norm_norm
-- Module: Mathlib.NumberTheory.LSeries.AbstractFuncEq
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
P : WeakFEPair E
refine_1 : IsBigO (E := ℝ) (F := ℝ) (𝓝[>] 0) (fun (x : ℝ) ↦ ‖P.ε‖ * ‖P.g₀‖ * ‖x ^ (-P.k)‖) fun (x : ℝ) ↦ ‖x ^ (-P.k)‖
⊢ IsBigO (E := ℝ) (F := ℝ) (𝓝[>] 0) (fun (x : ℝ) ↦ ‖(P.ε * (↑(x ^ (-P.k)) : ℂ)) • P.g₀‖) fun (x : ℝ) ↦ ‖x ^ (-P.k)‖

Tactic:
simp_rw [mul_smul, norm_smul, mul_comm _ ‖P.g₀‖, ← mul_assoc, norm_real]

Premises used: Norm.norm, norm_smul, mul_assoc, Complex.norm_real, WeakFEPair.g₀, mul_comm, SemigroupAction.mul_smul
-- Module: Mathlib.NumberTheory.LSeries.AbstractFuncEq
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
P : WeakFEPair E
⊢ IsBigO (E := ℝ) (F := ℝ) (𝓝[>] 0) (fun (x : ℝ) ↦ ‖P.ε‖ * ‖P.g₀‖ * ‖x ^ (-P.k)‖) fun (x : ℝ) ↦ ‖x ^ (-P.k)‖

Tactic:
apply (isBigO_refl _ _).const_mul_left

Premises used: Asymptotics.IsBigO.const_mul_left, Asymptotics.isBigO_refl
-- Module: Mathlib.NumberTheory.LSeries.AbstractFuncEq
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
P : WeakFEPair E
⊢ IsBigO.{0, u_1, 0} (E := E) (F := ℝ) (𝓝[>] 0) (fun (x : ℝ) ↦ P.f₀) fun (x : ℝ) ↦ x ^ (-P.k)

Tactic:
IsBigO.of_bound ‖P.f₀‖ (eventually_nhdsWithin_iff.mpr ?_)

Premises used: Iff.mpr, Norm.norm, WeakFEPair.f₀, eventually_nhdsWithin_iff, Asymptotics.IsBigO.of_bound
-- Module: Mathlib.NumberTheory.LSeries.AbstractFuncEq
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
P : WeakFEPair E
refine_2 : ∀ᶠ (x : ℝ) in 𝓝 0, Membership.mem (γ := Set ℝ) (Ioi 0) x → ‖P.f₀‖ ≤ ‖P.f₀‖ * ‖x ^ (-P.k)‖
⊢ IsBigO.{0, u_1, 0} (E := E) (F := ℝ) (𝓝[>] 0) (fun (x : ℝ) ↦ P.f₀) fun (x : ℝ) ↦ x ^ (-P.k)

Tactic:
refine IsBigO.of_bound ‖P.f₀‖ (eventually_nhdsWithin_iff.mpr ?_)

Premises used: Iff.mpr, Norm.norm, WeakFEPair.f₀, eventually_nhdsWithin_iff, Asymptotics.IsBigO.of_bound
-- Module: Mathlib.NumberTheory.LSeries.AbstractFuncEq
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
P : WeakFEPair E
x : ℝ
hx' : x ≤ 1
h : ∀ (hx : 0 < x), ‖P.f₀‖ ≤ ‖P.f₀‖ * ‖x ^ (-P.k)‖
⊢ Membership.mem (γ := Set ℝ) (Ioi 0) x → ‖P.f₀‖ ≤ ‖P.f₀‖ * ‖x ^ (-P.k)‖

Tactic:
(hx : 0 < x)
-- Module: Mathlib.NumberTheory.LSeries.AbstractFuncEq
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
P : WeakFEPair E
h : ∀ (x : ℝ) (hx' : x ≤ 1) (hx : 0 < x), ‖P.f₀‖ ≤ ‖P.f₀‖ * ‖x ^ (-P.k)‖
⊢ ∀ᶠ (x : ℝ) in 𝓝 0, Membership.mem (γ := Set ℝ) (Ioi 0) x → ‖P.f₀‖ ≤ ‖P.f₀‖ * ‖x ^ (-P.k)‖

Tactic:
filter_upwards [eventually_le_nhds zero_lt_one] with x hx' (hx : 0 < x)

Premises used: zero_lt_one, eventually_le_nhds
-- Module: Mathlib.NumberTheory.LSeries.AbstractFuncEq
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
P : WeakFEPair E
x : ℝ
hx' : x ≤ 1
hx : 0 < x
h : 1 ≤ ‖x ^ (-P.k)‖
⊢ ‖P.f₀‖ ≤ ‖P.f₀‖ * ‖x ^ (-P.k)‖

Tactic:
apply le_mul_of_one_le_right (norm_nonneg _)

Premises used: le_mul_of_one_le_right, norm_nonneg
-- Module: Mathlib.NumberTheory.LSeries.AbstractFuncEq
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
P : WeakFEPair E
x : ℝ
hx' : x ≤ 1
hx : 0 < x
h : 1 ≤ (x ^ P.k)⁻¹
⊢ 1 ≤ ‖x ^ (-P.k)‖

Tactic:
rw [norm_of_nonneg (rpow_pos_of_pos hx _).le, rpow_neg hx.le]

Premises used: Real.rpow_pos_of_pos, LT.lt.le, Real.rpow_neg, Real.norm_of_nonneg
-- Module: Mathlib.NumberTheory.LSeries.AbstractFuncEq
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
P : WeakFEPair E
x : ℝ
hx' : x ≤ 1
hx : 0 < x
⊢ 1 ≤ (x ^ P.k)⁻¹

Tactic:
(one_le_inv₀ (rpow_pos_of_pos hx _)).2 (rpow_le_one hx.le hx' P.hk.le)

Premises used: Iff.mpr, Real.rpow_pos_of_pos, one_le_inv₀, WeakFEPair.hk, LT.lt.le, Real.rpow_le_one
-- Module: Mathlib.NumberTheory.LSeries.AbstractFuncEq
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
P : WeakFEPair E
x : ℝ
hx' : x ≤ 1
hx : 0 < x
⊢ 1 ≤ (x ^ P.k)⁻¹

Tactic:
exact (one_le_inv₀ (rpow_pos_of_pos hx _)).2 (rpow_le_one hx.le hx' P.hk.le)

Premises used: Iff.mpr, Real.rpow_pos_of_pos, one_le_inv₀, WeakFEPair.hk, LT.lt.le, Real.rpow_le_one
-- Module: Mathlib.NumberTheory.LSeries.AbstractFuncEq
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
P : StrongFEPair E
r : ℝ
⊢ IsBigO (F := ℝ) atTop P.f fun (x : ℝ) ↦ x ^ r

Tactic:
simpa [P.hf₀] using P.hf_top r

Premises used: StrongFEPair.hf₀, StrongFEPair.toWeakFEPair, WeakFEPair.hf_top
-- Module: Mathlib.NumberTheory.LSeries.AbstractFuncEq
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
P : StrongFEPair E
r : ℝ
⊢ IsBigO (F := ℝ) (𝓝[>] 0) P.f fun (x : ℝ) ↦ x ^ r

Tactic:
simpa using (P.hg₀ ▸ P.hf_zero r :)
-- Module: Mathlib.NumberTheory.LSeries.AbstractFuncEq
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
P : StrongFEPair E
s : ℂ
⊢ HasMellin P.f s (P.Λ s)

Tactic:
let ⟨_, ht⟩ := exists_gt s.re
  let ⟨_, hu⟩ := exists_lt s.re
  ⟨mellinConvergent_of_isBigO_rpow P.hf_int (P.hf_top' _) ht (P.hf_zero' _) hu, rfl⟩

Premises used: WeakFEPair.f, _private.0.StrongFEPair.hasMellin.match_1, StrongFEPair.hf_zero', NoMaxOrder.exists_gt, Complex.re, StrongFEPair.Λ, StrongFEPair.toWeakFEPair, And.intro, NoMinOrder.exists_lt, WeakFEPair.hf_int, StrongFEPair.hf_top', mellinConvergent_of_isBigO_rpow, _private.0.StrongFEPair.hasMellin.match_2, HasMellin, Neg.neg, rfl
-- Module: Mathlib.NumberTheory.LSeries.AbstractFuncEq
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
P : StrongFEPair E
⊢ P.Λ = mellin P.f

Tactic:
rfl

Premises used: StrongFEPair.Λ, rfl
-- Module: Mathlib.NumberTheory.LSeries.AbstractFuncEq
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
P : StrongFEPair E
⊢ P.symm.Λ = mellin P.g

Tactic:
rfl

Premises used: StrongFEPair.Λ, rfl
-- Module: Mathlib.NumberTheory.LSeries.AbstractFuncEq
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
P : StrongFEPair E
⊢ Differentiable ℂ P.Λ

Tactic:
fun s ↦
  let ⟨_, ht⟩ := exists_gt s.re
  let ⟨_, hu⟩ := exists_lt s.re
  mellin_differentiableAt_of_isBigO_rpow P.hf_int (P.hf_top' _) ht (P.hf_zero' _) hu

Premises used: Differentiable, DifferentiableAt, _private.0.StrongFEPair.hasMellin.match_1, StrongFEPair.hf_zero', NoMaxOrder.exists_gt, Complex.re, StrongFEPair.Λ, StrongFEPair.toWeakFEPair, NoMinOrder.exists_lt, WeakFEPair.hf_int, StrongFEPair.hf_top', mellin_differentiableAt_of_isBigO_rpow, Complex, _private.0.StrongFEPair.hasMellin.match_2, Neg.neg
-- Module: Mathlib.NumberTheory.LSeries.AbstractFuncEq
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
P : StrongFEPair E
s : ℂ
rw : mellin P.f ((↑P.k : ℂ) - s) = P.ε • mellin P.g s
⊢ P.Λ ((↑P.k : ℂ) - s) = P.ε • P.symm.Λ s

Tactic:
rw [P.Λ_eq, P.symm_Λ_eq]

Premises used: StrongFEPair.Λ_eq, StrongFEPair.symm_Λ_eq
-- Module: Mathlib.NumberTheory.LSeries.AbstractFuncEq
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
P : StrongFEPair E
s : ℂ
⊢ mellin (fun (t : ℝ) ↦ P.g (HPow.hPow (β := ℝ) t (-1))) (-s) =
    HSMul.hSMul (α := ℝ) |(-1)|⁻¹ (mellin P.g (-s / (↑(-1) : ℂ)))

Tactic:
have step1 := mellin_comp_rpow P.g (-s) (-1)
-- Module: Mathlib.NumberTheory.LSeries.AbstractFuncEq
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
P : StrongFEPair E
s : ℂ
step1 :
  mellin (fun (t : ℝ) ↦ P.g (HPow.hPow (β := ℝ) t (-1))) (-s) =
    HSMul.hSMul (α := ℝ) |(-1)|⁻¹ (mellin P.g (-s / (↑(-1) : ℂ)))
⊢ mellin (fun (t : ℝ) ↦ P.g (1 / t)) (-s) = mellin P.g s

Tactic:
simp_rw [abs_neg, abs_one, inv_one, one_smul, ofReal_neg, ofReal_one, div_neg, div_one, neg_neg,
    rpow_neg_one, ← one_div] at step1

Premises used: abs_neg, Real.rpow_neg_one, inv_one, Complex.ofReal_neg, neg_neg, Complex.ofReal_one, one_smul, div_neg, one_div, abs_one, div_one
-- Module: Mathlib.NumberTheory.LSeries.AbstractFuncEq
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
P : StrongFEPair E
s : ℂ
step1 : mellin (fun (t : ℝ) ↦ P.g (1 / t)) (-s) = mellin P.g s
⊢ Eq.{u_1 + 1} (α := E) (mellin (fun (t : ℝ) ↦ (↑t : ℂ) ^ (-(↑P.k : ℂ)) • P.g (1 / t)) ((↑P.k : ℂ) - s))
    (mellin (fun (t : ℝ) ↦ P.g (1 / t)) ((↑P.k : ℂ) - s + -(↑P.k : ℂ)))

Tactic:
have step2 := mellin_cpow_smul (fun t ↦ P.g (1 / t)) (P.k - s) (-P.k)
-- Module: Mathlib.NumberTheory.LSeries.AbstractFuncEq
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
P : StrongFEPair E
s : ℂ
step1 : mellin (fun (t : ℝ) ↦ P.g (1 / t)) (-s) = mellin P.g s
step2 :
  Eq.{u_1 + 1} (α := E) (mellin (fun (t : ℝ) ↦ (↑t : ℂ) ^ (-(↑P.k : ℂ)) • P.g (1 / t)) ((↑P.k : ℂ) - s))
    (mellin (fun (t : ℝ) ↦ P.g (1 / t)) ((↑P.k : ℂ) - s + -(↑P.k : ℂ)))
⊢ mellin (fun (t : ℝ) ↦ (↑t : ℂ) ^ (-(↑P.k : ℂ)) • P.g (1 / t)) ((↑P.k : ℂ) - s) = mellin P.g s

Tactic:
rw [← sub_eq_add_neg, sub_right_comm, sub_self, zero_sub, step1] at step2

Premises used: sub_self, sub_eq_add_neg, sub_right_comm, zero_sub
-- Module: Mathlib.NumberTheory.LSeries.AbstractFuncEq
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
P : StrongFEPair E
s : ℂ
step1 : mellin (fun (t : ℝ) ↦ P.g (1 / t)) (-s) = mellin P.g s
step2 : mellin (fun (t : ℝ) ↦ (↑t : ℂ) ^ (-(↑P.k : ℂ)) • P.g (1 / t)) ((↑P.k : ℂ) - s) = mellin P.g s
⊢ mellin (fun (t : ℝ) ↦ P.ε • (↑t : ℂ) ^ (-(↑P.k : ℂ)) • P.g (1 / t)) ((↑P.k : ℂ) - s) =
    HSMul.hSMul (β := E) P.ε (mellin (fun (t : ℝ) ↦ (↑t : ℂ) ^ (-(↑P.k : ℂ)) • P.g (1 / t)) ((↑P.k : ℂ) - s))

Tactic:
have step3 := mellin_const_smul (fun t ↦ (t : ℂ) ^ (-P.k : ℂ) • P.g (1 / t)) (P.k - s) P.ε
-- Module: Mathlib.NumberTheory.LSeries.AbstractFuncEq
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
P : StrongFEPair E
s : ℂ
step1 : mellin (fun (t : ℝ) ↦ P.g (1 / t)) (-s) = mellin P.g s
step2 : mellin (fun (t : ℝ) ↦ (↑t : ℂ) ^ (-(↑P.k : ℂ)) • P.g (1 / t)) ((↑P.k : ℂ) - s) = mellin P.g s
step3 :
  mellin (fun (t : ℝ) ↦ P.ε • (↑t : ℂ) ^ (-(↑P.k : ℂ)) • P.g (1 / t)) ((↑P.k : ℂ) - s) =
    HSMul.hSMul (β := E) P.ε (mellin (fun (t : ℝ) ↦ (↑t : ℂ) ^ (-(↑P.k : ℂ)) • P.g (1 / t)) ((↑P.k : ℂ) - s))
⊢ mellin (fun (t : ℝ) ↦ P.ε • (↑t : ℂ) ^ (-(↑P.k : ℂ)) • P.g (1 / t)) ((↑P.k : ℂ) - s) = P.ε • mellin P.g s

Tactic:
rw [step2] at step3
-- Module: Mathlib.NumberTheory.LSeries.AbstractFuncEq
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
P : StrongFEPair E
s : ℂ
step1 : mellin (fun (t : ℝ) ↦ P.g (1 / t)) (-s) = mellin P.g s
step2 : mellin (fun (t : ℝ) ↦ (↑t : ℂ) ^ (-(↑P.k : ℂ)) • P.g (1 / t)) ((↑P.k : ℂ) - s) = mellin P.g s
step3 : mellin (fun (t : ℝ) ↦ P.ε • (↑t : ℂ) ^ (-(↑P.k : ℂ)) • P.g (1 / t)) ((↑P.k : ℂ) - s) = P.ε • mellin P.g s
rw : mellin P.f ((↑P.k : ℂ) - s) = mellin (fun (t : ℝ) ↦ P.ε • (↑t : ℂ) ^ (-(↑P.k : ℂ)) • P.g (1 / t)) ((↑P.k : ℂ) - s)
⊢ mellin P.f ((↑P.k : ℂ) - s) = P.ε • mellin P.g s

Tactic:
rw [← step3]
-- Module: Mathlib.NumberTheory.LSeries.AbstractFuncEq
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
P : StrongFEPair E
s : ℂ
step1 : mellin (fun (t : ℝ) ↦ P.g (1 / t)) (-s) = mellin P.g s
step2 : mellin (fun (t : ℝ) ↦ (↑t : ℂ) ^ (-(↑P.k : ℂ)) • P.g (1 / t)) ((↑P.k : ℂ) - s) = mellin P.g s
step3 : mellin (fun (t : ℝ) ↦ P.ε • (↑t : ℂ) ^ (-(↑P.k : ℂ)) • P.g (1 / t)) ((↑P.k : ℂ) - s) = P.ε • mellin P.g s
⊢ mellin P.f ((↑P.k : ℂ) - s) = mellin (fun (t : ℝ) ↦ P.ε • (↑t : ℂ) ^ (-(↑P.k : ℂ)) • P.g (1 / t)) ((↑P.k : ℂ) - s)

Tactic:
setIntegral_congr_fun measurableSet_Ioi (fun t ht ↦ ?_)

Premises used: measurableSet_Ioi, MeasureTheory.setIntegral_congr_fun, mellin
-- Module: Mathlib.NumberTheory.LSeries.AbstractFuncEq
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
P : StrongFEPair E
s : ℂ
step1 : mellin (fun (t : ℝ) ↦ P.g (1 / t)) (-s) = mellin P.g s
step2 : mellin (fun (t : ℝ) ↦ (↑t : ℂ) ^ (-(↑P.k : ℂ)) • P.g (1 / t)) ((↑P.k : ℂ) - s) = mellin P.g s
step3 : mellin (fun (t : ℝ) ↦ P.ε • (↑t : ℂ) ^ (-(↑P.k : ℂ)) • P.g (1 / t)) ((↑P.k : ℂ) - s) = P.ε • mellin P.g s
refine :
  ∀ (t : ℝ) (ht : Membership.mem (γ := Set ℝ) (Ioi 0) t),
    (↑t : ℂ) ^ ((↑P.k : ℂ) - s - 1) • P.f t =
      HSMul.hSMul (β := E) ((↑t : ℂ) ^ ((↑P.k : ℂ) - s - 1))
        ((fun (t : ℝ) ↦ P.ε • (↑t : ℂ) ^ (-(↑P.k : ℂ)) • P.g (1 / t)) t)
⊢ mellin P.f ((↑P.k : ℂ) - s) = mellin (fun (t : ℝ) ↦ P.ε • (↑t : ℂ) ^ (-(↑P.k : ℂ)) • P.g (1 / t)) ((↑P.k : ℂ) - s)

Tactic:
refine setIntegral_congr_fun measurableSet_Ioi (fun t ht ↦ ?_)

Premises used: measurableSet_Ioi, MeasureTheory.setIntegral_congr_fun
-- Module: Mathlib.NumberTheory.LSeries.AbstractFuncEq
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
P : StrongFEPair E
s : ℂ
step1 : mellin (fun (t : ℝ) ↦ P.g (1 / t)) (-s) = mellin P.g s
step2 : mellin (fun (t : ℝ) ↦ (↑t : ℂ) ^ (-(↑P.k : ℂ)) • P.g (1 / t)) ((↑P.k : ℂ) - s) = mellin P.g s
step3 : mellin (fun (t : ℝ) ↦ P.ε • (↑t : ℂ) ^ (-(↑P.k : ℂ)) • P.g (1 / t)) ((↑P.k : ℂ) - s) = P.ε • mellin P.g s
t : ℝ
ht : Membership.mem (γ := Set ℝ) (Ioi 0) t
simp_rw :
  (↑t : ℂ) ^ ((↑P.k : ℂ) - s - 1) • P.f t =
    ((↑t : ℂ) ^ ((↑P.k : ℂ) - s - 1) * (P.ε * ((↑t : ℂ) ^ (-(↑P.k : ℂ)) * (P.ε⁻¹ * (↑(t ^ P.k) : ℂ))))) • P.f t
⊢ (↑t : ℂ) ^ ((↑P.k : ℂ) - s - 1) • P.f t =
    HSMul.hSMul (β := E) ((↑t : ℂ) ^ ((↑P.k : ℂ) - s - 1))
      ((fun (t : ℝ) ↦ P.ε • (↑t : ℂ) ^ (-(↑P.k : ℂ)) • P.g (1 / t)) t)

Tactic:
simp_rw [P.h_feq' t ht, ← mul_smul]

Premises used: WeakFEPair.h_feq', StrongFEPair.toWeakFEPair, SemigroupAction.mul_smul
-- Module: Mathlib.NumberTheory.LSeries.AbstractFuncEq
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
P : StrongFEPair E
s : ℂ
step1 : mellin (fun (t : ℝ) ↦ P.g (1 / t)) (-s) = mellin P.g s
step2 : mellin (fun (t : ℝ) ↦ (↑t : ℂ) ^ (-(↑P.k : ℂ)) • P.g (1 / t)) ((↑P.k : ℂ) - s) = mellin P.g s
step3 : mellin (fun (t : ℝ) ↦ P.ε • (↑t : ℂ) ^ (-(↑P.k : ℂ)) • P.g (1 / t)) ((↑P.k : ℂ) - s) = P.ε • mellin P.g s
t : ℝ
ht : Membership.mem (γ := Set ℝ) (Ioi 0) t
rw :
  (↑t : ℂ) ^ ((↑P.k : ℂ) - s - 1) • P.f t =
    ((↑t : ℂ) ^ ((↑P.k : ℂ) - s - 1) * (P.ε * (((↑t : ℂ) ^ (↑P.k : ℂ))⁻¹ * (P.ε⁻¹ * (↑t : ℂ) ^ (↑P.k : ℂ))))) • P.f t
⊢ (↑t : ℂ) ^ ((↑P.k : ℂ) - s - 1) • P.f t =
    ((↑t : ℂ) ^ ((↑P.k : ℂ) - s - 1) * (P.ε * ((↑t : ℂ) ^ (-(↑P.k : ℂ)) * (P.ε⁻¹ * (↑(t ^ P.k) : ℂ))))) • P.f t

Tactic:
rw [cpow_neg, ofReal_cpow (le_of_lt ht)]

Premises used: Complex.ofReal_cpow, le_of_lt, Complex.cpow_neg