awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.AbelSummation
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
c : ℕ → 𝕜
f : ℝ → 𝕜
hf_diff : ∀ (t : ℝ), Membership.mem (γ := Set ℝ) (Set.Ici 0) t → DifferentiableAt ℝ (F := ℝ) (fun (x : ℝ) ↦ ‖f x‖) t
hf_int : LocallyIntegrableOn (X := ℝ) (ε := ℝ) (deriv fun (t : ℝ) ↦ ‖f t‖) (Set.Ici 0) volume
h_bdd : Asymptotics.IsBigO (E := ℝ) (F := ℝ) atTop (fun (n : ℕ) ↦ ‖f (↑n : ℝ)‖ * ∑ k ∈ Icc 0 n, ‖c k‖) fun (x : ℕ) ↦ 1
g : ℝ → ℝ
hg₁ :
  Asymptotics.IsBigO (E := ℝ) atTop
    (fun (t : ℝ) ↦ HMul.hMul (α := ℝ) (deriv (fun (t : ℝ) ↦ ‖f t‖) t) (∑ k ∈ Icc 0 ⌊t⌋₊, ‖c k‖)) g
hg₂ : IntegrableAtFilter (mα := MeasureSpace.toMeasurableSpace) g atTop volume
refine :
  ∀ (n : ℕ),
    ∑ k ∈ Icc 0 n, ‖f (↑k : ℝ)‖ * ‖c k‖ =
      ‖f (↑n : ℝ)‖ * ∑ k ∈ Icc 0 n, ‖c k‖ -
        @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Ioc (↑0 : ℝ) (↑n : ℝ)))
          fun (t : ℝ) ↦ HMul.hMul (α := ℝ) (deriv (fun (t : ℝ) ↦ ‖f t‖) t) (∑ k ∈ Icc 0 ⌊t⌋₊, ‖c k‖)
⊢ Summable.{u_1, 0} (α := 𝕜) fun (n : ℕ) ↦ f (↑n : ℝ) * c n

Tactic:
refine summable_mul_of_bigO_atTop_aux c 0 h_bdd (by rwa [Nat.cast_zero]) (fun n ↦ ?_) hg₁ hg₂

Premises used: _private.0.summable_mul_of_bigO_atTop_aux, OfNat.ofNat
-- Module: Mathlib.NumberTheory.AbelSummation
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
c : ℕ → 𝕜
f : ℝ → 𝕜
hf_diff : ∀ (t : ℝ), Membership.mem (γ := Set ℝ) (Set.Ici 0) t → DifferentiableAt ℝ (F := ℝ) (fun (x : ℝ) ↦ ‖f x‖) t
hf_int : LocallyIntegrableOn (X := ℝ) (ε := ℝ) (deriv fun (t : ℝ) ↦ ‖f t‖) (Set.Ici 0) volume
h_bdd : Asymptotics.IsBigO (E := ℝ) (F := ℝ) atTop (fun (n : ℕ) ↦ ‖f (↑n : ℝ)‖ * ∑ k ∈ Icc 0 n, ‖c k‖) fun (x : ℕ) ↦ 1
g : ℝ → ℝ
hg₁ :
  Asymptotics.IsBigO (E := ℝ) atTop
    (fun (t : ℝ) ↦ HMul.hMul (α := ℝ) (deriv (fun (t : ℝ) ↦ ‖f t‖) t) (∑ k ∈ Icc 0 ⌊t⌋₊, ‖c k‖)) g
hg₂ : IntegrableAtFilter (mα := MeasureSpace.toMeasurableSpace) g atTop volume
n : ℕ
⊢ ∑ k ∈ Icc 0 n, ‖f (↑k : ℝ)‖ * ‖c k‖ =
    ‖f (↑n : ℝ)‖ * ∑ k ∈ Icc 0 n, ‖c k‖ -
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Ioc (↑0 : ℝ) (↑n : ℝ)))
        fun (t : ℝ) ↦ HMul.hMul (α := ℝ) (deriv (fun (t : ℝ) ↦ ‖f t‖) t) (∑ k ∈ Icc 0 ⌊t⌋₊, ‖c k‖)

Tactic:
exact_mod_cast sum_mul_eq_sub_integral_mul' _ _ (fun _ ht ↦ hf_diff _ ht.1)
    (hf_int.integrableOn_compact_subset Set.Icc_subset_Ici_self isCompact_Icc)

Premises used: sum_mul_eq_sub_integral_mul', CompactIccSpace.isCompact_Icc, And.left, MeasureTheory.LocallyIntegrableOn.integrableOn_compact_subset, Set.Icc_subset_Ici_self
-- Module: Mathlib.NumberTheory.AbelSummation
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
c : ℕ → 𝕜
f : ℝ → 𝕜
hf_diff : ∀ (t : ℝ), Membership.mem (γ := Set ℝ) (Set.Ici 1) t → DifferentiableAt ℝ (F := ℝ) (fun (x : ℝ) ↦ ‖f x‖) t
hf_int : LocallyIntegrableOn (X := ℝ) (ε := ℝ) (deriv fun (t : ℝ) ↦ ‖f t‖) (Set.Ici 1) volume
h_bdd : Asymptotics.IsBigO (E := ℝ) (F := ℝ) atTop (fun (n : ℕ) ↦ ‖f (↑n : ℝ)‖ * ∑ k ∈ Icc 1 n, ‖c k‖) fun (x : ℕ) ↦ 1
g : ℝ → ℝ
hg₁ :
  Asymptotics.IsBigO (E := ℝ) atTop
    (fun (t : ℝ) ↦ HMul.hMul (α := ℝ) (deriv (fun (t : ℝ) ↦ ‖f t‖) t) (∑ k ∈ Icc 1 ⌊t⌋₊, ‖c k‖)) g
hg₂ : IntegrableAtFilter (mα := MeasureSpace.toMeasurableSpace) g atTop volume
n : ℕ
rw :
  ∑ k ∈ Icc 1 n, ‖c k‖ =
    norm.{u_1} (E := 𝕜) ((fun (n : ℕ) ↦ if n = 0 then 0 else c n) 0) +
      ∑ x ∈ Icc 1 n, norm.{u_1} (E := 𝕜) ((fun (n : ℕ) ↦ if n = 0 then 0 else c n) x)
⊢ Eq (α := ℝ) (∑ k ∈ Icc 1 n, ‖c k‖) (∑ k ∈ Icc 0 n, norm.{u_1} (E := 𝕜) ((fun (n : ℕ) ↦ if n = 0 then 0 else c n) k))

Tactic:
rw [Icc_eq_cons_Ioc n.zero_le, sum_cons, ← Icc_add_one_left_eq_Ioc, zero_add]

Premises used: Finset.Icc_add_one_left_eq_Ioc, Nat.zero_le, Finset.sum_cons, Finset.Icc_eq_cons_Ioc, zero_add
-- Module: Mathlib.NumberTheory.AbelSummation
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
c : ℕ → 𝕜
f : ℝ → 𝕜
hf_diff : ∀ (t : ℝ), Membership.mem (γ := Set ℝ) (Set.Ici 1) t → DifferentiableAt ℝ (F := ℝ) (fun (x : ℝ) ↦ ‖f x‖) t
hf_int : LocallyIntegrableOn (X := ℝ) (ε := ℝ) (deriv fun (t : ℝ) ↦ ‖f t‖) (Set.Ici 1) volume
h_bdd : Asymptotics.IsBigO (E := ℝ) (F := ℝ) atTop (fun (n : ℕ) ↦ ‖f (↑n : ℝ)‖ * ∑ k ∈ Icc 1 n, ‖c k‖) fun (x : ℕ) ↦ 1
g : ℝ → ℝ
hg₁ :
  Asymptotics.IsBigO (E := ℝ) atTop
    (fun (t : ℝ) ↦ HMul.hMul (α := ℝ) (deriv (fun (t : ℝ) ↦ ‖f t‖) t) (∑ k ∈ Icc 1 ⌊t⌋₊, ‖c k‖)) g
hg₂ : IntegrableAtFilter (mα := MeasureSpace.toMeasurableSpace) g atTop volume
n : ℕ
simp_rw : Eq (α := ℝ) (∑ k ∈ Icc 1 n, ‖c k‖) (∑ x ∈ Icc 1 n, ‖if x = 0 then 0 else c x‖)
⊢ ∑ k ∈ Icc 1 n, ‖c k‖ =
    norm.{u_1} (E := 𝕜) ((fun (n : ℕ) ↦ if n = 0 then 0 else c n) 0) +
      ∑ x ∈ Icc 1 n, norm.{u_1} (E := 𝕜) ((fun (n : ℕ) ↦ if n = 0 then 0 else c n) x)

Tactic:
simp_rw [if_pos, norm_zero, zero_add]

Premises used: norm_zero, if_pos, zero_add
-- Module: Mathlib.NumberTheory.AbelSummation
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
c : ℕ → 𝕜
f : ℝ → 𝕜
hf_diff : ∀ (t : ℝ), Membership.mem (γ := Set ℝ) (Set.Ici 1) t → DifferentiableAt ℝ (F := ℝ) (fun (x : ℝ) ↦ ‖f x‖) t
hf_int : LocallyIntegrableOn (X := ℝ) (ε := ℝ) (deriv fun (t : ℝ) ↦ ‖f t‖) (Set.Ici 1) volume
h_bdd : Asymptotics.IsBigO (E := ℝ) (F := ℝ) atTop (fun (n : ℕ) ↦ ‖f (↑n : ℝ)‖ * ∑ k ∈ Icc 1 n, ‖c k‖) fun (x : ℕ) ↦ 1
g : ℝ → ℝ
hg₁ :
  Asymptotics.IsBigO (E := ℝ) atTop
    (fun (t : ℝ) ↦ HMul.hMul (α := ℝ) (deriv (fun (t : ℝ) ↦ ‖f t‖) t) (∑ k ∈ Icc 1 ⌊t⌋₊, ‖c k‖)) g
hg₂ : IntegrableAtFilter (mα := MeasureSpace.toMeasurableSpace) g atTop volume
n x : ℕ
h : x ∈ Icc 1 n
rw rw₁ : ‖c x‖ = ‖c x‖
⊢ ‖c x‖ = ‖if x = 0 then 0 else c x‖

Tactic:
rw [if_neg (zero_lt_one.trans_le (mem_Icc.mp h).1).ne']

Premises used: Finset.mem_Icc, LT.lt.ne', zero_lt_one, And.left, LT.lt.trans_le, Iff.mp, if_neg
-- Module: Mathlib.NumberTheory.AbelSummation
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
c : ℕ → 𝕜
f : ℝ → 𝕜
hf_diff : ∀ (t : ℝ), Membership.mem (γ := Set ℝ) (Set.Ici 1) t → DifferentiableAt ℝ (F := ℝ) (fun (x : ℝ) ↦ ‖f x‖) t
hf_int : LocallyIntegrableOn (X := ℝ) (ε := ℝ) (deriv fun (t : ℝ) ↦ ‖f t‖) (Set.Ici 1) volume
h_bdd : Asymptotics.IsBigO (E := ℝ) (F := ℝ) atTop (fun (n : ℕ) ↦ ‖f (↑n : ℝ)‖ * ∑ k ∈ Icc 1 n, ‖c k‖) fun (x : ℕ) ↦ 1
g : ℝ → ℝ
hg₁ :
  Asymptotics.IsBigO (E := ℝ) atTop
    (fun (t : ℝ) ↦ HMul.hMul (α := ℝ) (deriv (fun (t : ℝ) ↦ ‖f t‖) t) (∑ k ∈ Icc 1 ⌊t⌋₊, ‖c k‖)) g
hg₂ : IntegrableAtFilter (mα := MeasureSpace.toMeasurableSpace) g atTop volume
n : ℕ
⊢ Eq (α := ℝ) (∑ k ∈ Icc 1 n, ‖c k‖) (∑ x ∈ Icc 1 n, ‖if x = 0 then 0 else c x‖)

Tactic:
exact Finset.sum_congr rfl fun _ h ↦ by rw [if_neg (zero_lt_one.trans_le (mem_Icc.mp h).1).ne']

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.NumberTheory.AbelSummation
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
c : ℕ → 𝕜
f : ℝ → 𝕜
hf_diff : ∀ (t : ℝ), Membership.mem (γ := Set ℝ) (Set.Ici 1) t → DifferentiableAt ℝ (F := ℝ) (fun (x : ℝ) ↦ ‖f x‖) t
hf_int : LocallyIntegrableOn (X := ℝ) (ε := ℝ) (deriv fun (t : ℝ) ↦ ‖f t‖) (Set.Ici 1) volume
h_bdd : Asymptotics.IsBigO (E := ℝ) (F := ℝ) atTop (fun (n : ℕ) ↦ ‖f (↑n : ℝ)‖ * ∑ k ∈ Icc 1 n, ‖c k‖) fun (x : ℕ) ↦ 1
g : ℝ → ℝ
hg₁ :
  Asymptotics.IsBigO (E := ℝ) atTop
    (fun (t : ℝ) ↦ HMul.hMul (α := ℝ) (deriv (fun (t : ℝ) ↦ ‖f t‖) t) (∑ k ∈ Icc 1 ⌊t⌋₊, ‖c k‖)) g
hg₂ : IntegrableAtFilter (mα := MeasureSpace.toMeasurableSpace) g atTop volume
⊢ ∀ (n : ℕ),
    Eq (α := ℝ) (∑ k ∈ Icc 1 n, ‖c k‖) (∑ k ∈ Icc 0 n, norm.{u_1} (E := 𝕜) ((fun (n : ℕ) ↦ if n = 0 then 0 else c n) k))

Tactic:
have h : ∀ n, ∑ k ∈ Icc 1 n, ‖c k‖ = ∑ k ∈ Icc 0 n, ‖(fun n ↦ if n = 0 then 0 else c n) k‖ := by
    intro n
    rw [Icc_eq_cons_Ioc n.zero_le, sum_cons, ← Icc_add_one_left_eq_Ioc, zero_add]
    simp_rw [if_pos, norm_zero, zero_add]
    exact Finset.sum_congr rfl fun _ h ↦ by rw [if_neg (zero_lt_one.trans_le (mem_Icc.mp h).1).ne']
-- Module: Mathlib.NumberTheory.AbelSummation
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
c : ℕ → 𝕜
f : ℝ → 𝕜
hf_diff : ∀ (t : ℝ), Membership.mem (γ := Set ℝ) (Set.Ici 1) t → DifferentiableAt ℝ (F := ℝ) (fun (x : ℝ) ↦ ‖f x‖) t
hf_int : LocallyIntegrableOn (X := ℝ) (ε := ℝ) (deriv fun (t : ℝ) ↦ ‖f t‖) (Set.Ici 1) volume
h_bdd : Asymptotics.IsBigO (E := ℝ) (F := ℝ) atTop (fun (n : ℕ) ↦ ‖f (↑n : ℝ)‖ * ∑ k ∈ Icc 1 n, ‖c k‖) fun (x : ℕ) ↦ 1
g : ℝ → ℝ
hg₁ :
  Asymptotics.IsBigO (E := ℝ) atTop
    (fun (t : ℝ) ↦ HMul.hMul (α := ℝ) (deriv (fun (t : ℝ) ↦ ‖f t‖) t) (∑ k ∈ Icc 1 ⌊t⌋₊, ‖c k‖)) g
hg₂ : IntegrableAtFilter (mα := MeasureSpace.toMeasurableSpace) g atTop volume
h :
  ∀ (n : ℕ),
    Eq (α := ℝ) (∑ k ∈ Icc 1 n, ‖c k‖) (∑ k ∈ Icc 0 n, norm.{u_1} (E := 𝕜) ((fun (n : ℕ) ↦ if n = 0 then 0 else c n) k))
⊢ Asymptotics.IsBigO (E := ℝ) (F := ℝ) atTop (fun (n : ℕ) ↦ ‖f (↑n : ℝ)‖ * ∑ x ∈ Icc 0 n, ‖if x = 0 then 0 else c x‖)
    fun (x : ℕ) ↦ 1

Tactic:
simp_rw [h] at h_bdd hg₁
-- Module: Mathlib.NumberTheory.AbelSummation
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
c : ℕ → 𝕜
f : ℝ → 𝕜
hf_diff : ∀ (t : ℝ), Membership.mem (γ := Set ℝ) (Set.Ici 1) t → DifferentiableAt ℝ (F := ℝ) (fun (x : ℝ) ↦ ‖f x‖) t
hf_int : LocallyIntegrableOn (X := ℝ) (ε := ℝ) (deriv fun (t : ℝ) ↦ ‖f t‖) (Set.Ici 1) volume
h_bdd : Asymptotics.IsBigO (E := ℝ) (F := ℝ) atTop (fun (n : ℕ) ↦ ‖f (↑n : ℝ)‖ * ∑ k ∈ Icc 1 n, ‖c k‖) fun (x : ℕ) ↦ 1
g : ℝ → ℝ
hg₁ :
  Asymptotics.IsBigO (E := ℝ) atTop
    (fun (t : ℝ) ↦ HMul.hMul (α := ℝ) (deriv (fun (t : ℝ) ↦ ‖f t‖) t) (∑ k ∈ Icc 1 ⌊t⌋₊, ‖c k‖)) g
hg₂ : IntegrableAtFilter (mα := MeasureSpace.toMeasurableSpace) g atTop volume
h :
  ∀ (n : ℕ),
    Eq (α := ℝ) (∑ k ∈ Icc 1 n, ‖c k‖) (∑ k ∈ Icc 0 n, norm.{u_1} (E := 𝕜) ((fun (n : ℕ) ↦ if n = 0 then 0 else c n) k))
h_bdd₁ :
  Asymptotics.IsBigO (E := ℝ) (F := ℝ) atTop (fun (n : ℕ) ↦ ‖f (↑n : ℝ)‖ * ∑ x ∈ Icc 0 n, ‖if x = 0 then 0 else c x‖)
    fun (x : ℕ) ↦ 1
⊢ Asymptotics.IsBigO (E := ℝ) atTop
    (fun (t : ℝ) ↦ HMul.hMul (α := ℝ) (deriv (fun (t : ℝ) ↦ ‖f t‖) t) (∑ x ∈ Icc 0 ⌊t⌋₊, ‖if x = 0 then 0 else c x‖)) g

Tactic:
simp_rw [h] at h_bdd hg₁
-- Module: Mathlib.NumberTheory.AbelSummation
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
c : ℕ → 𝕜
f : ℝ → 𝕜
hf_diff : ∀ (t : ℝ), Membership.mem (γ := Set ℝ) (Set.Ici 1) t → DifferentiableAt ℝ (F := ℝ) (fun (x : ℝ) ↦ ‖f x‖) t
hf_int : LocallyIntegrableOn (X := ℝ) (ε := ℝ) (deriv fun (t : ℝ) ↦ ‖f t‖) (Set.Ici 1) volume
g : ℝ → ℝ
hg₂ : IntegrableAtFilter (mα := MeasureSpace.toMeasurableSpace) g atTop volume
h :
  ∀ (n : ℕ),
    Eq (α := ℝ) (∑ k ∈ Icc 1 n, ‖c k‖) (∑ k ∈ Icc 0 n, norm.{u_1} (E := 𝕜) ((fun (n : ℕ) ↦ if n = 0 then 0 else c n) k))
h_bdd :
  Asymptotics.IsBigO (E := ℝ) (F := ℝ) atTop (fun (n : ℕ) ↦ ‖f (↑n : ℝ)‖ * ∑ x ∈ Icc 0 n, ‖if x = 0 then 0 else c x‖)
    fun (x : ℕ) ↦ 1
hg₁ :
  Asymptotics.IsBigO (E := ℝ) atTop
    (fun (t : ℝ) ↦ HMul.hMul (α := ℝ) (deriv (fun (t : ℝ) ↦ ‖f t‖) t) (∑ x ∈ Icc 0 ⌊t⌋₊, ‖if x = 0 then 0 else c x‖)) g
rwa rwa₁ rwa₂ rwa₃ : LocallyIntegrableOn (X := ℝ) (ε := ℝ) (deriv fun (t : ℝ) ↦ ‖f t‖) (Set.Ici 1) volume
⊢ LocallyIntegrableOn (X := ℝ) (ε := ℝ) (deriv fun (t : ℝ) ↦ ‖f t‖) (Set.Ici (↑1 : ℝ)) volume

Tactic:
rwa [Nat.cast_one]

Premises used: Nat.cast_one
-- Module: Mathlib.NumberTheory.AbelSummation
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
c : ℕ → 𝕜
f : ℝ → 𝕜
hf_diff : ∀ (t : ℝ), Membership.mem (γ := Set ℝ) (Set.Ici 1) t → DifferentiableAt ℝ (F := ℝ) (fun (x : ℝ) ↦ ‖f x‖) t
hf_int : LocallyIntegrableOn (X := ℝ) (ε := ℝ) (deriv fun (t : ℝ) ↦ ‖f t‖) (Set.Ici 1) volume
g : ℝ → ℝ
hg₂ : IntegrableAtFilter (mα := MeasureSpace.toMeasurableSpace) g atTop volume
h :
  ∀ (n : ℕ),
    Eq (α := ℝ) (∑ k ∈ Icc 1 n, ‖c k‖) (∑ k ∈ Icc 0 n, norm.{u_1} (E := 𝕜) ((fun (n : ℕ) ↦ if n = 0 then 0 else c n) k))
h_bdd :
  Asymptotics.IsBigO (E := ℝ) (F := ℝ) atTop (fun (n : ℕ) ↦ ‖f (↑n : ℝ)‖ * ∑ x ∈ Icc 0 n, ‖if x = 0 then 0 else c x‖)
    fun (x : ℕ) ↦ 1
hg₁ :
  Asymptotics.IsBigO (E := ℝ) atTop
    (fun (t : ℝ) ↦ HMul.hMul (α := ℝ) (deriv (fun (t : ℝ) ↦ ‖f t‖) t) (∑ x ∈ Icc 0 ⌊t⌋₊, ‖if x = 0 then 0 else c x‖)) g
refine_1 :
  ∀ (n : ℕ),
    ∑ k ∈ Icc 0 n, ‖f (↑k : ℝ)‖ * norm.{u_1} (E := 𝕜) ((fun (n : ℕ) ↦ if n = 0 then 0 else c n) k) =
      ‖f (↑n : ℝ)‖ * ∑ k ∈ Icc 0 n, norm.{u_1} (E := 𝕜) ((fun (n : ℕ) ↦ if n = 0 then 0 else c n) k) -
        @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Ioc (↑1 : ℝ) (↑n : ℝ)))
          fun (t : ℝ) ↦
          HMul.hMul (α := ℝ) (deriv (fun (t : ℝ) ↦ ‖f t‖) t)
            (∑ k ∈ Icc 0 ⌊t⌋₊, norm.{u_1} (E := 𝕜) ((fun (n : ℕ) ↦ if n = 0 then 0 else c n) k))
refine_2 :
  EventuallyEq.{0, u_1} (β := 𝕜) atTop (fun (n : ℕ) ↦ f (↑n : ℝ) * (fun (n : ℕ) ↦ if n = 0 then 0 else c n) n)
    fun (n : ℕ) ↦ f (↑n : ℝ) * c n
⊢ Summable.{u_1, 0} (α := 𝕜) fun (n : ℕ) ↦ f (↑n : ℝ) * c n

Tactic:
refine Summable.congr_atTop (summable_mul_of_bigO_atTop_aux (fun n ↦ if n = 0 then 0 else c n) 1
    h_bdd (by rwa [Nat.cast_one]) (fun n ↦ ?_) hg₁ hg₂) ?_

Premises used: _private.0.summable_mul_of_bigO_atTop_aux, Summable.congr_atTop, OfNat.ofNat, Eq, ite
-- Module: Mathlib.NumberTheory.AbelSummation
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
c : ℕ → 𝕜
f : ℝ → 𝕜
hf_diff : ∀ (t : ℝ), Membership.mem (γ := Set ℝ) (Set.Ici 1) t → DifferentiableAt ℝ (F := ℝ) (fun (x : ℝ) ↦ ‖f x‖) t
hf_int : LocallyIntegrableOn (X := ℝ) (ε := ℝ) (deriv fun (t : ℝ) ↦ ‖f t‖) (Set.Ici 1) volume
g : ℝ → ℝ
hg₂ : IntegrableAtFilter (mα := MeasureSpace.toMeasurableSpace) g atTop volume
h :
  ∀ (n : ℕ),
    Eq (α := ℝ) (∑ k ∈ Icc 1 n, ‖c k‖) (∑ k ∈ Icc 0 n, norm.{u_1} (E := 𝕜) ((fun (n : ℕ) ↦ if n = 0 then 0 else c n) k))
h_bdd :
  Asymptotics.IsBigO (E := ℝ) (F := ℝ) atTop (fun (n : ℕ) ↦ ‖f (↑n : ℝ)‖ * ∑ x ∈ Icc 0 n, ‖if x = 0 then 0 else c x‖)
    fun (x : ℕ) ↦ 1
hg₁ :
  Asymptotics.IsBigO (E := ℝ) atTop
    (fun (t : ℝ) ↦ HMul.hMul (α := ℝ) (deriv (fun (t : ℝ) ↦ ‖f t‖) t) (∑ x ∈ Icc 0 ⌊t⌋₊, ‖if x = 0 then 0 else c x‖)) g
n : ℕ
⊢ norm.{u_1} (E := 𝕜) ((fun (n : ℕ) ↦ if n = 0 then 0 else c n) 0) = 0

Tactic:
simp only [reduceIte, norm_zero]

Premises used: norm_zero, reduceIte
-- Module: Mathlib.NumberTheory.AbelSummation
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
c : ℕ → 𝕜
f : ℝ → 𝕜
hf_diff : ∀ (t : ℝ), Membership.mem (γ := Set ℝ) (Set.Ici 1) t → DifferentiableAt ℝ (F := ℝ) (fun (x : ℝ) ↦ ‖f x‖) t
hf_int : LocallyIntegrableOn (X := ℝ) (ε := ℝ) (deriv fun (t : ℝ) ↦ ‖f t‖) (Set.Ici 1) volume
g : ℝ → ℝ
hg₂ : IntegrableAtFilter (mα := MeasureSpace.toMeasurableSpace) g atTop volume
h :
  ∀ (n : ℕ),
    Eq (α := ℝ) (∑ k ∈ Icc 1 n, ‖c k‖) (∑ k ∈ Icc 0 n, norm.{u_1} (E := 𝕜) ((fun (n : ℕ) ↦ if n = 0 then 0 else c n) k))
h_bdd :
  Asymptotics.IsBigO (E := ℝ) (F := ℝ) atTop (fun (n : ℕ) ↦ ‖f (↑n : ℝ)‖ * ∑ x ∈ Icc 0 n, ‖if x = 0 then 0 else c x‖)
    fun (x : ℕ) ↦ 1
hg₁ :
  Asymptotics.IsBigO (E := ℝ) atTop
    (fun (t : ℝ) ↦ HMul.hMul (α := ℝ) (deriv (fun (t : ℝ) ↦ ‖f t‖) t) (∑ x ∈ Icc 0 ⌊t⌋₊, ‖if x = 0 then 0 else c x‖)) g
n : ℕ
⊢ ∑ k ∈ Icc 0 n, ‖f (↑k : ℝ)‖ * norm.{u_1} (E := 𝕜) ((fun (n : ℕ) ↦ if n = 0 then 0 else c n) k) =
    ‖f (↑n : ℝ)‖ * ∑ k ∈ Icc 0 n, norm.{u_1} (E := 𝕜) ((fun (n : ℕ) ↦ if n = 0 then 0 else c n) k) -
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Ioc (↑1 : ℝ) (↑n : ℝ)))
        fun (t : ℝ) ↦
        HMul.hMul (α := ℝ) (deriv (fun (t : ℝ) ↦ ‖f t‖) t)
          (∑ k ∈ Icc 0 ⌊t⌋₊, norm.{u_1} (E := 𝕜) ((fun (n : ℕ) ↦ if n = 0 then 0 else c n) k))

Tactic:
exact_mod_cast sum_mul_eq_sub_integral_mul₀' _ (by simp only [reduceIte, norm_zero]) n
      (fun _ ht ↦ hf_diff _ ht.1)
      (hf_int.integrableOn_compact_subset Set.Icc_subset_Ici_self isCompact_Icc)

Premises used: CompactIccSpace.isCompact_Icc, sum_mul_eq_sub_integral_mul₀', And.left, MeasureTheory.LocallyIntegrableOn.integrableOn_compact_subset, Set.Icc_subset_Ici_self
-- Module: Mathlib.NumberTheory.AbelSummation
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
c : ℕ → 𝕜
f : ℝ → 𝕜
hf_diff : ∀ (t : ℝ), Membership.mem (γ := Set ℝ) (Set.Ici 1) t → DifferentiableAt ℝ (F := ℝ) (fun (x : ℝ) ↦ ‖f x‖) t
hf_int : LocallyIntegrableOn (X := ℝ) (ε := ℝ) (deriv fun (t : ℝ) ↦ ‖f t‖) (Set.Ici 1) volume
g : ℝ → ℝ
hg₂ : IntegrableAtFilter (mα := MeasureSpace.toMeasurableSpace) g atTop volume
h :
  ∀ (n : ℕ),
    Eq (α := ℝ) (∑ k ∈ Icc 1 n, ‖c k‖) (∑ k ∈ Icc 0 n, norm.{u_1} (E := 𝕜) ((fun (n : ℕ) ↦ if n = 0 then 0 else c n) k))
h_bdd :
  Asymptotics.IsBigO (E := ℝ) (F := ℝ) atTop (fun (n : ℕ) ↦ ‖f (↑n : ℝ)‖ * ∑ x ∈ Icc 0 n, ‖if x = 0 then 0 else c x‖)
    fun (x : ℕ) ↦ 1
hg₁ :
  Asymptotics.IsBigO (E := ℝ) atTop
    (fun (t : ℝ) ↦ HMul.hMul (α := ℝ) (deriv (fun (t : ℝ) ↦ ‖f t‖) t) (∑ x ∈ Icc 0 ⌊t⌋₊, ‖if x = 0 then 0 else c x‖)) g
h₁ : ∀ (k : ℕ) (hk : k ≠ 0), (f (↑k : ℝ) * if k = 0 then 0 else c k) = f (↑k : ℝ) * c k
⊢ EventuallyEq.{0, u_1} (β := 𝕜) atTop (fun (n : ℕ) ↦ f (↑n : ℝ) * (fun (n : ℕ) ↦ if n = 0 then 0 else c n) n)
    fun (n : ℕ) ↦ f (↑n : ℝ) * c n

Tactic:
filter_upwards [eventually_ne_atTop 0] with k hk

Premises used: Filter.eventually_ne_atTop, OfNat.ofNat
-- Module: Mathlib.NumberTheory.AbelSummation
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
c : ℕ → 𝕜
f : ℝ → 𝕜
hf_diff : ∀ (t : ℝ), Membership.mem (γ := Set ℝ) (Set.Ici 1) t → DifferentiableAt ℝ (F := ℝ) (fun (x : ℝ) ↦ ‖f x‖) t
hf_int : LocallyIntegrableOn (X := ℝ) (ε := ℝ) (deriv fun (t : ℝ) ↦ ‖f t‖) (Set.Ici 1) volume
g : ℝ → ℝ
hg₂ : IntegrableAtFilter (mα := MeasureSpace.toMeasurableSpace) g atTop volume
h :
  ∀ (n : ℕ),
    Eq (α := ℝ) (∑ k ∈ Icc 1 n, ‖c k‖) (∑ k ∈ Icc 0 n, norm.{u_1} (E := 𝕜) ((fun (n : ℕ) ↦ if n = 0 then 0 else c n) k))
h_bdd :
  Asymptotics.IsBigO (E := ℝ) (F := ℝ) atTop (fun (n : ℕ) ↦ ‖f (↑n : ℝ)‖ * ∑ x ∈ Icc 0 n, ‖if x = 0 then 0 else c x‖)
    fun (x : ℕ) ↦ 1
hg₁ :
  Asymptotics.IsBigO (E := ℝ) atTop
    (fun (t : ℝ) ↦ HMul.hMul (α := ℝ) (deriv (fun (t : ℝ) ↦ ‖f t‖) t) (∑ x ∈ Icc 0 ⌊t⌋₊, ‖if x = 0 then 0 else c x‖)) g
k : ℕ
hk : k ≠ 0
⊢ (f (↑k : ℝ) * if k = 0 then 0 else c k) = f (↑k : ℝ) * c k

Tactic:
simp_rw [if_neg hk]

Premises used: if_neg
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Carmichael
Goal:
hn : Ne (α := ℕ) 0 0
⊢ (λ : (a : ℕ) → ℕ) 0 = exponent (ZMod 0)ˣ

Tactic:
contradiction
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Carmichael
Goal:
n : ℕ
hn : n + 1 ≠ 0
⊢ Nat.find (p := fun (n_1 : ℕ) ↦ 0 < n_1 ∧ ∀ (g : (ZMod (n + 1))ˣ), g ^ n_1 = 1) ⋯ = exponent (ZMod (n + 1))ˣ

Tactic:
grind [exponent, ExponentExists.of_finite]

Premises used: Monoid.exponent, Monoid.ExponentExists.of_finite
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Carmichael
Goal:
n : ℕ
hn : n ≠ 0
zero : ∀ (hn : Ne (α := ℕ) 0 0), (λ : (a : ℕ) → ℕ) 0 = exponent (ZMod 0)ˣ
succ : ∀ (n : ℕ) (hn : n + 1 ≠ 0), (λ : (a : ℕ) → ℕ) (n + 1) = exponent (ZMod (n + 1))ˣ
⊢ (λ : (a : ℕ) → ℕ) n = exponent (ZMod n)ˣ

Tactic:
cases n with | zero => contradiction | succ n =>
  change Nat.find _ = _
  grind [exponent, ExponentExists.of_finite]

Premises used: ArithmeticFunction.zero, Nat.find, Monoid.exponent, Nat.succ, Monoid.ExponentExists.of_finite
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Carmichael
Goal:
n : ℕ
inst : NeZero n
⊢ (λ : (a : ℕ) → ℕ) n = exponent (ZMod n)ˣ

Tactic:
carmichael_eq_exponent <| NeZero.ne n

Premises used: ArithmeticFunction.carmichael_eq_exponent, NeZero.ne
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Carmichael
Goal:
n : ℕ
a : (ZMod n)ˣ
zero : ∀ (a : (ZMod 0)ˣ), HPow.hPow (β := ℕ) a ((λ : (a : ℕ) → ℕ) 0 : ℕ) = 1
succ : ∀ (n : ℕ) (a : (ZMod (n + 1))ˣ), HPow.hPow (β := ℕ) a ((λ : (a : ℕ) → ℕ) (n + 1) : ℕ) = 1
⊢ HPow.hPow (β := ℕ) a ((λ : (a : ℕ) → ℕ) n : ℕ) = 1

Tactic:
cases n
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Carmichael
Goal:
a : (ZMod 0)ˣ
zero : HPow.hPow (β := ℕ) a 0 = 1
zero₁ zero₂ : Eq (α := (ZMod 0)ˣ) 1 1
⊢ HPow.hPow (β := ℕ) a ((λ : (a : ℕ) → ℕ) 0 : ℕ) = 1

Tactic:
rw [map_zero, pow_zero]

Premises used: pow_zero, ArithmeticFunction.map_zero
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Carmichael
Goal:
n : ℕ
a : (ZMod (n + 1))ˣ
succ : a ^ exponent (ZMod (n + 1))ˣ = 1
⊢ HPow.hPow (β := ℕ) a ((λ : (a : ℕ) → ℕ) (n + 1) : ℕ) = 1

Tactic:
rw [carmichael_eq_exponent']

Premises used: ArithmeticFunction.carmichael_eq_exponent'
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Carmichael
Goal:
n : ℕ
a : (ZMod (n + 1))ˣ
⊢ a ^ exponent (ZMod (n + 1))ˣ = 1

Tactic:
pow_exponent_eq_one a

Premises used: Monoid.pow_exponent_eq_one
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Carmichael
Goal:
n : ℕ
a : (ZMod (n + 1))ˣ
⊢ a ^ exponent (ZMod (n + 1))ˣ = 1

Tactic:
exact pow_exponent_eq_one a

Premises used: Monoid.pow_exponent_eq_one
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Carmichael
Goal:
n : ℕ
zero : (λ : (a : ℕ) → ℕ) 0 ∣ φ 0
succ : ∀ (n : ℕ), (λ : (a : ℕ) → ℕ) (n + 1) ∣ φ (n + 1)
⊢ (λ : (a : ℕ) → ℕ) n ∣ φ n

Tactic:
cases n
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Carmichael
Goal:
⊢ (λ : (a : ℕ) → ℕ) 0 ∣ φ 0

Tactic:
simp
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Carmichael
Goal:
n : ℕ
succ : exponent (ZMod (n + 1))ˣ ∣ Fintype.card (ZMod (n + 1))ˣ
⊢ (λ : (a : ℕ) → ℕ) (n + 1) ∣ φ (n + 1)

Tactic:
rw [← ZMod.card_units_eq_totient, carmichael_eq_exponent']

Premises used: ZMod.card_units_eq_totient, ArithmeticFunction.carmichael_eq_exponent'
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Carmichael
Goal:
n : ℕ
⊢ exponent (ZMod (n + 1))ˣ ∣ Fintype.card (ZMod (n + 1))ˣ

Tactic:
Group.exponent_dvd_card

Premises used: Group.exponent_dvd_card
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Carmichael
Goal:
n : ℕ
⊢ exponent (ZMod (n + 1))ˣ ∣ Fintype.card (ZMod (n + 1))ˣ

Tactic:
exact Group.exponent_dvd_card

Premises used: Group.exponent_dvd_card
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Carmichael
Goal:
a b : ℕ
h : a ∣ b
zero : ∀ (h : a ∣ 0), Dvd.dvd (α := ℕ) ((λ : (a : ℕ) → ℕ) a : ℕ) ((λ : (a : ℕ) → ℕ) 0 : ℕ)
succ : ∀ (n : ℕ) (h : a ∣ n + 1), Dvd.dvd (α := ℕ) ((λ : (a : ℕ) → ℕ) a : ℕ) ((λ : (a : ℕ) → ℕ) (n + 1) : ℕ)
⊢ Dvd.dvd (α := ℕ) ((λ : (a : ℕ) → ℕ) a : ℕ) ((λ : (a : ℕ) → ℕ) b : ℕ)

Tactic:
cases b
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Carmichael
Goal:
a : ℕ
h : a ∣ 0
⊢ Dvd.dvd (α := ℕ) ((λ : (a : ℕ) → ℕ) a : ℕ) ((λ : (a : ℕ) → ℕ) 0 : ℕ)

Tactic:
simp
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Carmichael
Goal:
a n : ℕ
h : a ∣ n + 1
⊢ n + 1 ≠ 0

Tactic:
lia
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Carmichael
Goal:
a n : ℕ
h : a ∣ n + 1
succ : exponent (ZMod a)ˣ ∣ exponent (ZMod (n + 1))ˣ
⊢ Dvd.dvd (α := ℕ) ((λ : (a : ℕ) → ℕ) a : ℕ) ((λ : (a : ℕ) → ℕ) (n + 1) : ℕ)

Tactic:
rw [carmichael_eq_exponent <| ne_zero_of_dvd_ne_zero (by lia) h, carmichael_eq_exponent']

Premises used: ArithmeticFunction.carmichael_eq_exponent', ArithmeticFunction.carmichael_eq_exponent, ne_zero_of_dvd_ne_zero
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Carmichael
Goal:
a n : ℕ
h : a ∣ n + 1
⊢ exponent (ZMod a)ˣ ∣ exponent (ZMod (n + 1))ˣ

Tactic:
MonoidHom.exponent_dvd <| ZMod.unitsMap_surjective h

Premises used: ZMod.unitsMap_surjective, MonoidHom.exponent_dvd
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Carmichael
Goal:
a n : ℕ
h : a ∣ n + 1
⊢ exponent (ZMod a)ˣ ∣ exponent (ZMod (n + 1))ˣ

Tactic:
exact MonoidHom.exponent_dvd <| ZMod.unitsMap_surjective h

Premises used: ZMod.unitsMap_surjective, MonoidHom.exponent_dvd
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Carmichael
Goal:
a b : ℕ
pos : ∀ (h₀ : a = 0 ∨ b = 0), (λ : (a : ℕ) → ℕ) (a.lcm b) = Nat.lcm ((λ : (a : ℕ) → ℕ) a) ((λ : (a : ℕ) → ℕ) b)
neg : ∀ (h₀ : a ≠ 0 ∧ b ≠ 0), (λ : (a : ℕ) → ℕ) (a.lcm b) = Nat.lcm ((λ : (a : ℕ) → ℕ) a) ((λ : (a : ℕ) → ℕ) b)
⊢ (λ : (a : ℕ) → ℕ) (a.lcm b) = Nat.lcm ((λ : (a : ℕ) → ℕ) a) ((λ : (a : ℕ) → ℕ) b)

Tactic:
by_cases! h₀ : a = 0 ∨ b = 0
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Carmichael
Goal:
a b : ℕ
h₀ : a = 0 ∨ b = 0
⊢ (λ : (a : ℕ) → ℕ) (a.lcm b) = Nat.lcm ((λ : (a : ℕ) → ℕ) a) ((λ : (a : ℕ) → ℕ) b)

Tactic:
grind [Nat.lcm_eq_zero_iff, map_zero]

Premises used: Nat.lcm_eq_zero_iff, ArithmeticFunction.map_zero
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Carmichael
Goal:
a b : ℕ
h₀ : a ≠ 0 ∧ b ≠ 0
neg : (λ : (a : ℕ) → ℕ) (a.lcm b) ∣ Nat.lcm ((λ : (a : ℕ) → ℕ) a) ((λ : (a : ℕ) → ℕ) b)
neg₁ : Nat.lcm ((λ : (a : ℕ) → ℕ) a) ((λ : (a : ℕ) → ℕ) b) ∣ (λ : (a : ℕ) → ℕ) (a.lcm b)
⊢ (λ : (a : ℕ) → ℕ) (a.lcm b) = Nat.lcm ((λ : (a : ℕ) → ℕ) a) ((λ : (a : ℕ) → ℕ) b)

Tactic:
apply dvd_antisymm

Premises used: dvd_antisymm