internlm/Lean-Github huggingface dataset:
Theorem: deriv_ζ₁_apply_of_ne_one
Proof state before:
z : ℂ
hz : z ≠ 1
⊢ deriv ζ₁ z = deriv ζ z * (z - 1) + ζ z
Tactic:
have H : deriv ζ₁ z = deriv (fun w ↦ ζ w * (w - 1)) z := by
  refine Filter.EventuallyEq.deriv_eq <| Filter.eventuallyEq_iff_exists_mem.mpr ?_
  refine ⟨{w | w ≠ 1}, IsOpen.mem_nhds isOpen_ne hz, fun w hw ↦ ?_⟩
  simp only [ζ₁, ne_eq, Set.mem_setOf.mp hw, not_false_eq_true, Function.update_noteq]
Proof state after:
z : ℂ
hz : z ≠ 1
H : deriv ζ₁ z = deriv (fun w => ζ w * (w - 1)) z
⊢ deriv ζ₁ z = deriv ζ z * (z - 1) + ζ z
Theorem: deriv_ζ₁_apply_of_ne_one
Proof state before:
z : ℂ
hz : z ≠ 1
H : deriv ζ₁ z = deriv (fun w => ζ w * (w - 1)) z
⊢ deriv ζ₁ z = deriv ζ z * (z - 1) + ζ z
Tactic:
rw [H, deriv_mul (differentiableAt_riemannZeta hz) <| differentiableAt_id'.sub <|
  differentiableAt_const 1, deriv_sub_const, deriv_id'', mul_one]
Proof state after:
no goals
Theorem: deriv_ζ₁_apply_of_ne_one
Proof state before:
z : ℂ
hz : z ≠ 1
⊢ deriv ζ₁ z = deriv (fun w => ζ w * (w - 1)) z
Tactic:
refine Filter.EventuallyEq.deriv_eq <| Filter.eventuallyEq_iff_exists_mem.mpr ?_
Proof state after:
z : ℂ
hz : z ≠ 1
⊢ ∃ s ∈ nhds z, Set.EqOn ζ₁ (fun w => ζ w * (w - 1)) s
Theorem: deriv_ζ₁_apply_of_ne_one
Proof state before:
z : ℂ
hz : z ≠ 1
⊢ ∃ s ∈ nhds z, Set.EqOn ζ₁ (fun w => ζ w * (w - 1)) s
Tactic:
refine ⟨{w | w ≠ 1}, IsOpen.mem_nhds isOpen_ne hz, fun w hw ↦ ?_⟩
Proof state after:
z : ℂ
hz : z ≠ 1
w : ℂ
hw : w ∈ {w | w ≠ 1}
⊢ ζ₁ w = (fun w => ζ w * (w - 1)) w
Theorem: deriv_ζ₁_apply_of_ne_one
Proof state before:
z : ℂ
hz : z ≠ 1
w : ℂ
hw : w ∈ {w | w ≠ 1}
⊢ ζ₁ w = (fun w => ζ w * (w - 1)) w
Tactic:
simp only [ζ₁, ne_eq, Set.mem_setOf.mp hw, not_false_eq_true, Function.update_noteq]
Proof state after:
no goals
Theorem: neg_logDeriv_ζ₁_eq
Proof state before:
z : ℂ
hz₁ : z ≠ 1
hz₂ : ζ z ≠ 0
⊢ -deriv ζ₁ z / ζ₁ z = -deriv ζ z / ζ z - 1 / (z - 1)
Tactic:
rw [ζ₁_apply_of_ne_one hz₁, deriv_ζ₁_apply_of_ne_one hz₁]
Proof state after:
z : ℂ
hz₁ : z ≠ 1
hz₂ : ζ z ≠ 0
⊢ -(deriv ζ z * (z - 1) + ζ z) / (ζ z * (z - 1)) = -deriv ζ z / ζ z - 1 / (z - 1)
Theorem: neg_logDeriv_ζ₁_eq
Proof state before:
z : ℂ
hz₁ : z ≠ 1
hz₂ : ζ z ≠ 0
⊢ -(deriv ζ z * (z - 1) + ζ z) / (ζ z * (z - 1)) = -deriv ζ z / ζ z - 1 / (z - 1)
Tactic:
field_simp [sub_ne_zero.mpr hz₁]
Proof state after:
z : ℂ
hz₁ : z ≠ 1
hz₂ : ζ z ≠ 0
⊢ -ζ z + -(deriv ζ z * (z - 1)) = -(deriv ζ z * (z - 1)) - ζ z
Theorem: neg_logDeriv_ζ₁_eq
Proof state before:
z : ℂ
hz₁ : z ≠ 1
hz₂ : ζ z ≠ 0
⊢ -ζ z + -(deriv ζ z * (z - 1)) = -(deriv ζ z * (z - 1)) - ζ z
Tactic:
ring
Proof state after:
no goals
Theorem: continuousOn_neg_logDeriv_ζ₁
Proof state before:
⊢ ContinuousOn (fun z => -deriv ζ₁ z / ζ₁ z) {z | z = 1 ∨ ζ z ≠ 0}
Tactic:
simp_rw [neg_div]
Proof state after:
⊢ ContinuousOn (fun z => -(deriv ζ₁ z / ζ₁ z)) {z | z = 1 ∨ ζ z ≠ 0}
Theorem: continuousOn_neg_logDeriv_ζ₁
Proof state before:
⊢ ContinuousOn (fun z => -(deriv ζ₁ z / ζ₁ z)) {z | z = 1 ∨ ζ z ≠ 0}
Tactic:
refine ((ζ₁_differentiable.contDiff.continuous_deriv le_rfl).continuousOn.div
  ζ₁_differentiable.continuous.continuousOn fun w hw ↦ ?_).neg
Proof state after:
w : ℂ
hw : w ∈ {z | z = 1 ∨ ζ z ≠ 0}
⊢ ζ₁ w ≠ 0
Theorem: continuousOn_neg_logDeriv_ζ₁
Proof state before:
w : ℂ
hw : w ∈ {z | z = 1 ∨ ζ z ≠ 0}
⊢ ζ₁ w ≠ 0
Tactic:
rcases eq_or_ne w 1 with rfl | hw'
Proof state after:
case inl
hw : 1 ∈ {z | z = 1 ∨ ζ z ≠ 0}
⊢ ζ₁ 1 ≠ 0

case inr
w : ℂ
hw : w ∈ {z | z = 1 ∨ ζ z ≠ 0}
hw' : w ≠ 1
⊢ ζ₁ w ≠ 0
Theorem: continuousOn_neg_logDeriv_ζ₁
Proof state before:
case inl
hw : 1 ∈ {z | z = 1 ∨ ζ z ≠ 0}
⊢ ζ₁ 1 ≠ 0
Tactic:
simp only [ζ₁, Function.update_same, ne_eq, one_ne_zero, not_false_eq_true]
Proof state after:
no goals
Theorem: continuousOn_neg_logDeriv_ζ₁
Proof state before:
case inr
w : ℂ
hw : w ∈ {z | z = 1 ∨ ζ z ≠ 0}
hw' : w ≠ 1
⊢ ζ₁ w ≠ 0
Tactic:
simp only [ne_eq, Set.mem_setOf_eq, hw', false_or] at hw
Proof state after:
case inr
w : ℂ
hw' : w ≠ 1
hw : ¬ζ w = 0
⊢ ζ₁ w ≠ 0
Theorem: continuousOn_neg_logDeriv_ζ₁
Proof state before:
case inr
w : ℂ
hw' : w ≠ 1
hw : ¬ζ w = 0
⊢ ζ₁ w ≠ 0
Tactic:
simp only [ζ₁, ne_eq, hw', not_false_eq_true, Function.update_noteq, _root_.mul_eq_zero, hw,
  false_or]
Proof state after:
case inr
w : ℂ
hw' : w ≠ 1
hw : ¬ζ w = 0
⊢ ¬w - 1 = 0
Theorem: continuousOn_neg_logDeriv_ζ₁
Proof state before:
case inr
w : ℂ
hw' : w ≠ 1
hw : ¬ζ w = 0
⊢ ¬w - 1 = 0
Tactic:
exact sub_ne_zero.mpr hw'
Proof state after:
no goals
Theorem: PNT_vonMangoldt
Proof state before:
WIT : WienerIkeharaTheorem
⊢ Tendsto (fun N => (Finset.range N).sum ⇑Λ / ↑N) atTop (nhds 1)
Tactic:
have hnv := riemannZeta_ne_zero_of_one_le_re
Proof state after:
WIT : WienerIkeharaTheorem
hnv : ∀ ⦃z : ℂ⦄, z ≠ 1 → 1 ≤ z.re → ζ z ≠ 0
⊢ Tendsto (fun N => (Finset.range N).sum ⇑Λ / ↑N) atTop (nhds 1)
Theorem: PNT_vonMangoldt
Proof state before:
WIT : WienerIkeharaTheorem
hnv : ∀ ⦃z : ℂ⦄, z ≠ 1 → 1 ≤ z.re → ζ z ≠ 0
⊢ Tendsto (fun N => (Finset.range N).sum ⇑Λ / ↑N) atTop (nhds 1)
Tactic:
refine WIT (F := fun z ↦ -deriv ζ₁ z / ζ₁ z) (fun _ ↦ vonMangoldt_nonneg) (fun s hs ↦ ?_) ?_
Proof state after:
case refine_1
WIT : WienerIkeharaTheorem
hnv : ∀ ⦃z : ℂ⦄, z ≠ 1 → 1 ≤ z.re → ζ z ≠ 0
s : ℂ
hs : s ∈ {s | 1 < s.re}
⊢ (fun z => -deriv ζ₁ z / ζ₁ z) s = (fun s => L (fun n => ↑(Λ n)) s - ↑1 / (s - 1)) s

case refine_2
WIT : WienerIkeharaTheorem
hnv : ∀ ⦃z : ℂ⦄, z ≠ 1 → 1 ≤ z.re → ζ z ≠ 0
⊢ ContinuousOn (fun z => -deriv ζ₁ z / ζ₁ z) {s | 1 ≤ s.re}
Theorem: PNT_vonMangoldt
Proof state before:
case refine_1
WIT : WienerIkeharaTheorem
hnv : ∀ ⦃z : ℂ⦄, z ≠ 1 → 1 ≤ z.re → ζ z ≠ 0
s : ℂ
hs : s ∈ {s | 1 < s.re}
⊢ (fun z => -deriv ζ₁ z / ζ₁ z) s = (fun s => L (fun n => ↑(Λ n)) s - ↑1 / (s - 1)) s
Tactic:
have hs₁ : s ≠ 1 := by
  rintro rfl
  simp at hs
Proof state after:
case refine_1
WIT : WienerIkeharaTheorem
hnv : ∀ ⦃z : ℂ⦄, z ≠ 1 → 1 ≤ z.re → ζ z ≠ 0
s : ℂ
hs : s ∈ {s | 1 < s.re}
hs₁ : s ≠ 1
⊢ (fun z => -deriv ζ₁ z / ζ₁ z) s = (fun s => L (fun n => ↑(Λ n)) s - ↑1 / (s - 1)) s
Theorem: PNT_vonMangoldt
Proof state before:
case refine_1
WIT : WienerIkeharaTheorem
hnv : ∀ ⦃z : ℂ⦄, z ≠ 1 → 1 ≤ z.re → ζ z ≠ 0
s : ℂ
hs : s ∈ {s | 1 < s.re}
hs₁ : s ≠ 1
⊢ (fun z => -deriv ζ₁ z / ζ₁ z) s = (fun s => L (fun n => ↑(Λ n)) s - ↑1 / (s - 1)) s
Tactic:
simp only [ne_eq, hs₁, not_false_eq_true, LSeries_vonMangoldt_eq_deriv_riemannZeta_div hs,
  ofReal_one]
Proof state after:
case refine_1
WIT : WienerIkeharaTheorem
hnv : ∀ ⦃z : ℂ⦄, z ≠ 1 → 1 ≤ z.re → ζ z ≠ 0
s : ℂ
hs : s ∈ {s | 1 < s.re}
hs₁ : s ≠ 1
⊢ -deriv ζ₁ s / ζ₁ s = -deriv ζ s / ζ s - 1 / (s - 1)
Theorem: PNT_vonMangoldt
Proof state before:
case refine_1
WIT : WienerIkeharaTheorem
hnv : ∀ ⦃z : ℂ⦄, z ≠ 1 → 1 ≤ z.re → ζ z ≠ 0
s : ℂ
hs : s ∈ {s | 1 < s.re}
hs₁ : s ≠ 1
⊢ -deriv ζ₁ s / ζ₁ s = -deriv ζ s / ζ s - 1 / (s - 1)
Tactic:
exact neg_logDeriv_ζ₁_eq hs₁ <| hnv hs₁ (Set.mem_setOf.mp hs).le
Proof state after:
no goals
Theorem: PNT_vonMangoldt
Proof state before:
WIT : WienerIkeharaTheorem
hnv : ∀ ⦃z : ℂ⦄, z ≠ 1 → 1 ≤ z.re → ζ z ≠ 0
s : ℂ
hs : s ∈ {s | 1 < s.re}
⊢ s ≠ 1
Tactic:
rintro rfl
Proof state after:
WIT : WienerIkeharaTheorem
hnv : ∀ ⦃z : ℂ⦄, z ≠ 1 → 1 ≤ z.re → ζ z ≠ 0
hs : 1 ∈ {s | 1 < s.re}
⊢ False
Theorem: PNT_vonMangoldt
Proof state before:
WIT : WienerIkeharaTheorem
hnv : ∀ ⦃z : ℂ⦄, z ≠ 1 → 1 ≤ z.re → ζ z ≠ 0
hs : 1 ∈ {s | 1 < s.re}
⊢ False
Tactic:
simp at hs
Proof state after:
no goals
Theorem: PNT_vonMangoldt
Proof state before:
case refine_2
WIT : WienerIkeharaTheorem
hnv : ∀ ⦃z : ℂ⦄, z ≠ 1 → 1 ≤ z.re → ζ z ≠ 0
⊢ ContinuousOn (fun z => -deriv ζ₁ z / ζ₁ z) {s | 1 ≤ s.re}
Tactic:
refine continuousOn_neg_logDeriv_ζ₁.mono fun s _ ↦ ?_
Proof state after:
case refine_2
WIT : WienerIkeharaTheorem
hnv : ∀ ⦃z : ℂ⦄, z ≠ 1 → 1 ≤ z.re → ζ z ≠ 0
s : ℂ
x✝ : s ∈ {s | 1 ≤ s.re}
⊢ s ∈ {z | z = 1 ∨ ζ z ≠ 0}
Theorem: PNT_vonMangoldt
Proof state before:
case refine_2
WIT : WienerIkeharaTheorem
hnv : ∀ ⦃z : ℂ⦄, z ≠ 1 → 1 ≤ z.re → ζ z ≠ 0
s : ℂ
x✝ : s ∈ {s | 1 ≤ s.re}
⊢ s ∈ {z | z = 1 ∨ ζ z ≠ 0}
Tactic:
specialize @hnv s
Proof state after:
case refine_2
WIT : WienerIkeharaTheorem
s : ℂ
x✝ : s ∈ {s | 1 ≤ s.re}
hnv : s ≠ 1 → 1 ≤ s.re → ζ s ≠ 0
⊢ s ∈ {z | z = 1 ∨ ζ z ≠ 0}
Theorem: PNT_vonMangoldt
Proof state before:
case refine_2
WIT : WienerIkeharaTheorem
s : ℂ
x✝ : s ∈ {s | 1 ≤ s.re}
hnv : s ≠ 1 → 1 ≤ s.re → ζ s ≠ 0
⊢ s ∈ {z | z = 1 ∨ ζ z ≠ 0}
Tactic:
simp at *
Proof state after:
case refine_2
WIT : WienerIkeharaTheorem
s : ℂ
x✝ : 1 ≤ s.re
hnv : ¬s = 1 → 1 ≤ s.re → ¬ζ s = 0
⊢ s = 1 ∨ ¬ζ s = 0
Theorem: PNT_vonMangoldt
Proof state before:
case refine_2
WIT : WienerIkeharaTheorem
s : ℂ
x✝ : 1 ≤ s.re
hnv : ¬s = 1 → 1 ≤ s.re → ¬ζ s = 0
⊢ s = 1 ∨ ¬ζ s = 0
Tactic:
tauto
Proof state after:
no goals
Theorem: Complex.cpow_natCast_add_one_ne_zero
Proof state before:
n : ℕ
z : ℂ
H : ↑n + 1 = 0 ∧ z ≠ 0
⊢ False
Tactic:
norm_cast at H
Proof state after:
n : ℕ
z : ℂ
H : False ∧ ¬z = 0
⊢ False
Theorem: Complex.cpow_natCast_add_one_ne_zero
Proof state before:
n : ℕ
z : ℂ
H : False ∧ ¬z = 0
⊢ False
Tactic:
exact H.1
Proof state after:
no goals
Theorem: LSeries.abscissaOfAbsConv_binop_le
Proof state before:
F : (ℕ → ℂ) → (ℕ → ℂ) → ℕ → ℂ
hF : ∀ {f g : ℕ → ℂ} {s : ℂ}, LSeriesSummable f s → LSeriesSummable g s → LSeriesSummable (F f g) s
f g : ℕ → ℂ
⊢ abscissaOfAbsConv (F f g) ≤ max (abscissaOfAbsConv f) (abscissaOfAbsConv g)
Tactic:
refine abscissaOfAbsConv_le_of_forall_lt_LSeriesSummable' fun x hx ↦  hF ?_ ?_
Proof state after:
case refine_1
F : (ℕ → ℂ) → (ℕ → ℂ) → ℕ → ℂ
hF : ∀ {f g : ℕ → ℂ} {s : ℂ}, LSeriesSummable f s → LSeriesSummable g s → LSeriesSummable (F f g) s
f g : ℕ → ℂ
x : ℝ
hx : max (abscissaOfAbsConv f) (abscissaOfAbsConv g) < ↑x
⊢ LSeriesSummable f ↑x

case refine_2
F : (ℕ → ℂ) → (ℕ → ℂ) → ℕ → ℂ
hF : ∀ {f g : ℕ → ℂ} {s : ℂ}, LSeriesSummable f s → LSeriesSummable g s → LSeriesSummable (F f g) s
f g : ℕ → ℂ
x : ℝ
hx : max (abscissaOfAbsConv f) (abscissaOfAbsConv g) < ↑x
⊢ LSeriesSummable g ↑x
Theorem: LSeries.abscissaOfAbsConv_binop_le
Proof state before:
case refine_1
F : (ℕ → ℂ) → (ℕ → ℂ) → ℕ → ℂ
hF : ∀ {f g : ℕ → ℂ} {s : ℂ}, LSeriesSummable f s → LSeriesSummable g s → LSeriesSummable (F f g) s
f g : ℕ → ℂ
x : ℝ
hx : max (abscissaOfAbsConv f) (abscissaOfAbsConv g) < ↑x
⊢ LSeriesSummable f ↑x
Tactic:
exact LSeriesSummable_of_abscissaOfAbsConv_lt_re <|
  (ofReal_re x).symm ▸ (le_max_left ..).trans_lt hx
Proof state after:
no goals
Theorem: LSeries.abscissaOfAbsConv_binop_le
Proof state before:
case refine_2
F : (ℕ → ℂ) → (ℕ → ℂ) → ℕ → ℂ
hF : ∀ {f g : ℕ → ℂ} {s : ℂ}, LSeriesSummable f s → LSeriesSummable g s → LSeriesSummable (F f g) s
f g : ℕ → ℂ
x : ℝ
hx : max (abscissaOfAbsConv f) (abscissaOfAbsConv g) < ↑x
⊢ LSeriesSummable g ↑x
Tactic:
exact LSeriesSummable_of_abscissaOfAbsConv_lt_re <|
    (ofReal_re x).symm ▸ (le_max_right ..).trans_lt hx
Proof state after:
no goals
Theorem: foo
Proof state before:
m n : ℕ
z : ℂ
x : ℝ
⊢ (↑n + 1) ^ ↑x * (z / ↑m ^ ↑x) = z / (↑m / (↑n + 1)) ^ ↑x
Tactic:
have Hm : (0 : ℝ) ≤ m := m.cast_nonneg
Proof state after:
m n : ℕ
z : ℂ
x : ℝ
Hm : 0 ≤ ↑m
⊢ (↑n + 1) ^ ↑x * (z / ↑m ^ ↑x) = z / (↑m / (↑n + 1)) ^ ↑x
Theorem: foo
Proof state before:
m n : ℕ
z : ℂ
x : ℝ
Hm : 0 ≤ ↑m
⊢ (↑n + 1) ^ ↑x * (z / ↑m ^ ↑x) = z / (↑m / (↑n + 1)) ^ ↑x
Tactic:
have Hn : (0 : ℝ) ≤ (n + 1 : ℝ)⁻¹ := by positivity
Proof state after:
m n : ℕ
z : ℂ
x : ℝ
Hm : 0 ≤ ↑m
Hn : 0 ≤ (↑n + 1)⁻¹
⊢ (↑n + 1) ^ ↑x * (z / ↑m ^ ↑x) = z / (↑m / (↑n + 1)) ^ ↑x
Theorem: foo
Proof state before:
m n : ℕ
z : ℂ
x : ℝ
Hm : 0 ≤ ↑m
Hn : 0 ≤ (↑n + 1)⁻¹
⊢ (↑n + 1) ^ ↑x * (z / ↑m ^ ↑x) = z / (↑m / (↑n + 1)) ^ ↑x
Tactic:
rw [← mul_div_assoc, mul_comm, div_eq_mul_inv z, mul_div_assoc]
Proof state after:
m n : ℕ
z : ℂ
x : ℝ
Hm : 0 ≤ ↑m
Hn : 0 ≤ (↑n + 1)⁻¹
⊢ z * ((↑n + 1) ^ ↑x / ↑m ^ ↑x) = z * ((↑m / (↑n + 1)) ^ ↑x)⁻¹
Theorem: foo
Proof state before:
m n : ℕ
z : ℂ
x : ℝ
Hm : 0 ≤ ↑m
Hn : 0 ≤ (↑n + 1)⁻¹
⊢ z * ((↑n + 1) ^ ↑x / ↑m ^ ↑x) = z * ((↑m / (↑n + 1)) ^ ↑x)⁻¹
Tactic:
congr
Proof state after:
case e_a
m n : ℕ
z : ℂ
x : ℝ
Hm : 0 ≤ ↑m
Hn : 0 ≤ (↑n + 1)⁻¹
⊢ (↑n + 1) ^ ↑x / ↑m ^ ↑x = ((↑m / (↑n + 1)) ^ ↑x)⁻¹
Theorem: foo
Proof state before:
case e_a
m n : ℕ
z : ℂ
x : ℝ
Hm : 0 ≤ ↑m
Hn : 0 ≤ (↑n + 1)⁻¹
⊢ (↑n + 1) ^ ↑x / ↑m ^ ↑x = ((↑m / (↑n + 1)) ^ ↑x)⁻¹
Tactic:
simp_rw [div_eq_mul_inv]
Proof state after:
case e_a
m n : ℕ
z : ℂ
x : ℝ
Hm : 0 ≤ ↑m
Hn : 0 ≤ (↑n + 1)⁻¹
⊢ (↑n + 1) ^ ↑x * (↑m ^ ↑x)⁻¹ = ((↑m * (↑n + 1)⁻¹) ^ ↑x)⁻¹
Theorem: foo
Proof state before:
case e_a
m n : ℕ
z : ℂ
x : ℝ
Hm : 0 ≤ ↑m
Hn : 0 ≤ (↑n + 1)⁻¹
⊢ (↑n + 1) ^ ↑x * (↑m ^ ↑x)⁻¹ = ((↑m * (↑n + 1)⁻¹) ^ ↑x)⁻¹
Tactic:
rw [show (n + 1 : ℂ)⁻¹ = (n + 1 : ℝ)⁻¹ by
      simp only [ofReal_inv, ofReal_add, ofReal_natCast, ofReal_one],
  show (n + 1 : ℂ) = (n + 1 : ℝ) by norm_cast, show (m : ℂ) = (m : ℝ) by norm_cast,
  mul_cpow_ofReal_nonneg Hm Hn, mul_inv, mul_comm]
Proof state after:
case e_a
m n : ℕ
z : ℂ
x : ℝ
Hm : 0 ≤ ↑m
Hn : 0 ≤ (↑n + 1)⁻¹
⊢ (↑↑m ^ ↑x)⁻¹ * ↑(↑n + 1) ^ ↑x = (↑↑m ^ ↑x)⁻¹ * (↑(↑n + 1)⁻¹ ^ ↑x)⁻¹
Theorem: foo
Proof state before:
case e_a
m n : ℕ
z : ℂ
x : ℝ
Hm : 0 ≤ ↑m
Hn : 0 ≤ (↑n + 1)⁻¹
⊢ (↑↑m ^ ↑x)⁻¹ * ↑(↑n + 1) ^ ↑x = (↑↑m ^ ↑x)⁻¹ * (↑(↑n + 1)⁻¹ ^ ↑x)⁻¹
Tactic:
congr
Proof state after:
case e_a.e_a
m n : ℕ
z : ℂ
x : ℝ
Hm : 0 ≤ ↑m
Hn : 0 ≤ (↑n + 1)⁻¹
⊢ ↑(↑n + 1) ^ ↑x = (↑(↑n + 1)⁻¹ ^ ↑x)⁻¹
Theorem: foo
Proof state before:
case e_a.e_a
m n : ℕ
z : ℂ
x : ℝ
Hm : 0 ≤ ↑m
Hn : 0 ≤ (↑n + 1)⁻¹
⊢ ↑(↑n + 1) ^ ↑x = (↑(↑n + 1)⁻¹ ^ ↑x)⁻¹
Tactic:
rw [← cpow_neg, show (-x : ℂ) = (-1 : ℝ) * x by simp only [ofReal_neg, ofReal_one,
  neg_mul, one_mul], cpow_mul_ofReal_nonneg Hn, Real.rpow_neg_one, inv_inv]
Proof state after:
no goals
Theorem: foo
Proof state before:
m n : ℕ
z : ℂ
x : ℝ
Hm : 0 ≤ ↑m
⊢ 0 ≤ (↑n + 1)⁻¹
Tactic:
positivity
Proof state after:
no goals
Theorem: foo
Proof state before:
m n : ℕ
z : ℂ
x : ℝ
Hm : 0 ≤ ↑m
Hn : 0 ≤ (↑n + 1)⁻¹
⊢ (↑n + 1)⁻¹ = ↑(↑n + 1)⁻¹
Tactic:
simp only [ofReal_inv, ofReal_add, ofReal_natCast, ofReal_one]
Proof state after:
no goals
Theorem: foo
Proof state before:
m n : ℕ
z : ℂ
x : ℝ
Hm : 0 ≤ ↑m
Hn : 0 ≤ (↑n + 1)⁻¹
⊢ ↑n + 1 = ↑(↑n + 1)
Tactic:
norm_cast
Proof state after:
no goals
Theorem: foo
Proof state before:
m n : ℕ
z : ℂ
x : ℝ
Hm : 0 ≤ ↑m
Hn : 0 ≤ (↑n + 1)⁻¹
⊢ ↑m = ↑↑m
Tactic:
norm_cast
Proof state after:
no goals
Theorem: foo
Proof state before:
m n : ℕ
z : ℂ
x : ℝ
Hm : 0 ≤ ↑m
Hn : 0 ≤ (↑n + 1)⁻¹
⊢ -↑x = ↑(-1) * ↑x
Tactic:
simp only [ofReal_neg, ofReal_one,
neg_mul, one_mul]
Proof state after:
no goals
Theorem: LSeries.pow_mul_term_eq
Proof state before:
f : ℕ → ℂ
s : ℂ
n : ℕ
⊢ (↑n + 1) ^ s * term f s (n + 1) = f (n + 1)
Tactic:
simp only [term, add_eq_zero, one_ne_zero, and_false, ↓reduceIte, Nat.cast_add, Nat.cast_one,
  mul_div_assoc', ne_eq, cpow_natCast_add_one_ne_zero n _, not_false_eq_true, div_eq_iff,
  mul_comm (f _)]
Proof state after:
no goals
Theorem: LSeries.tendsto_pow_mul_atTop
Proof state before:
f : ℕ → ℂ
n : ℕ
h : ∀ m ≤ n, f m = 0
ha : abscissaOfAbsConv f < ⊤
⊢ Tendsto (fun x => (↑n + 1) ^ ↑x * LSeries f ↑x) atTop (nhds (f (n + 1)))
Tactic:
obtain ⟨y, hay, hyt⟩ := exists_between ha
Proof state after:
case intro.intro
f : ℕ → ℂ
n : ℕ
h : ∀ m ≤ n, f m = 0
ha : abscissaOfAbsConv f < ⊤
y : EReal
hay : abscissaOfAbsConv f < y
hyt : y < ⊤
⊢ Tendsto (fun x => (↑n + 1) ^ ↑x * LSeries f ↑x) atTop (nhds (f (n + 1)))
Theorem: LSeries.tendsto_pow_mul_atTop
Proof state before:
case intro.intro
f : ℕ → ℂ
n : ℕ
h : ∀ m ≤ n, f m = 0
ha : abscissaOfAbsConv f < ⊤
y : EReal
hay : abscissaOfAbsConv f < y
hyt : y < ⊤
⊢ Tendsto (fun x => (↑n + 1) ^ ↑x * LSeries f ↑x) atTop (nhds (f (n + 1)))
Tactic:
lift y to ℝ using ⟨hyt.ne, ((OrderBot.bot_le _).trans_lt hay).ne'⟩
Proof state after:
case intro.intro.intro
f : ℕ → ℂ
n : ℕ
h : ∀ m ≤ n, f m = 0
ha : abscissaOfAbsConv f < ⊤
y : ℝ
hay : abscissaOfAbsConv f < ↑y
hyt : ↑y < ⊤
⊢ Tendsto (fun x => (↑n + 1) ^ ↑x * LSeries f ↑x) atTop (nhds (f (n + 1)))
Theorem: LSeries.tendsto_pow_mul_atTop
Proof state before:
case intro.intro.intro
f : ℕ → ℂ
n : ℕ
h : ∀ m ≤ n, f m = 0
ha : abscissaOfAbsConv f < ⊤
y : ℝ
hay : abscissaOfAbsConv f < ↑y
hyt : ↑y < ⊤
⊢ Tendsto (fun x => (↑n + 1) ^ ↑x * LSeries f ↑x) atTop (nhds (f (n + 1)))
Tactic:
let F := fun (x : ℝ) ↦ {m | n + 1 < m}.indicator (fun m ↦ f m / (m / (n + 1) : ℂ) ^ (x : ℂ))
Proof state after:
case intro.intro.intro
f : ℕ → ℂ
n : ℕ
h : ∀ m ≤ n, f m = 0
ha : abscissaOfAbsConv f < ⊤
y : ℝ
hay : abscissaOfAbsConv f < ↑y
hyt : ↑y < ⊤
F : ℝ → ℕ → ℂ := fun x => {m | n + 1 < m}.indicator fun m => f m / (↑m / (↑n + 1)) ^ ↑x
⊢ Tendsto (fun x => (↑n + 1) ^ ↑x * LSeries f ↑x) atTop (nhds (f (n + 1)))
Theorem: LSeries.tendsto_pow_mul_atTop
Proof state before:
case intro.intro.intro
f : ℕ → ℂ
n : ℕ
h : ∀ m ≤ n, f m = 0
ha : abscissaOfAbsConv f < ⊤
y : ℝ
hay : abscissaOfAbsConv f < ↑y
hyt : ↑y < ⊤
F : ℝ → ℕ → ℂ := fun x => {m | n + 1 < m}.indicator fun m => f m / (↑m / (↑n + 1)) ^ ↑x
⊢ Tendsto (fun x => (↑n + 1) ^ ↑x * LSeries f ↑x) atTop (nhds (f (n + 1)))
Tactic:
have hF₀ (x : ℝ) {m : ℕ} (hm : m ≤ n + 1) : F x m = 0 := by
  simp only [Set.mem_setOf_eq, not_lt_of_le hm, not_false_eq_true, Set.indicator_of_not_mem, F]
Proof state after:
case intro.intro.intro
f : ℕ → ℂ
n : ℕ
h : ∀ m ≤ n, f m = 0
ha : abscissaOfAbsConv f < ⊤
y : ℝ
hay : abscissaOfAbsConv f < ↑y
hyt : ↑y < ⊤
F : ℝ → ℕ → ℂ := fun x => {m | n + 1 < m}.indicator fun m => f m / (↑m / (↑n + 1)) ^ ↑x
hF₀ : ∀ (x : ℝ) {m : ℕ}, m ≤ n + 1 → F x m = 0
⊢ Tendsto (fun x => (↑n + 1) ^ ↑x * LSeries f ↑x) atTop (nhds (f (n + 1)))
Theorem: LSeries.tendsto_pow_mul_atTop
Proof state before:
case intro.intro.intro
f : ℕ → ℂ
n : ℕ
h : ∀ m ≤ n, f m = 0
ha : abscissaOfAbsConv f < ⊤
y : ℝ
hay : abscissaOfAbsConv f < ↑y
hyt : ↑y < ⊤
F : ℝ → ℕ → ℂ := fun x => {m | n + 1 < m}.indicator fun m => f m / (↑m / (↑n + 1)) ^ ↑x
hF₀ : ∀ (x : ℝ) {m : ℕ}, m ≤ n + 1 → F x m = 0
hF : ∀ (x : ℝ) {m : ℕ}, m ≠ n + 1 → F x m = (↑n + 1) ^ ↑x * term f (↑x) m
⊢ Tendsto (fun x => (↑n + 1) ^ ↑x * LSeries f ↑x) atTop (nhds (f (n + 1)))
Tactic:
have hs {x : ℝ} (hx : x ≥ y) : Summable fun m ↦ (n + 1) ^ (x : ℂ) * term f x m := by
  refine (summable_mul_left_iff <| cpow_natCast_add_one_ne_zero n _).mpr <|
     LSeriesSummable_of_abscissaOfAbsConv_lt_re ?_
  simpa only [ofReal_re] using hay.trans_le <| EReal.coe_le_coe_iff.mpr hx
Proof state after:
case intro.intro.intro
f : ℕ → ℂ
n : ℕ
h : ∀ m ≤ n, f m = 0
ha : abscissaOfAbsConv f < ⊤
y : ℝ
hay : abscissaOfAbsConv f < ↑y
hyt : ↑y < ⊤
F : ℝ → ℕ → ℂ := fun x => {m | n + 1 < m}.indicator fun m => f m / (↑m / (↑n + 1)) ^ ↑x
hF₀ : ∀ (x : ℝ) {m : ℕ}, m ≤ n + 1 → F x m = 0
hF : ∀ (x : ℝ) {m : ℕ}, m ≠ n + 1 → F x m = (↑n + 1) ^ ↑x * term f (↑x) m
hs : ∀ {x : ℝ}, x ≥ y → Summable fun m => (↑n + 1) ^ ↑x * term f (↑x) m
⊢ Tendsto (fun x => (↑n + 1) ^ ↑x * LSeries f ↑x) atTop (nhds (f (n + 1)))
Theorem: LSeries.tendsto_pow_mul_atTop
Proof state before:
case intro.intro.intro
f : ℕ → ℂ
n : ℕ
h : ∀ m ≤ n, f m = 0
ha : abscissaOfAbsConv f < ⊤
y : ℝ
hay : abscissaOfAbsConv f < ↑y
hyt : ↑y < ⊤
F : ℝ → ℕ → ℂ := fun x => {m | n + 1 < m}.indicator fun m => f m / (↑m / (↑n + 1)) ^ ↑x
hF₀ : ∀ (x : ℝ) {m : ℕ}, m ≤ n + 1 → F x m = 0
hF : ∀ (x : ℝ) {m : ℕ}, m ≠ n + 1 → F x m = (↑n + 1) ^ ↑x * term f (↑x) m
hs : ∀ {x : ℝ}, x ≥ y → Summable fun m => (↑n + 1) ^ ↑x * term f (↑x) m
key : ∀ x ≥ y, (↑n + 1) ^ ↑x * LSeries f ↑x = f (n + 1) + ∑' (m : ℕ), F x m
⊢ Tendsto (fun x => (↑n + 1) ^ ↑x * LSeries f ↑x) atTop (nhds (f (n + 1)))
Tactic:
conv => enter [3, 1]; rw [← add_zero (f _)]
Proof state after:
case intro.intro.intro
f : ℕ → ℂ
n : ℕ
h : ∀ m ≤ n, f m = 0
ha : abscissaOfAbsConv f < ⊤
y : ℝ
hay : abscissaOfAbsConv f < ↑y
hyt : ↑y < ⊤
F : ℝ → ℕ → ℂ := fun x => {m | n + 1 < m}.indicator fun m => f m / (↑m / (↑n + 1)) ^ ↑x
hF₀ : ∀ (x : ℝ) {m : ℕ}, m ≤ n + 1 → F x m = 0
hF : ∀ (x : ℝ) {m : ℕ}, m ≠ n + 1 → F x m = (↑n + 1) ^ ↑x * term f (↑x) m
hs : ∀ {x : ℝ}, x ≥ y → Summable fun m => (↑n + 1) ^ ↑x * term f (↑x) m
key : ∀ x ≥ y, (↑n + 1) ^ ↑x * LSeries f ↑x = f (n + 1) + ∑' (m : ℕ), F x m
⊢ Tendsto (fun x => (↑n + 1) ^ ↑x * LSeries f ↑x) atTop (nhds (f (n + 1) + 0))
Theorem: LSeries.tendsto_pow_mul_atTop
Proof state before:
case intro.intro.intro
f : ℕ → ℂ
n : ℕ
h : ∀ m ≤ n, f m = 0
ha : abscissaOfAbsConv f < ⊤
y : ℝ
hay : abscissaOfAbsConv f < ↑y
hyt : ↑y < ⊤
F : ℝ → ℕ → ℂ := fun x => {m | n + 1 < m}.indicator fun m => f m / (↑m / (↑n + 1)) ^ ↑x
hF₀ : ∀ (x : ℝ) {m : ℕ}, m ≤ n + 1 → F x m = 0
hF : ∀ (x : ℝ) {m : ℕ}, m ≠ n + 1 → F x m = (↑n + 1) ^ ↑x * term f (↑x) m
hs : ∀ {x : ℝ}, x ≥ y → Summable fun m => (↑n + 1) ^ ↑x * term f (↑x) m
key : ∀ x ≥ y, (↑n + 1) ^ ↑x * LSeries f ↑x = f (n + 1) + ∑' (m : ℕ), F x m
⊢ Tendsto (fun x => (↑n + 1) ^ ↑x * LSeries f ↑x) atTop (nhds (f (n + 1) + 0))
Tactic:
refine Tendsto.congr'
  (eventuallyEq_of_mem (s := {x | y ≤ x}) (mem_atTop y) key).symm <| tendsto_const_nhds.add ?_
Proof state after:
case intro.intro.intro
f : ℕ → ℂ
n : ℕ
h : ∀ m ≤ n, f m = 0
ha : abscissaOfAbsConv f < ⊤
y : ℝ
hay : abscissaOfAbsConv f < ↑y
hyt : ↑y < ⊤
F : ℝ → ℕ → ℂ := fun x => {m | n + 1 < m}.indicator fun m => f m / (↑m / (↑n + 1)) ^ ↑x
hF₀ : ∀ (x : ℝ) {m : ℕ}, m ≤ n + 1 → F x m = 0
hF : ∀ (x : ℝ) {m : ℕ}, m ≠ n + 1 → F x m = (↑n + 1) ^ ↑x * term f (↑x) m
hs : ∀ {x : ℝ}, x ≥ y → Summable fun m => (↑n + 1) ^ ↑x * term f (↑x) m
key : ∀ x ≥ y, (↑n + 1) ^ ↑x * LSeries f ↑x = f (n + 1) + ∑' (m : ℕ), F x m
⊢ Tendsto (fun x => ∑' (m : ℕ), F x m) atTop (nhds 0)
Theorem: LSeries.tendsto_pow_mul_atTop
Proof state before:
case intro.intro.intro
f : ℕ → ℂ
n : ℕ
h : ∀ m ≤ n, f m = 0
ha : abscissaOfAbsConv f < ⊤
y : ℝ
hay : abscissaOfAbsConv f < ↑y
hyt : ↑y < ⊤
F : ℝ → ℕ → ℂ := fun x => {m | n + 1 < m}.indicator fun m => f m / (↑m / (↑n + 1)) ^ ↑x
hF₀ : ∀ (x : ℝ) {m : ℕ}, m ≤ n + 1 → F x m = 0
hF : ∀ (x : ℝ) {m : ℕ}, m ≠ n + 1 → F x m = (↑n + 1) ^ ↑x * term f (↑x) m
hs : ∀ {x : ℝ}, x ≥ y → Summable fun m => (↑n + 1) ^ ↑x * term f (↑x) m
key : ∀ x ≥ y, (↑n + 1) ^ ↑x * LSeries f ↑x = f (n + 1) + ∑' (m : ℕ), F x m
hys : Summable (F y)
hc : ∀ (k : ℕ), Tendsto (fun x => F x k) atTop (nhds 0)
⊢ Tendsto (fun x => ∑' (m : ℕ), F x m) atTop (nhds 0)
Tactic:
rw [show (0 : ℂ) = tsum (fun _ : ℕ ↦ 0) from tsum_zero.symm]
Proof state after:
case intro.intro.intro
f : ℕ → ℂ
n : ℕ
h : ∀ m ≤ n, f m = 0
ha : abscissaOfAbsConv f < ⊤
y : ℝ
hay : abscissaOfAbsConv f < ↑y
hyt : ↑y < ⊤
F : ℝ → ℕ → ℂ := fun x => {m | n + 1 < m}.indicator fun m => f m / (↑m / (↑n + 1)) ^ ↑x
hF₀ : ∀ (x : ℝ) {m : ℕ}, m ≤ n + 1 → F x m = 0
hF : ∀ (x : ℝ) {m : ℕ}, m ≠ n + 1 → F x m = (↑n + 1) ^ ↑x * term f (↑x) m
hs : ∀ {x : ℝ}, x ≥ y → Summable fun m => (↑n + 1) ^ ↑x * term f (↑x) m
key : ∀ x ≥ y, (↑n + 1) ^ ↑x * LSeries f ↑x = f (n + 1) + ∑' (m : ℕ), F x m
hys : Summable (F y)
hc : ∀ (k : ℕ), Tendsto (fun x => F x k) atTop (nhds 0)
⊢ Tendsto (fun x => ∑' (m : ℕ), F x m) atTop (nhds (∑' (x : ℕ), 0))
Theorem: LSeries.tendsto_pow_mul_atTop
Proof state before:
case intro.intro.intro
f : ℕ → ℂ
n : ℕ
h : ∀ m ≤ n, f m = 0
ha : abscissaOfAbsConv f < ⊤
y : ℝ
hay : abscissaOfAbsConv f < ↑y
hyt : ↑y < ⊤
F : ℝ → ℕ → ℂ := fun x => {m | n + 1 < m}.indicator fun m => f m / (↑m / (↑n + 1)) ^ ↑x
hF₀ : ∀ (x : ℝ) {m : ℕ}, m ≤ n + 1 → F x m = 0
hF : ∀ (x : ℝ) {m : ℕ}, m ≠ n + 1 → F x m = (↑n + 1) ^ ↑x * term f (↑x) m
hs : ∀ {x : ℝ}, x ≥ y → Summable fun m => (↑n + 1) ^ ↑x * term f (↑x) m
key : ∀ x ≥ y, (↑n + 1) ^ ↑x * LSeries f ↑x = f (n + 1) + ∑' (m : ℕ), F x m
hys : Summable (F y)
hc : ∀ (k : ℕ), Tendsto (fun x => F x k) atTop (nhds 0)
⊢ Tendsto (fun x => ∑' (m : ℕ), F x m) atTop (nhds (∑' (x : ℕ), 0))
Tactic:
refine tendsto_tsum_of_dominated_convergence hys.norm hc <| eventually_iff.mpr ?_
Proof state after:
case intro.intro.intro
f : ℕ → ℂ
n : ℕ
h : ∀ m ≤ n, f m = 0
ha : abscissaOfAbsConv f < ⊤
y : ℝ
hay : abscissaOfAbsConv f < ↑y
hyt : ↑y < ⊤
F : ℝ → ℕ → ℂ := fun x => {m | n + 1 < m}.indicator fun m => f m / (↑m / (↑n + 1)) ^ ↑x
hF₀ : ∀ (x : ℝ) {m : ℕ}, m ≤ n + 1 → F x m = 0
hF : ∀ (x : ℝ) {m : ℕ}, m ≠ n + 1 → F x m = (↑n + 1) ^ ↑x * term f (↑x) m
hs : ∀ {x : ℝ}, x ≥ y → Summable fun m => (↑n + 1) ^ ↑x * term f (↑x) m
key : ∀ x ≥ y, (↑n + 1) ^ ↑x * LSeries f ↑x = f (n + 1) + ∑' (m : ℕ), F x m
hys : Summable (F y)
hc : ∀ (k : ℕ), Tendsto (fun x => F x k) atTop (nhds 0)
⊢ {x | ∀ (k : ℕ), ‖F x k‖ ≤ ‖F y k‖} ∈ atTop