internlm/Lean-Github huggingface dataset:
Theorem: Complex.monotoneOn_of_iteratedDeriv_nonneg
Proof state before:
f : ℂ → ℂ
hf : Differentiable ℂ f
h : ∀ (n : ℕ), 0 ≤ iteratedDeriv n f 0
D : ℕ → ℝ := fun n => (iteratedDeriv n f 0).re
hD : ∀ (n : ℕ), iteratedDeriv n f 0 = ↑(D n)
⊢ MonotoneOn (f ∘ ofReal') (Set.Ici 0)
Tactic:
obtain ⟨F, hFd, hF⟩ := realValued_of_iteratedDeriv_real hf hD
Proof state after:
case intro.intro
f : ℂ → ℂ
hf : Differentiable ℂ f
h : ∀ (n : ℕ), 0 ≤ iteratedDeriv n f 0
D : ℕ → ℝ := fun n => (iteratedDeriv n f 0).re
hD : ∀ (n : ℕ), iteratedDeriv n f 0 = ↑(D n)
F : ℝ → ℝ
hFd : Differentiable ℝ F
hF : f ∘ ofReal' = ofReal' ∘ F
⊢ MonotoneOn (f ∘ ofReal') (Set.Ici 0)
Theorem: Complex.monotoneOn_of_iteratedDeriv_nonneg
Proof state before:
case intro.intro
f : ℂ → ℂ
hf : Differentiable ℂ f
h : ∀ (n : ℕ), 0 ≤ iteratedDeriv n f 0
D : ℕ → ℝ := fun n => (iteratedDeriv n f 0).re
hD : ∀ (n : ℕ), iteratedDeriv n f 0 = ↑(D n)
F : ℝ → ℝ
hFd : Differentiable ℝ F
hF : f ∘ ofReal' = ofReal' ∘ F
⊢ MonotoneOn (f ∘ ofReal') (Set.Ici 0)
Tactic:
rw [hF]
Proof state after:
case intro.intro
f : ℂ → ℂ
hf : Differentiable ℂ f
h : ∀ (n : ℕ), 0 ≤ iteratedDeriv n f 0
D : ℕ → ℝ := fun n => (iteratedDeriv n f 0).re
hD : ∀ (n : ℕ), iteratedDeriv n f 0 = ↑(D n)
F : ℝ → ℝ
hFd : Differentiable ℝ F
hF : f ∘ ofReal' = ofReal' ∘ F
⊢ MonotoneOn (ofReal' ∘ F) (Set.Ici 0)
Theorem: Complex.monotoneOn_of_iteratedDeriv_nonneg
Proof state before:
case intro.intro
f : ℂ → ℂ
hf : Differentiable ℂ f
h : ∀ (n : ℕ), 0 ≤ iteratedDeriv n f 0
D : ℕ → ℝ := fun n => (iteratedDeriv n f 0).re
hD : ∀ (n : ℕ), iteratedDeriv n f 0 = ↑(D n)
F : ℝ → ℝ
hFd : Differentiable ℝ F
hF : f ∘ ofReal' = ofReal' ∘ F
⊢ MonotoneOn (ofReal' ∘ F) (Set.Ici 0)
Tactic:
refine monotone_ofReal.comp_monotoneOn <| monotoneOn_of_deriv_nonneg (convex_Ici 0)
  hFd.continuous.continuousOn hFd.differentiableOn fun x hx ↦ ?_
Proof state after:
case intro.intro
f : ℂ → ℂ
hf : Differentiable ℂ f
h : ∀ (n : ℕ), 0 ≤ iteratedDeriv n f 0
D : ℕ → ℝ := fun n => (iteratedDeriv n f 0).re
hD : ∀ (n : ℕ), iteratedDeriv n f 0 = ↑(D n)
F : ℝ → ℝ
hFd : Differentiable ℝ F
hF : f ∘ ofReal' = ofReal' ∘ F
x : ℝ
hx : x ∈ interior (Set.Ici 0)
⊢ 0 ≤ deriv F x
Theorem: Complex.monotoneOn_of_iteratedDeriv_nonneg
Proof state before:
case intro.intro
f : ℂ → ℂ
hf : Differentiable ℂ f
h : ∀ (n : ℕ), 0 ≤ iteratedDeriv n f 0
D : ℕ → ℝ := fun n => (iteratedDeriv n f 0).re
hD : ∀ (n : ℕ), iteratedDeriv n f 0 = ↑(D n)
F : ℝ → ℝ
hFd : Differentiable ℝ F
hF : f ∘ ofReal' = ofReal' ∘ F
x : ℝ
hx : x ∈ interior (Set.Ici 0)
⊢ 0 ≤ deriv F x
Tactic:
have hD' (n : ℕ) : 0 ≤ iteratedDeriv n (deriv f) 0 := by
  rw [← iteratedDeriv_succ']
  exact h (n + 1)
Proof state after:
case intro.intro
f : ℂ → ℂ
hf : Differentiable ℂ f
h : ∀ (n : ℕ), 0 ≤ iteratedDeriv n f 0
D : ℕ → ℝ := fun n => (iteratedDeriv n f 0).re
hD : ∀ (n : ℕ), iteratedDeriv n f 0 = ↑(D n)
F : ℝ → ℝ
hFd : Differentiable ℝ F
hF : f ∘ ofReal' = ofReal' ∘ F
x : ℝ
hx : x ∈ interior (Set.Ici 0)
hD' : ∀ (n : ℕ), 0 ≤ iteratedDeriv n (deriv f) 0
⊢ 0 ≤ deriv F x
Theorem: Complex.monotoneOn_of_iteratedDeriv_nonneg
Proof state before:
case intro.intro
f : ℂ → ℂ
hf : Differentiable ℂ f
h : ∀ (n : ℕ), 0 ≤ iteratedDeriv n f 0
D : ℕ → ℝ := fun n => (iteratedDeriv n f 0).re
hD : ∀ (n : ℕ), iteratedDeriv n f 0 = ↑(D n)
F : ℝ → ℝ
hFd : Differentiable ℝ F
hF : f ∘ ofReal' = ofReal' ∘ F
x : ℝ
hx : x ∈ interior (Set.Ici 0)
hD' : ∀ (n : ℕ), 0 ≤ iteratedDeriv n (deriv f) 0
⊢ 0 ≤ deriv F x
Tactic:
have hf' := (contDiff_succ_iff_deriv.mp <| hf.contDiff (n := 2)).2.differentiable rfl.le
Proof state after:
case intro.intro
f : ℂ → ℂ
hf : Differentiable ℂ f
h : ∀ (n : ℕ), 0 ≤ iteratedDeriv n f 0
D : ℕ → ℝ := fun n => (iteratedDeriv n f 0).re
hD : ∀ (n : ℕ), iteratedDeriv n f 0 = ↑(D n)
F : ℝ → ℝ
hFd : Differentiable ℝ F
hF : f ∘ ofReal' = ofReal' ∘ F
x : ℝ
hx : x ∈ interior (Set.Ici 0)
hD' : ∀ (n : ℕ), 0 ≤ iteratedDeriv n (deriv f) 0
hf' : Differentiable ℂ (deriv f)
⊢ 0 ≤ deriv F x
Theorem: Complex.monotoneOn_of_iteratedDeriv_nonneg
Proof state before:
case intro.intro
f : ℂ → ℂ
hf : Differentiable ℂ f
h : ∀ (n : ℕ), 0 ≤ iteratedDeriv n f 0
D : ℕ → ℝ := fun n => (iteratedDeriv n f 0).re
hD : ∀ (n : ℕ), iteratedDeriv n f 0 = ↑(D n)
F : ℝ → ℝ
hFd : Differentiable ℝ F
hF : f ∘ ofReal' = ofReal' ∘ F
x : ℝ
hx : x ∈ interior (Set.Ici 0)
hD' : ∀ (n : ℕ), 0 ≤ iteratedDeriv n (deriv f) 0
hf' : Differentiable ℂ (deriv f)
⊢ 0 ≤ deriv F x
Tactic:
have hx : (0 : ℂ) ≤ x := by
  norm_cast
  simp only [Set.nonempty_Iio, interior_Ici', Set.mem_Ioi] at hx
  exact hx.le
Proof state after:
case intro.intro
f : ℂ → ℂ
hf : Differentiable ℂ f
h : ∀ (n : ℕ), 0 ≤ iteratedDeriv n f 0
D : ℕ → ℝ := fun n => (iteratedDeriv n f 0).re
hD : ∀ (n : ℕ), iteratedDeriv n f 0 = ↑(D n)
F : ℝ → ℝ
hFd : Differentiable ℝ F
hF : f ∘ ofReal' = ofReal' ∘ F
x : ℝ
hx✝ : x ∈ interior (Set.Ici 0)
hD' : ∀ (n : ℕ), 0 ≤ iteratedDeriv n (deriv f) 0
hf' : Differentiable ℂ (deriv f)
hx : 0 ≤ ↑x
⊢ 0 ≤ deriv F x
Theorem: Complex.monotoneOn_of_iteratedDeriv_nonneg
Proof state before:
case intro.intro
f : ℂ → ℂ
hf : Differentiable ℂ f
h : ∀ (n : ℕ), 0 ≤ iteratedDeriv n f 0
D : ℕ → ℝ := fun n => (iteratedDeriv n f 0).re
hD : ∀ (n : ℕ), iteratedDeriv n f 0 = ↑(D n)
F : ℝ → ℝ
hFd : Differentiable ℝ F
hF : f ∘ ofReal' = ofReal' ∘ F
x : ℝ
hx✝ : x ∈ interior (Set.Ici 0)
hD' : ∀ (n : ℕ), 0 ≤ iteratedDeriv n (deriv f) 0
hf' : Differentiable ℂ (deriv f)
hx : 0 ≤ ↑x
⊢ 0 ≤ deriv F x
Tactic:
have H := nonneg_of_iteratedDeriv_nonneg hf' hD' hx
Proof state after:
case intro.intro
f : ℂ → ℂ
hf : Differentiable ℂ f
h : ∀ (n : ℕ), 0 ≤ iteratedDeriv n f 0
D : ℕ → ℝ := fun n => (iteratedDeriv n f 0).re
hD : ∀ (n : ℕ), iteratedDeriv n f 0 = ↑(D n)
F : ℝ → ℝ
hFd : Differentiable ℝ F
hF : f ∘ ofReal' = ofReal' ∘ F
x : ℝ
hx✝ : x ∈ interior (Set.Ici 0)
hD' : ∀ (n : ℕ), 0 ≤ iteratedDeriv n (deriv f) 0
hf' : Differentiable ℂ (deriv f)
hx : 0 ≤ ↑x
H : 0 ≤ deriv f ↑x
⊢ 0 ≤ deriv F x
Theorem: Complex.monotoneOn_of_iteratedDeriv_nonneg
Proof state before:
case intro.intro
f : ℂ → ℂ
hf : Differentiable ℂ f
h : ∀ (n : ℕ), 0 ≤ iteratedDeriv n f 0
D : ℕ → ℝ := fun n => (iteratedDeriv n f 0).re
hD : ∀ (n : ℕ), iteratedDeriv n f 0 = ↑(D n)
F : ℝ → ℝ
hFd : Differentiable ℝ F
hF : f ∘ ofReal' = ofReal' ∘ F
x : ℝ
hx✝ : x ∈ interior (Set.Ici 0)
hD' : ∀ (n : ℕ), 0 ≤ iteratedDeriv n (deriv f) 0
hf' : Differentiable ℂ (deriv f)
hx : 0 ≤ ↑x
H : 0 ≤ deriv f ↑x
⊢ 0 ≤ deriv F x
Tactic:
rw [← deriv.comp_ofReal hf.differentiableAt] at H
Proof state after:
case intro.intro
f : ℂ → ℂ
hf : Differentiable ℂ f
h : ∀ (n : ℕ), 0 ≤ iteratedDeriv n f 0
D : ℕ → ℝ := fun n => (iteratedDeriv n f 0).re
hD : ∀ (n : ℕ), iteratedDeriv n f 0 = ↑(D n)
F : ℝ → ℝ
hFd : Differentiable ℝ F
hF : f ∘ ofReal' = ofReal' ∘ F
x : ℝ
hx✝ : x ∈ interior (Set.Ici 0)
hD' : ∀ (n : ℕ), 0 ≤ iteratedDeriv n (deriv f) 0
hf' : Differentiable ℂ (deriv f)
hx : 0 ≤ ↑x
H : 0 ≤ deriv (fun x => f ↑x) x
⊢ 0 ≤ deriv F x
Theorem: Complex.monotoneOn_of_iteratedDeriv_nonneg
Proof state before:
case intro.intro
f : ℂ → ℂ
hf : Differentiable ℂ f
h : ∀ (n : ℕ), 0 ≤ iteratedDeriv n f 0
D : ℕ → ℝ := fun n => (iteratedDeriv n f 0).re
hD : ∀ (n : ℕ), iteratedDeriv n f 0 = ↑(D n)
F : ℝ → ℝ
hFd : Differentiable ℝ F
hF : f ∘ ofReal' = ofReal' ∘ F
x : ℝ
hx✝ : x ∈ interior (Set.Ici 0)
hD' : ∀ (n : ℕ), 0 ≤ iteratedDeriv n (deriv f) 0
hf' : Differentiable ℂ (deriv f)
hx : 0 ≤ ↑x
H : 0 ≤ deriv (fun x => f ↑x) x
⊢ 0 ≤ deriv F x
Tactic:
change 0 ≤ deriv (f ∘ ofReal') x at H
Proof state after:
case intro.intro
f : ℂ → ℂ
hf : Differentiable ℂ f
h : ∀ (n : ℕ), 0 ≤ iteratedDeriv n f 0
D : ℕ → ℝ := fun n => (iteratedDeriv n f 0).re
hD : ∀ (n : ℕ), iteratedDeriv n f 0 = ↑(D n)
F : ℝ → ℝ
hFd : Differentiable ℝ F
hF : f ∘ ofReal' = ofReal' ∘ F
x : ℝ
hx✝ : x ∈ interior (Set.Ici 0)
hD' : ∀ (n : ℕ), 0 ≤ iteratedDeriv n (deriv f) 0
hf' : Differentiable ℂ (deriv f)
hx : 0 ≤ ↑x
H : 0 ≤ deriv (f ∘ ofReal') x
⊢ 0 ≤ deriv F x
Theorem: Complex.monotoneOn_of_iteratedDeriv_nonneg
Proof state before:
case intro.intro
f : ℂ → ℂ
hf : Differentiable ℂ f
h : ∀ (n : ℕ), 0 ≤ iteratedDeriv n f 0
D : ℕ → ℝ := fun n => (iteratedDeriv n f 0).re
hD : ∀ (n : ℕ), iteratedDeriv n f 0 = ↑(D n)
F : ℝ → ℝ
hFd : Differentiable ℝ F
hF : f ∘ ofReal' = ofReal' ∘ F
x : ℝ
hx✝ : x ∈ interior (Set.Ici 0)
hD' : ∀ (n : ℕ), 0 ≤ iteratedDeriv n (deriv f) 0
hf' : Differentiable ℂ (deriv f)
hx : 0 ≤ ↑x
H : 0 ≤ deriv (f ∘ ofReal') x
⊢ 0 ≤ deriv F x
Tactic:
erw [hF, deriv.ofReal_comp] at H
Proof state after:
case intro.intro
f : ℂ → ℂ
hf : Differentiable ℂ f
h : ∀ (n : ℕ), 0 ≤ iteratedDeriv n f 0
D : ℕ → ℝ := fun n => (iteratedDeriv n f 0).re
hD : ∀ (n : ℕ), iteratedDeriv n f 0 = ↑(D n)
F : ℝ → ℝ
hFd : Differentiable ℝ F
hF : f ∘ ofReal' = ofReal' ∘ F
x : ℝ
hx✝ : x ∈ interior (Set.Ici 0)
hD' : ∀ (n : ℕ), 0 ≤ iteratedDeriv n (deriv f) 0
hf' : Differentiable ℂ (deriv f)
hx : 0 ≤ ↑x
H : 0 ≤ ↑(deriv (fun y => F y) x)
⊢ 0 ≤ deriv F x
Theorem: Complex.monotoneOn_of_iteratedDeriv_nonneg
Proof state before:
case intro.intro
f : ℂ → ℂ
hf : Differentiable ℂ f
h : ∀ (n : ℕ), 0 ≤ iteratedDeriv n f 0
D : ℕ → ℝ := fun n => (iteratedDeriv n f 0).re
hD : ∀ (n : ℕ), iteratedDeriv n f 0 = ↑(D n)
F : ℝ → ℝ
hFd : Differentiable ℝ F
hF : f ∘ ofReal' = ofReal' ∘ F
x : ℝ
hx✝ : x ∈ interior (Set.Ici 0)
hD' : ∀ (n : ℕ), 0 ≤ iteratedDeriv n (deriv f) 0
hf' : Differentiable ℂ (deriv f)
hx : 0 ≤ ↑x
H : 0 ≤ ↑(deriv (fun y => F y) x)
⊢ 0 ≤ deriv F x
Tactic:
norm_cast at H
Proof state after:
no goals
Theorem: Complex.monotoneOn_of_iteratedDeriv_nonneg
Proof state before:
f : ℂ → ℂ
hf : Differentiable ℂ f
h : ∀ (n : ℕ), 0 ≤ iteratedDeriv n f 0
D : ℕ → ℝ := fun n => (iteratedDeriv n f 0).re
n : ℕ
⊢ iteratedDeriv n f 0 = ↑(D n)
Tactic:
refine Complex.ext rfl ?_
Proof state after:
f : ℂ → ℂ
hf : Differentiable ℂ f
h : ∀ (n : ℕ), 0 ≤ iteratedDeriv n f 0
D : ℕ → ℝ := fun n => (iteratedDeriv n f 0).re
n : ℕ
⊢ (iteratedDeriv n f 0).im = (↑(D n)).im
Theorem: Complex.monotoneOn_of_iteratedDeriv_nonneg
Proof state before:
f : ℂ → ℂ
hf : Differentiable ℂ f
h : ∀ (n : ℕ), 0 ≤ iteratedDeriv n f 0
D : ℕ → ℝ := fun n => (iteratedDeriv n f 0).re
n : ℕ
⊢ (iteratedDeriv n f 0).im = (↑(D n)).im
Tactic:
simp only [ofReal_im]
Proof state after:
f : ℂ → ℂ
hf : Differentiable ℂ f
h : ∀ (n : ℕ), 0 ≤ iteratedDeriv n f 0
D : ℕ → ℝ := fun n => (iteratedDeriv n f 0).re
n : ℕ
⊢ (iteratedDeriv n f 0).im = 0
Theorem: Complex.monotoneOn_of_iteratedDeriv_nonneg
Proof state before:
f : ℂ → ℂ
hf : Differentiable ℂ f
h : ∀ (n : ℕ), 0 ≤ iteratedDeriv n f 0
D : ℕ → ℝ := fun n => (iteratedDeriv n f 0).re
n : ℕ
⊢ (iteratedDeriv n f 0).im = 0
Tactic:
exact (le_def.mp (h n)).2.symm
Proof state after:
no goals
Theorem: Complex.monotoneOn_of_iteratedDeriv_nonneg
Proof state before:
f : ℂ → ℂ
hf : Differentiable ℂ f
h : ∀ (n : ℕ), 0 ≤ iteratedDeriv n f 0
D : ℕ → ℝ := fun n => (iteratedDeriv n f 0).re
hD : ∀ (n : ℕ), iteratedDeriv n f 0 = ↑(D n)
F : ℝ → ℝ
hFd : Differentiable ℝ F
hF : f ∘ ofReal' = ofReal' ∘ F
x : ℝ
hx : x ∈ interior (Set.Ici 0)
n : ℕ
⊢ 0 ≤ iteratedDeriv n (deriv f) 0
Tactic:
rw [← iteratedDeriv_succ']
Proof state after:
f : ℂ → ℂ
hf : Differentiable ℂ f
h : ∀ (n : ℕ), 0 ≤ iteratedDeriv n f 0
D : ℕ → ℝ := fun n => (iteratedDeriv n f 0).re
hD : ∀ (n : ℕ), iteratedDeriv n f 0 = ↑(D n)
F : ℝ → ℝ
hFd : Differentiable ℝ F
hF : f ∘ ofReal' = ofReal' ∘ F
x : ℝ
hx : x ∈ interior (Set.Ici 0)
n : ℕ
⊢ 0 ≤ iteratedDeriv (n + 1) f 0
Theorem: Complex.monotoneOn_of_iteratedDeriv_nonneg
Proof state before:
f : ℂ → ℂ
hf : Differentiable ℂ f
h : ∀ (n : ℕ), 0 ≤ iteratedDeriv n f 0
D : ℕ → ℝ := fun n => (iteratedDeriv n f 0).re
hD : ∀ (n : ℕ), iteratedDeriv n f 0 = ↑(D n)
F : ℝ → ℝ
hFd : Differentiable ℝ F
hF : f ∘ ofReal' = ofReal' ∘ F
x : ℝ
hx : x ∈ interior (Set.Ici 0)
n : ℕ
⊢ 0 ≤ iteratedDeriv (n + 1) f 0
Tactic:
exact h (n + 1)
Proof state after:
no goals
Theorem: Complex.monotoneOn_of_iteratedDeriv_nonneg
Proof state before:
f : ℂ → ℂ
hf : Differentiable ℂ f
h : ∀ (n : ℕ), 0 ≤ iteratedDeriv n f 0
D : ℕ → ℝ := fun n => (iteratedDeriv n f 0).re
hD : ∀ (n : ℕ), iteratedDeriv n f 0 = ↑(D n)
F : ℝ → ℝ
hFd : Differentiable ℝ F
hF : f ∘ ofReal' = ofReal' ∘ F
x : ℝ
hx : x ∈ interior (Set.Ici 0)
hD' : ∀ (n : ℕ), 0 ≤ iteratedDeriv n (deriv f) 0
hf' : Differentiable ℂ (deriv f)
⊢ 0 ≤ ↑x
Tactic:
norm_cast
Proof state after:
f : ℂ → ℂ
hf : Differentiable ℂ f
h : ∀ (n : ℕ), 0 ≤ iteratedDeriv n f 0
D : ℕ → ℝ := fun n => (iteratedDeriv n f 0).re
hD : ∀ (n : ℕ), iteratedDeriv n f 0 = ↑(D n)
F : ℝ → ℝ
hFd : Differentiable ℝ F
hF : f ∘ ofReal' = ofReal' ∘ F
x : ℝ
hx : x ∈ interior (Set.Ici 0)
hD' : ∀ (n : ℕ), 0 ≤ iteratedDeriv n (deriv f) 0
hf' : Differentiable ℂ (deriv f)
⊢ 0 ≤ x
Theorem: Complex.monotoneOn_of_iteratedDeriv_nonneg
Proof state before:
f : ℂ → ℂ
hf : Differentiable ℂ f
h : ∀ (n : ℕ), 0 ≤ iteratedDeriv n f 0
D : ℕ → ℝ := fun n => (iteratedDeriv n f 0).re
hD : ∀ (n : ℕ), iteratedDeriv n f 0 = ↑(D n)
F : ℝ → ℝ
hFd : Differentiable ℝ F
hF : f ∘ ofReal' = ofReal' ∘ F
x : ℝ
hx : x ∈ interior (Set.Ici 0)
hD' : ∀ (n : ℕ), 0 ≤ iteratedDeriv n (deriv f) 0
hf' : Differentiable ℂ (deriv f)
⊢ 0 ≤ x
Tactic:
simp only [Set.nonempty_Iio, interior_Ici', Set.mem_Ioi] at hx
Proof state after:
f : ℂ → ℂ
hf : Differentiable ℂ f
h : ∀ (n : ℕ), 0 ≤ iteratedDeriv n f 0
D : ℕ → ℝ := fun n => (iteratedDeriv n f 0).re
hD : ∀ (n : ℕ), iteratedDeriv n f 0 = ↑(D n)
F : ℝ → ℝ
hFd : Differentiable ℝ F
hF : f ∘ ofReal' = ofReal' ∘ F
x : ℝ
hD' : ∀ (n : ℕ), 0 ≤ iteratedDeriv n (deriv f) 0
hf' : Differentiable ℂ (deriv f)
hx : 0 < x
⊢ 0 ≤ x
Theorem: Complex.monotoneOn_of_iteratedDeriv_nonneg
Proof state before:
f : ℂ → ℂ
hf : Differentiable ℂ f
h : ∀ (n : ℕ), 0 ≤ iteratedDeriv n f 0
D : ℕ → ℝ := fun n => (iteratedDeriv n f 0).re
hD : ∀ (n : ℕ), iteratedDeriv n f 0 = ↑(D n)
F : ℝ → ℝ
hFd : Differentiable ℝ F
hF : f ∘ ofReal' = ofReal' ∘ F
x : ℝ
hD' : ∀ (n : ℕ), 0 ≤ iteratedDeriv n (deriv f) 0
hf' : Differentiable ℂ (deriv f)
hx : 0 < x
⊢ 0 ≤ x
Tactic:
exact hx.le
Proof state after:
no goals
Theorem: Complex.at_zero_le_of_iteratedDeriv_nonneg
Proof state before:
f : ℂ → ℂ
hf : Differentiable ℂ f
h : ∀ (n : ℕ), n ≠ 0 → 0 ≤ iteratedDeriv n f 0
z : ℂ
hz : 0 ≤ z
h' : ∀ (n : ℕ), 0 ≤ iteratedDeriv n (fun x => f x - f 0) 0
⊢ f 0 ≤ f z
Tactic:
exact sub_nonneg.mp <| nonneg_of_iteratedDeriv_nonneg (hf.sub_const (f 0)) h' hz
Proof state after:
no goals
Theorem: Complex.at_zero_le_of_iteratedDeriv_nonneg
Proof state before:
f : ℂ → ℂ
hf : Differentiable ℂ f
h : ∀ (n : ℕ), n ≠ 0 → 0 ≤ iteratedDeriv n f 0
z : ℂ
hz : 0 ≤ z
n : ℕ
⊢ 0 ≤ iteratedDeriv n (fun x => f x - f 0) 0
Tactic:
cases n with
| zero => simp only [iteratedDeriv_zero, sub_self, le_refl]
| succ n =>
  specialize h n.succ <| succ_ne_zero n
  rw [iteratedDeriv_succ'] at h ⊢
  convert h using 2
  ext w
  exact deriv_sub_const (f 0)
Proof state after:
no goals
Theorem: Complex.at_zero_le_of_iteratedDeriv_nonneg
Proof state before:
case zero
f : ℂ → ℂ
hf : Differentiable ℂ f
h : ∀ (n : ℕ), n ≠ 0 → 0 ≤ iteratedDeriv n f 0
z : ℂ
hz : 0 ≤ z
⊢ 0 ≤ iteratedDeriv 0 (fun x => f x - f 0) 0
Tactic:
simp only [iteratedDeriv_zero, sub_self, le_refl]
Proof state after:
no goals
Theorem: Complex.at_zero_le_of_iteratedDeriv_nonneg
Proof state before:
case succ
f : ℂ → ℂ
hf : Differentiable ℂ f
h : ∀ (n : ℕ), n ≠ 0 → 0 ≤ iteratedDeriv n f 0
z : ℂ
hz : 0 ≤ z
n : ℕ
⊢ 0 ≤ iteratedDeriv (n + 1) (fun x => f x - f 0) 0
Tactic:
specialize h n.succ <| succ_ne_zero n
Proof state after:
case succ
f : ℂ → ℂ
hf : Differentiable ℂ f
z : ℂ
hz : 0 ≤ z
n : ℕ
h : 0 ≤ iteratedDeriv n.succ f 0
⊢ 0 ≤ iteratedDeriv (n + 1) (fun x => f x - f 0) 0
Theorem: Complex.at_zero_le_of_iteratedDeriv_nonneg
Proof state before:
case succ
f : ℂ → ℂ
hf : Differentiable ℂ f
z : ℂ
hz : 0 ≤ z
n : ℕ
h : 0 ≤ iteratedDeriv n.succ f 0
⊢ 0 ≤ iteratedDeriv (n + 1) (fun x => f x - f 0) 0
Tactic:
rw [iteratedDeriv_succ'] at h ⊢
Proof state after:
case succ
f : ℂ → ℂ
hf : Differentiable ℂ f
z : ℂ
hz : 0 ≤ z
n : ℕ
h : 0 ≤ iteratedDeriv n (deriv f) 0
⊢ 0 ≤ iteratedDeriv n (deriv fun x => f x - f 0) 0
Theorem: Complex.at_zero_le_of_iteratedDeriv_nonneg
Proof state before:
case succ
f : ℂ → ℂ
hf : Differentiable ℂ f
z : ℂ
hz : 0 ≤ z
n : ℕ
h : 0 ≤ iteratedDeriv n (deriv f) 0
⊢ 0 ≤ iteratedDeriv n (deriv fun x => f x - f 0) 0
Tactic:
convert h using 2
Proof state after:
case h.e'_4.h.e'_7
f : ℂ → ℂ
hf : Differentiable ℂ f
z : ℂ
hz : 0 ≤ z
n : ℕ
h : 0 ≤ iteratedDeriv n (deriv f) 0
⊢ (deriv fun x => f x - f 0) = deriv f
Theorem: Complex.at_zero_le_of_iteratedDeriv_nonneg
Proof state before:
case h.e'_4.h.e'_7
f : ℂ → ℂ
hf : Differentiable ℂ f
z : ℂ
hz : 0 ≤ z
n : ℕ
h : 0 ≤ iteratedDeriv n (deriv f) 0
⊢ (deriv fun x => f x - f 0) = deriv f
Tactic:
ext w
Proof state after:
case h.e'_4.h.e'_7.h
f : ℂ → ℂ
hf : Differentiable ℂ f
z : ℂ
hz : 0 ≤ z
n : ℕ
h : 0 ≤ iteratedDeriv n (deriv f) 0
w : ℂ
⊢ deriv (fun x => f x - f 0) w = deriv f w
Theorem: Complex.at_zero_le_of_iteratedDeriv_nonneg
Proof state before:
case h.e'_4.h.e'_7.h
f : ℂ → ℂ
hf : Differentiable ℂ f
z : ℂ
hz : 0 ≤ z
n : ℕ
h : 0 ≤ iteratedDeriv n (deriv f) 0
w : ℂ
⊢ deriv (fun x => f x - f 0) w = deriv f w
Tactic:
exact deriv_sub_const (f 0)
Proof state after:
no goals
Theorem: Complex.at_zero_le_of_iteratedDeriv_alternating
Proof state before:
f : ℂ → ℂ
hf : Differentiable ℂ f
h : ∀ (n : ℕ), n ≠ 0 → 0 ≤ (-1) ^ n * iteratedDeriv n f 0
z : ℂ
hz : z ≤ 0
⊢ f 0 ≤ f z
Tactic:
let F : ℂ → ℂ := fun z ↦ f (-z)
Proof state after:
f : ℂ → ℂ
hf : Differentiable ℂ f
h : ∀ (n : ℕ), n ≠ 0 → 0 ≤ (-1) ^ n * iteratedDeriv n f 0
z : ℂ
hz : z ≤ 0
F : ℂ → ℂ := fun z => f (-z)
⊢ f 0 ≤ f z
Theorem: Complex.at_zero_le_of_iteratedDeriv_alternating
Proof state before:
f : ℂ → ℂ
hf : Differentiable ℂ f
h : ∀ (n : ℕ), n ≠ 0 → 0 ≤ (-1) ^ n * iteratedDeriv n f 0
z : ℂ
hz : z ≤ 0
F : ℂ → ℂ := fun z => f (-z)
⊢ f 0 ≤ f z
Tactic:
convert at_zero_le_of_iteratedDeriv_nonneg (f := F) (hf.comp <| differentiable_neg)
  (fun n hn ↦ ?_) (neg_nonneg.mpr hz) using 1
Proof state after:
case h.e'_3
f : ℂ → ℂ
hf : Differentiable ℂ f
h : ∀ (n : ℕ), n ≠ 0 → 0 ≤ (-1) ^ n * iteratedDeriv n f 0
z : ℂ
hz : z ≤ 0
F : ℂ → ℂ := fun z => f (-z)
⊢ f 0 = F 0

case h.e'_4
f : ℂ → ℂ
hf : Differentiable ℂ f
h : ∀ (n : ℕ), n ≠ 0 → 0 ≤ (-1) ^ n * iteratedDeriv n f 0
z : ℂ
hz : z ≤ 0
F : ℂ → ℂ := fun z => f (-z)
⊢ f z = F (-z)

f : ℂ → ℂ
hf : Differentiable ℂ f
h : ∀ (n : ℕ), n ≠ 0 → 0 ≤ (-1) ^ n * iteratedDeriv n f 0
z : ℂ
hz : z ≤ 0
F : ℂ → ℂ := fun z => f (-z)
n : ℕ
hn : n ≠ 0
⊢ 0 ≤ iteratedDeriv n F 0
Theorem: Complex.at_zero_le_of_iteratedDeriv_alternating
Proof state before:
case h.e'_3
f : ℂ → ℂ
hf : Differentiable ℂ f
h : ∀ (n : ℕ), n ≠ 0 → 0 ≤ (-1) ^ n * iteratedDeriv n f 0
z : ℂ
hz : z ≤ 0
F : ℂ → ℂ := fun z => f (-z)
⊢ f 0 = F 0
Tactic:
simp only [F, neg_zero]
Proof state after:
no goals
Theorem: Complex.at_zero_le_of_iteratedDeriv_alternating
Proof state before:
case h.e'_4
f : ℂ → ℂ
hf : Differentiable ℂ f
h : ∀ (n : ℕ), n ≠ 0 → 0 ≤ (-1) ^ n * iteratedDeriv n f 0
z : ℂ
hz : z ≤ 0
F : ℂ → ℂ := fun z => f (-z)
⊢ f z = F (-z)
Tactic:
simp only [F, neg_neg]
Proof state after:
no goals
Theorem: Complex.at_zero_le_of_iteratedDeriv_alternating
Proof state before:
f : ℂ → ℂ
hf : Differentiable ℂ f
h : ∀ (n : ℕ), n ≠ 0 → 0 ≤ (-1) ^ n * iteratedDeriv n f 0
z : ℂ
hz : z ≤ 0
F : ℂ → ℂ := fun z => f (-z)
n : ℕ
hn : n ≠ 0
⊢ 0 ≤ iteratedDeriv n F 0
Tactic:
simpa only [F, iteratedDeriv_comp_neg, neg_zero] using h n hn
Proof state after:
no goals
Theorem: LSeries.term_mul_aux
Proof state before:
a b : ℂ
m n : ℕ
s : ℂ
⊢ a / ↑m ^ s * (b / ↑n ^ s) = a * b / (↑m * ↑n) ^ s
Tactic:
rw [mul_comm_div, div_div, ← mul_div_assoc, mul_comm (m : ℂ), natCast_mul_natCast_cpow]
Proof state after:
no goals
Theorem: LSeries.term_mul
Proof state before:
f₁ f₂ f : ℕ → ℂ
m n : ℕ
h : f (m * n) = f₁ m * f₂ n
s : ℂ
⊢ term f s (m * n) = term f₁ s m * term f₂ s n
Tactic:
rcases eq_or_ne (m * n) 0 with H | H
Proof state after:
case inl
f₁ f₂ f : ℕ → ℂ
m n : ℕ
h : f (m * n) = f₁ m * f₂ n
s : ℂ
H : m * n = 0
⊢ term f s (m * n) = term f₁ s m * term f₂ s n

case inr
f₁ f₂ f : ℕ → ℂ
m n : ℕ
h : f (m * n) = f₁ m * f₂ n
s : ℂ
H : m * n ≠ 0
⊢ term f s (m * n) = term f₁ s m * term f₂ s n
Theorem: LSeries.term_mul
Proof state before:
case inl
f₁ f₂ f : ℕ → ℂ
m n : ℕ
h : f (m * n) = f₁ m * f₂ n
s : ℂ
H : m * n = 0
⊢ term f s (m * n) = term f₁ s m * term f₂ s n
Tactic:
rcases mul_eq_zero.mp H with rfl | rfl <;> simp only [term_zero, mul_zero, zero_mul]
Proof state after:
no goals
Theorem: LSeries.term_mul
Proof state before:
case inr
f₁ f₂ f : ℕ → ℂ
m n : ℕ
h : f (m * n) = f₁ m * f₂ n
s : ℂ
H : m * n ≠ 0
⊢ term f s (m * n) = term f₁ s m * term f₂ s n
Tactic:
obtain ⟨hm, hn⟩ := mul_ne_zero_iff.mp H
Proof state after:
case inr.intro
f₁ f₂ f : ℕ → ℂ
m n : ℕ
h : f (m * n) = f₁ m * f₂ n
s : ℂ
H : m * n ≠ 0
hm : m ≠ 0
hn : n ≠ 0
⊢ term f s (m * n) = term f₁ s m * term f₂ s n
Theorem: LSeries.term_mul
Proof state before:
case inr.intro
f₁ f₂ f : ℕ → ℂ
m n : ℕ
h : f (m * n) = f₁ m * f₂ n
s : ℂ
H : m * n ≠ 0
hm : m ≠ 0
hn : n ≠ 0
⊢ term f s (m * n) = term f₁ s m * term f₂ s n
Tactic:
simp only [ne_eq, H, not_false_eq_true, term_of_ne_zero, Nat.cast_mul, hm, hn, h, term_mul_aux]
Proof state after:
no goals
Theorem: LSeries.term_at_one
Proof state before:
f : ℕ → ℂ
h₁ : f 1 = 1
s : ℂ
⊢ term f s 1 = 1
Tactic:
rw [term_of_ne_zero one_ne_zero, h₁, Nat.cast_one, one_cpow, div_one]
Proof state after:
no goals
Theorem: DirichletCharacter.toFun_on_nat_map_one
Proof state before:
N : ℕ
χ : DirichletCharacter ℂ N
⊢ (fun n => χ ↑n) 1 = 1
Tactic:
simp only [cast_one, map_one]
Proof state after:
no goals
Theorem: DirichletCharacter.toFun_on_nat_map_mul
Proof state before:
N : ℕ
χ : DirichletCharacter ℂ N
m n : ℕ
⊢ (fun n => χ ↑n) (m * n) = (fun n => χ ↑n) m * (fun n => χ ↑n) n
Tactic:
simp only [cast_mul, map_mul]
Proof state after:
no goals
Theorem: DirichletCharacter.LSeries_eulerProduct
Proof state before:
N : ℕ
χ : DirichletCharacter ℂ N
s : ℂ
hs : 1 < s.re
⊢ Tendsto (fun n => ∏ p ∈ n.primesBelow, (1 - χ ↑p * ↑p ^ (-s))⁻¹) atTop (𝓝 (L (fun n => χ ↑n) s))
Tactic:
refine Tendsto.congr (fun n ↦ Finset.prod_congr rfl fun p hp ↦ ?_) <|
  eulerProduct_of_completelyMultiplicative (toFun_on_nat_map_one χ) (toFun_on_nat_map_mul χ) <|
  LSeriesSummable_of_one_lt_re χ hs
Proof state after:
N : ℕ
χ : DirichletCharacter ℂ N
s : ℂ
hs : 1 < s.re
n p : ℕ
hp : p ∈ n.primesBelow
⊢ (1 - term (fun n => χ ↑n) s p)⁻¹ = (1 - χ ↑p * ↑p ^ (-s))⁻¹
Theorem: DirichletCharacter.LSeries_eulerProduct
Proof state before:
N : ℕ
χ : DirichletCharacter ℂ N
s : ℂ
hs : 1 < s.re
n p : ℕ
hp : p ∈ n.primesBelow
⊢ (1 - term (fun n => χ ↑n) s p)⁻¹ = (1 - χ ↑p * ↑p ^ (-s))⁻¹
Tactic:
rw [term_of_ne_zero (prime_of_mem_primesBelow hp).ne_zero, cpow_neg, div_eq_mul_inv]
Proof state after:
no goals
Theorem: DirichletCharacter.LSeries_eulerProduct'
Proof state before:
N : ℕ
χ : DirichletCharacter ℂ N
s : ℂ
hs : 1 < s.re
⊢ cexp (∑' (p : Primes), -(1 - χ ↑↑p * ↑↑p ^ (-s)).log) = L (fun n => χ ↑n) s
Tactic:
rw [LSeries]
Proof state after:
N : ℕ
χ : DirichletCharacter ℂ N
s : ℂ
hs : 1 < s.re
⊢ cexp (∑' (p : Primes), -(1 - χ ↑↑p * ↑↑p ^ (-s)).log) = ∑' (n : ℕ), term (fun n => χ ↑n) s n
Theorem: DirichletCharacter.LSeries_eulerProduct'
Proof state before:
N : ℕ
χ : DirichletCharacter ℂ N
s : ℂ
hs : 1 < s.re
⊢ cexp (∑' (p : Primes), -(1 - χ ↑↑p * ↑↑p ^ (-s)).log) = ∑' (n : ℕ), term (fun n => χ ↑n) s n
Tactic:
convert exp_sum_primes_log_eq_tsum (f := dirichletSummandHom χ <| ne_zero_of_one_lt_re hs) <|
  summable_dirichletSummand χ hs
Proof state after:
case h.e'_3.h.e'_5.h.h.e
N : ℕ
χ : DirichletCharacter ℂ N
s : ℂ
hs : 1 < s.re
x✝ : ℕ
⊢ term (fun n => χ ↑n) s = ⇑(dirichletSummandHom χ ⋯)
Theorem: DirichletCharacter.LSeries_eulerProduct'
Proof state before:
case h.e'_3.h.e'_5.h.h.e
N : ℕ
χ : DirichletCharacter ℂ N
s : ℂ
hs : 1 < s.re
x✝ : ℕ
⊢ term (fun n => χ ↑n) s = ⇑(dirichletSummandHom χ ⋯)
Tactic:
ext n
Proof state after:
case h.e'_3.h.e'_5.h.h.e.h
N : ℕ
χ : DirichletCharacter ℂ N
s : ℂ
hs : 1 < s.re
x✝ n : ℕ
⊢ term (fun n => χ ↑n) s n = (dirichletSummandHom χ ⋯) n