internlm/Lean-Github huggingface dataset:
Theorem: product_drop'
Proof state before:
case intro
f : ℕ → ℂ
f0 : f 0 ≠ 0
g : ℂ
h : HasProd f g
⊢ ∏' (n : ℕ), f (n + 1) = tprod f / f 0
Tactic:
rw [HasProd.tprod_eq h]
Proof state after:
case intro
f : ℕ → ℂ
f0 : f 0 ≠ 0
g : ℂ
h : HasProd f g
⊢ ∏' (n : ℕ), f (n + 1) = g / f 0
Theorem: product_drop'
Proof state before:
case intro
f : ℕ → ℂ
f0 : f 0 ≠ 0
g : ℂ
h : HasProd f g
⊢ ∏' (n : ℕ), f (n + 1) = g / f 0
Tactic:
rw [HasProd.tprod_eq _]
Proof state after:
f : ℕ → ℂ
f0 : f 0 ≠ 0
g : ℂ
h : HasProd f g
⊢ HasProd (fun n => f (n + 1)) (g / f 0)
Theorem: product_drop'
Proof state before:
f : ℕ → ℂ
f0 : f 0 ≠ 0
g : ℂ
h : HasProd f g
⊢ HasProd (fun n => f (n + 1)) (g / f 0)
Tactic:
exact product_drop f0 h
Proof state after:
no goals
Theorem: product_head_zero
Proof state before:
f : ℕ → ℂ
f0 : f 0 = 0
⊢ HasProd f 0
Tactic:
rw [HasProd]
Proof state after:
f : ℕ → ℂ
f0 : f 0 = 0
⊢ Filter.Tendsto (fun s => s.prod fun b => f b) atTop (𝓝 0)
Theorem: product_head_zero
Proof state before:
f : ℕ → ℂ
f0 : f 0 = 0
⊢ Filter.Tendsto (fun s => s.prod fun b => f b) atTop (𝓝 0)
Tactic:
rw [Metric.tendsto_atTop]
Proof state after:
f : ℕ → ℂ
f0 : f 0 = 0
⊢ ∀ ε > 0, ∃ N, ∀ n ≥ N, dist (n.prod fun b => f b) 0 < ε
Theorem: product_head_zero
Proof state before:
f : ℕ → ℂ
f0 : f 0 = 0
⊢ ∀ ε > 0, ∃ N, ∀ n ≥ N, dist (n.prod fun b => f b) 0 < ε
Tactic:
intro e ep
Proof state after:
f : ℕ → ℂ
f0 : f 0 = 0
e : ℝ
ep : e > 0
⊢ ∃ N, ∀ n ≥ N, dist (n.prod fun b => f b) 0 < e
Theorem: product_head_zero
Proof state before:
f : ℕ → ℂ
f0 : f 0 = 0
e : ℝ
ep : e > 0
⊢ ∃ N, ∀ n ≥ N, dist (n.prod fun b => f b) 0 < e
Tactic:
use Finset.range 1
Proof state after:
case h
f : ℕ → ℂ
f0 : f 0 = 0
e : ℝ
ep : e > 0
⊢ ∀ n ≥ Finset.range 1, dist (n.prod fun b => f b) 0 < e
Theorem: product_head_zero
Proof state before:
case h
f : ℕ → ℂ
f0 : f 0 = 0
e : ℝ
ep : e > 0
⊢ ∀ n ≥ Finset.range 1, dist (n.prod fun b => f b) 0 < e
Tactic:
intro N N1
Proof state after:
case h
f : ℕ → ℂ
f0 : f 0 = 0
e : ℝ
ep : e > 0
N : Finset ℕ
N1 : N ≥ Finset.range 1
⊢ dist (N.prod fun b => f b) 0 < e
Theorem: product_head_zero
Proof state before:
case h
f : ℕ → ℂ
f0 : f 0 = 0
e : ℝ
ep : e > 0
N : Finset ℕ
N1 : N ≥ Finset.range 1
⊢ dist (N.prod fun b => f b) 0 < e
Tactic:
simp at N1
Proof state after:
case h
f : ℕ → ℂ
f0 : f 0 = 0
e : ℝ
ep : e > 0
N : Finset ℕ
N1 : 0 ∈ N
⊢ dist (N.prod fun b => f b) 0 < e
Theorem: product_head_zero
Proof state before:
case h
f : ℕ → ℂ
f0 : f 0 = 0
e : ℝ
ep : e > 0
N : Finset ℕ
N1 : 0 ∈ N
⊢ dist (N.prod fun b => f b) 0 < e
Tactic:
rw [Finset.prod_eq_zero N1 f0]
Proof state after:
case h
f : ℕ → ℂ
f0 : f 0 = 0
e : ℝ
ep : e > 0
N : Finset ℕ
N1 : 0 ∈ N
⊢ dist 0 0 < e
Theorem: product_head_zero
Proof state before:
case h
f : ℕ → ℂ
f0 : f 0 = 0
e : ℝ
ep : e > 0
N : Finset ℕ
N1 : 0 ∈ N
⊢ dist 0 0 < e
Tactic:
simpa
Proof state after:
no goals
Theorem: product_split
Proof state before:
f : ℕ → ℂ
h : ProdExists f
⊢ tprod f = f 0 * ∏' (n : ℕ), f (n + 1)
Tactic:
by_cases f0 : f 0 = 0
Proof state after:
case pos
f : ℕ → ℂ
h : ProdExists f
f0 : f 0 = 0
⊢ tprod f = f 0 * ∏' (n : ℕ), f (n + 1)

case neg
f : ℕ → ℂ
h : ProdExists f
f0 : ¬f 0 = 0
⊢ tprod f = f 0 * ∏' (n : ℕ), f (n + 1)
Theorem: product_split
Proof state before:
case neg
f : ℕ → ℂ
h : ProdExists f
f0 : ¬f 0 = 0
⊢ tprod f = f 0 * ∏' (n : ℕ), f (n + 1)
Tactic:
rw [product_drop' f0 h]
Proof state after:
case neg
f : ℕ → ℂ
h : ProdExists f
f0 : ¬f 0 = 0
⊢ tprod f = f 0 * (tprod f / f 0)
Theorem: product_split
Proof state before:
case neg
f : ℕ → ℂ
h : ProdExists f
f0 : ¬f 0 = 0
⊢ tprod f = f 0 * (tprod f / f 0)
Tactic:
field_simp
Proof state after:
no goals
Theorem: product_split
Proof state before:
case pos
f : ℕ → ℂ
h : ProdExists f
f0 : f 0 = 0
⊢ tprod f = f 0 * ∏' (n : ℕ), f (n + 1)
Tactic:
rw [f0, (product_head_zero f0).tprod_eq]
Proof state after:
case pos
f : ℕ → ℂ
h : ProdExists f
f0 : f 0 = 0
⊢ 0 = 0 * ∏' (n : ℕ), f (n + 1)
Theorem: product_split
Proof state before:
case pos
f : ℕ → ℂ
h : ProdExists f
f0 : f 0 = 0
⊢ 0 = 0 * ∏' (n : ℕ), f (n + 1)
Tactic:
simp
Proof state after:
no goals
Theorem: cauchy_on_cball_radius
Proof state before:
f : ℂ → ℂ
z : ℂ
r : ℝ≥0
rp : r > 0
h : AnalyticOn ℂ f (closedBall z ↑r)
⊢ HasFPowerSeriesOnBall f (cauchyPowerSeries f z ↑r) z ↑r
Tactic:
have hd : DifferentiableOn ℂ f (closedBall z r) := by
  intro x H; exact AnalyticAt.differentiableWithinAt (h x H)
Proof state after:
f : ℂ → ℂ
z : ℂ
r : ℝ≥0
rp : r > 0
h : AnalyticOn ℂ f (closedBall z ↑r)
hd : DifferentiableOn ℂ f (closedBall z ↑r)
⊢ HasFPowerSeriesOnBall f (cauchyPowerSeries f z ↑r) z ↑r
Theorem: cauchy_on_cball_radius
Proof state before:
f : ℂ → ℂ
z : ℂ
r : ℝ≥0
rp : r > 0
h : AnalyticOn ℂ f (closedBall z ↑r)
hd : DifferentiableOn ℂ f (closedBall z ↑r)
⊢ HasFPowerSeriesOnBall f (cauchyPowerSeries f z ↑r) z ↑r
Tactic:
set p : FormalMultilinearSeries ℂ ℂ ℂ := cauchyPowerSeries f z r
Proof state after:
f : ℂ → ℂ
z : ℂ
r : ℝ≥0
rp : r > 0
h : AnalyticOn ℂ f (closedBall z ↑r)
hd : DifferentiableOn ℂ f (closedBall z ↑r)
p : FormalMultilinearSeries ℂ ℂ ℂ := cauchyPowerSeries f z ↑r
⊢ HasFPowerSeriesOnBall f p z ↑r
Theorem: cauchy_on_cball_radius
Proof state before:
f : ℂ → ℂ
z : ℂ
r : ℝ≥0
rp : r > 0
h : AnalyticOn ℂ f (closedBall z ↑r)
hd : DifferentiableOn ℂ f (closedBall z ↑r)
p : FormalMultilinearSeries ℂ ℂ ℂ := cauchyPowerSeries f z ↑r
⊢ HasFPowerSeriesOnBall f p z ↑r
Tactic:
exact DifferentiableOn.hasFPowerSeriesOnBall hd rp
Proof state after:
no goals
Theorem: cauchy_on_cball_radius
Proof state before:
f : ℂ → ℂ
z : ℂ
r : ℝ≥0
rp : r > 0
h : AnalyticOn ℂ f (closedBall z ↑r)
⊢ DifferentiableOn ℂ f (closedBall z ↑r)
Tactic:
intro x H
Proof state after:
f : ℂ → ℂ
z : ℂ
r : ℝ≥0
rp : r > 0
h : AnalyticOn ℂ f (closedBall z ↑r)
x : ℂ
H : x ∈ closedBall z ↑r
⊢ DifferentiableWithinAt ℂ f (closedBall z ↑r) x
Theorem: cauchy_on_cball_radius
Proof state before:
f : ℂ → ℂ
z : ℂ
r : ℝ≥0
rp : r > 0
h : AnalyticOn ℂ f (closedBall z ↑r)
x : ℂ
H : x ∈ closedBall z ↑r
⊢ DifferentiableWithinAt ℂ f (closedBall z ↑r) x
Tactic:
exact AnalyticAt.differentiableWithinAt (h x H)
Proof state after:
no goals
Theorem: analyticOn_small_cball
Proof state before:
f : ℂ → ℂ
z : ℂ
r : ℝ≥0
h : AnalyticOn ℂ f (ball z ↑r)
s : ℝ≥0
sr : s < r
⊢ AnalyticOn ℂ f (closedBall z ↑s)
Tactic:
intro x hx
Proof state after:
f : ℂ → ℂ
z : ℂ
r : ℝ≥0
h : AnalyticOn ℂ f (ball z ↑r)
s : ℝ≥0
sr : s < r
x : ℂ
hx : x ∈ closedBall z ↑s
⊢ AnalyticAt ℂ f x
Theorem: analyticOn_small_cball
Proof state before:
f : ℂ → ℂ
z : ℂ
r : ℝ≥0
h : AnalyticOn ℂ f (ball z ↑r)
s : ℝ≥0
sr : s < r
x : ℂ
hx : x ∈ closedBall z ↑s
⊢ AnalyticAt ℂ f x
Tactic:
rw [closedBall] at hx
Proof state after:
f : ℂ → ℂ
z : ℂ
r : ℝ≥0
h : AnalyticOn ℂ f (ball z ↑r)
s : ℝ≥0
sr : s < r
x : ℂ
hx : x ∈ {y | dist y z ≤ ↑s}
⊢ AnalyticAt ℂ f x
Theorem: analyticOn_small_cball
Proof state before:
f : ℂ → ℂ
z : ℂ
r : ℝ≥0
h : AnalyticOn ℂ f (ball z ↑r)
s : ℝ≥0
sr : s < r
x : ℂ
hx : x ∈ {y | dist y z ≤ ↑s}
⊢ AnalyticAt ℂ f x
Tactic:
simp at hx
Proof state after:
f : ℂ → ℂ
z : ℂ
r : ℝ≥0
h : AnalyticOn ℂ f (ball z ↑r)
s : ℝ≥0
sr : s < r
x : ℂ
hx : nndist x z ≤ s
⊢ AnalyticAt ℂ f x
Theorem: analyticOn_small_cball
Proof state before:
f : ℂ → ℂ
z : ℂ
r : ℝ≥0
h : AnalyticOn ℂ f (ball z ↑r)
s : ℝ≥0
sr : s < r
x : ℂ
hx : nndist x z ≤ s
⊢ AnalyticAt ℂ f x
Tactic:
have hb : x ∈ ball z r := by
  rw [ball]; simp only [dist_lt_coe, Set.mem_setOf_eq]; exact lt_of_le_of_lt hx sr
Proof state after:
f : ℂ → ℂ
z : ℂ
r : ℝ≥0
h : AnalyticOn ℂ f (ball z ↑r)
s : ℝ≥0
sr : s < r
x : ℂ
hx : nndist x z ≤ s
hb : x ∈ ball z ↑r
⊢ AnalyticAt ℂ f x
Theorem: analyticOn_small_cball
Proof state before:
f : ℂ → ℂ
z : ℂ
r : ℝ≥0
h : AnalyticOn ℂ f (ball z ↑r)
s : ℝ≥0
sr : s < r
x : ℂ
hx : nndist x z ≤ s
hb : x ∈ ball z ↑r
⊢ AnalyticAt ℂ f x
Tactic:
exact h x hb
Proof state after:
no goals
Theorem: analyticOn_small_cball
Proof state before:
f : ℂ → ℂ
z : ℂ
r : ℝ≥0
h : AnalyticOn ℂ f (ball z ↑r)
s : ℝ≥0
sr : s < r
x : ℂ
hx : nndist x z ≤ s
⊢ x ∈ ball z ↑r
Tactic:
rw [ball]
Proof state after:
f : ℂ → ℂ
z : ℂ
r : ℝ≥0
h : AnalyticOn ℂ f (ball z ↑r)
s : ℝ≥0
sr : s < r
x : ℂ
hx : nndist x z ≤ s
⊢ x ∈ {y | dist y z < ↑r}
Theorem: analyticOn_small_cball
Proof state before:
f : ℂ → ℂ
z : ℂ
r : ℝ≥0
h : AnalyticOn ℂ f (ball z ↑r)
s : ℝ≥0
sr : s < r
x : ℂ
hx : nndist x z ≤ s
⊢ x ∈ {y | dist y z < ↑r}
Tactic:
simp only [dist_lt_coe, Set.mem_setOf_eq]
Proof state after:
f : ℂ → ℂ
z : ℂ
r : ℝ≥0
h : AnalyticOn ℂ f (ball z ↑r)
s : ℝ≥0
sr : s < r
x : ℂ
hx : nndist x z ≤ s
⊢ nndist x z < r
Theorem: analyticOn_small_cball
Proof state before:
f : ℂ → ℂ
z : ℂ
r : ℝ≥0
h : AnalyticOn ℂ f (ball z ↑r)
s : ℝ≥0
sr : s < r
x : ℂ
hx : nndist x z ≤ s
⊢ nndist x z < r
Tactic:
exact lt_of_le_of_lt hx sr
Proof state after:
no goals
Theorem: analyticOn_ball_radius
Proof state before:
f : ℂ → ℂ
z : ℂ
r : ℝ≥0
rp : r > 0
h : AnalyticOn ℂ f (ball z ↑r)
⊢ ∃ p, HasFPowerSeriesOnBall f p z ↑r
Tactic:
have h0 := analyticOn_small_cball h (r / 2) (NNReal.half_lt_self <| rp.ne')
Proof state after:
f : ℂ → ℂ
z : ℂ
r : ℝ≥0
rp : r > 0
h : AnalyticOn ℂ f (ball z ↑r)
h0 : AnalyticOn ℂ f (closedBall z ↑(r / 2))
⊢ ∃ p, HasFPowerSeriesOnBall f p z ↑r
Theorem: analyticOn_ball_radius
Proof state before:
f : ℂ → ℂ
z : ℂ
r : ℝ≥0
rp : r > 0
h : AnalyticOn ℂ f (ball z ↑r)
h0 : AnalyticOn ℂ f (closedBall z ↑(r / 2))
⊢ ∃ p, HasFPowerSeriesOnBall f p z ↑r
Tactic:
rcases analyticOn_cball_radius (half_pos rp) h0 with ⟨p, ph⟩
Proof state after:
case intro
f : ℂ → ℂ
z : ℂ
r : ℝ≥0
rp : r > 0
h : AnalyticOn ℂ f (ball z ↑r)
h0 : AnalyticOn ℂ f (closedBall z ↑(r / 2))
p : FormalMultilinearSeries ℂ ℂ ℂ
ph : HasFPowerSeriesOnBall f p z ↑(r / 2)
⊢ ∃ p, HasFPowerSeriesOnBall f p z ↑r
Theorem: analyticOn_ball_radius
Proof state before:
case intro
f : ℂ → ℂ
z : ℂ
r : ℝ≥0
rp : r > 0
h : AnalyticOn ℂ f (ball z ↑r)
h0 : AnalyticOn ℂ f (closedBall z ↑(r / 2))
p : FormalMultilinearSeries ℂ ℂ ℂ
ph : HasFPowerSeriesOnBall f p z ↑(r / 2)
⊢ ∃ p, HasFPowerSeriesOnBall f p z ↑r
Tactic:
set R := FormalMultilinearSeries.radius p
Proof state after:
case intro
f : ℂ → ℂ
z : ℂ
r : ℝ≥0
rp : r > 0
h : AnalyticOn ℂ f (ball z ↑r)
h0 : AnalyticOn ℂ f (closedBall z ↑(r / 2))
p : FormalMultilinearSeries ℂ ℂ ℂ
ph : HasFPowerSeriesOnBall f p z ↑(r / 2)
R : ENNReal := p.radius
⊢ ∃ p, HasFPowerSeriesOnBall f p z ↑r
Theorem: analyticOn_ball_radius
Proof state before:
case intro
f : ℂ → ℂ
z : ℂ
r : ℝ≥0
rp : r > 0
h : AnalyticOn ℂ f (ball z ↑r)
h0 : AnalyticOn ℂ f (closedBall z ↑(r / 2))
p : FormalMultilinearSeries ℂ ℂ ℂ
ph : HasFPowerSeriesOnBall f p z ↑(r / 2)
R : ENNReal := p.radius
⊢ ∃ p, HasFPowerSeriesOnBall f p z ↑r
Tactic:
refine
  ⟨p, {
      r_le := ?_
      r_pos := ENNReal.coe_pos.mpr rp
      hasSum := ?_ }⟩
Proof state after:
case intro.refine_1
f : ℂ → ℂ
z : ℂ
r : ℝ≥0
rp : r > 0
h : AnalyticOn ℂ f (ball z ↑r)
h0 : AnalyticOn ℂ f (closedBall z ↑(r / 2))
p : FormalMultilinearSeries ℂ ℂ ℂ
ph : HasFPowerSeriesOnBall f p z ↑(r / 2)
R : ENNReal := p.radius
⊢ ↑r ≤ p.radius

case intro.refine_2
f : ℂ → ℂ
z : ℂ
r : ℝ≥0
rp : r > 0
h : AnalyticOn ℂ f (ball z ↑r)
h0 : AnalyticOn ℂ f (closedBall z ↑(r / 2))
p : FormalMultilinearSeries ℂ ℂ ℂ
ph : HasFPowerSeriesOnBall f p z ↑(r / 2)
R : ENNReal := p.radius
⊢ ∀ {y : ℂ}, y ∈ EMetric.ball 0 ↑r → HasSum (fun n => (p n) fun x => y) (f (z + y))
Theorem: analyticOn_ball_radius
Proof state before:
case intro.refine_1
f : ℂ → ℂ
z : ℂ
r : ℝ≥0
rp : r > 0
h : AnalyticOn ℂ f (ball z ↑r)
h0 : AnalyticOn ℂ f (closedBall z ↑(r / 2))
p : FormalMultilinearSeries ℂ ℂ ℂ
ph : HasFPowerSeriesOnBall f p z ↑(r / 2)
R : ENNReal := p.radius
⊢ ↑r ≤ p.radius
Tactic:
apply ENNReal.le_of_forall_pos_nnreal_lt
Proof state after:
case intro.refine_1.h
f : ℂ → ℂ
z : ℂ
r : ℝ≥0
rp : r > 0
h : AnalyticOn ℂ f (ball z ↑r)
h0 : AnalyticOn ℂ f (closedBall z ↑(r / 2))
p : FormalMultilinearSeries ℂ ℂ ℂ
ph : HasFPowerSeriesOnBall f p z ↑(r / 2)
R : ENNReal := p.radius
⊢ ∀ (r_1 : ℝ≥0), 0 < r_1 → ↑r_1 < ↑r → ↑r_1 ≤ p.radius
Theorem: analyticOn_ball_radius
Proof state before:
case intro.refine_1.h
f : ℂ → ℂ
z : ℂ
r : ℝ≥0
rp : r > 0
h : AnalyticOn ℂ f (ball z ↑r)
h0 : AnalyticOn ℂ f (closedBall z ↑(r / 2))
p : FormalMultilinearSeries ℂ ℂ ℂ
ph : HasFPowerSeriesOnBall f p z ↑(r / 2)
R : ENNReal := p.radius
⊢ ∀ (r_1 : ℝ≥0), 0 < r_1 → ↑r_1 < ↑r → ↑r_1 ≤ p.radius
Tactic:
intro t tp tr
Proof state after:
case intro.refine_1.h
f : ℂ → ℂ
z : ℂ
r : ℝ≥0
rp : r > 0
h : AnalyticOn ℂ f (ball z ↑r)
h0 : AnalyticOn ℂ f (closedBall z ↑(r / 2))
p : FormalMultilinearSeries ℂ ℂ ℂ
ph : HasFPowerSeriesOnBall f p z ↑(r / 2)
R : ENNReal := p.radius
t : ℝ≥0
tp : 0 < t
tr : ↑t < ↑r
⊢ ↑t ≤ p.radius
Theorem: analyticOn_ball_radius
Proof state before:
case intro.refine_1.h
f : ℂ → ℂ
z : ℂ
r : ℝ≥0
rp : r > 0
h : AnalyticOn ℂ f (ball z ↑r)
h0 : AnalyticOn ℂ f (closedBall z ↑(r / 2))
p : FormalMultilinearSeries ℂ ℂ ℂ
ph : HasFPowerSeriesOnBall f p z ↑(r / 2)
R : ENNReal := p.radius
t : ℝ≥0
tp : 0 < t
tr : ↑t < ↑r
⊢ ↑t ≤ p.radius
Tactic:
have ht := analyticOn_small_cball h t (ENNReal.coe_lt_coe.mp tr)
Proof state after:
case intro.refine_1.h
f : ℂ → ℂ
z : ℂ
r : ℝ≥0
rp : r > 0
h : AnalyticOn ℂ f (ball z ↑r)
h0 : AnalyticOn ℂ f (closedBall z ↑(r / 2))
p : FormalMultilinearSeries ℂ ℂ ℂ
ph : HasFPowerSeriesOnBall f p z ↑(r / 2)
R : ENNReal := p.radius
t : ℝ≥0
tp : 0 < t
tr : ↑t < ↑r
ht : AnalyticOn ℂ f (closedBall z ↑t)
⊢ ↑t ≤ p.radius
Theorem: analyticOn_ball_radius
Proof state before:
case intro.refine_1.h
f : ℂ → ℂ
z : ℂ
r : ℝ≥0
rp : r > 0
h : AnalyticOn ℂ f (ball z ↑r)
h0 : AnalyticOn ℂ f (closedBall z ↑(r / 2))
p : FormalMultilinearSeries ℂ ℂ ℂ
ph : HasFPowerSeriesOnBall f p z ↑(r / 2)
R : ENNReal := p.radius
t : ℝ≥0
tp : 0 < t
tr : ↑t < ↑r
ht : AnalyticOn ℂ f (closedBall z ↑t)
⊢ ↑t ≤ p.radius
Tactic:
rcases analyticOn_cball_radius tp ht with ⟨p', hp'⟩
Proof state after:
case intro.refine_1.h.intro
f : ℂ → ℂ
z : ℂ
r : ℝ≥0
rp : r > 0
h : AnalyticOn ℂ f (ball z ↑r)
h0 : AnalyticOn ℂ f (closedBall z ↑(r / 2))
p : FormalMultilinearSeries ℂ ℂ ℂ
ph : HasFPowerSeriesOnBall f p z ↑(r / 2)
R : ENNReal := p.radius
t : ℝ≥0
tp : 0 < t
tr : ↑t < ↑r
ht : AnalyticOn ℂ f (closedBall z ↑t)
p' : FormalMultilinearSeries ℂ ℂ ℂ
hp' : HasFPowerSeriesOnBall f p' z ↑t
⊢ ↑t ≤ p.radius
Theorem: analyticOn_ball_radius
Proof state before:
case intro.refine_1.h.intro
f : ℂ → ℂ
z : ℂ
r : ℝ≥0
rp : r > 0
h : AnalyticOn ℂ f (ball z ↑r)
h0 : AnalyticOn ℂ f (closedBall z ↑(r / 2))
p : FormalMultilinearSeries ℂ ℂ ℂ
ph : HasFPowerSeriesOnBall f p z ↑(r / 2)
R : ENNReal := p.radius
t : ℝ≥0
tp : 0 < t
tr : ↑t < ↑r
ht : AnalyticOn ℂ f (closedBall z ↑t)
p' : FormalMultilinearSeries ℂ ℂ ℂ
hp' : HasFPowerSeriesOnBall f p' z ↑t
⊢ ↑t ≤ p.radius
Tactic:
have pp : p = p' := HasFPowerSeriesAt.eq_formalMultilinearSeries ⟨↑(r / 2), ph⟩ ⟨t, hp'⟩
Proof state after:
case intro.refine_1.h.intro
f : ℂ → ℂ
z : ℂ
r : ℝ≥0
rp : r > 0
h : AnalyticOn ℂ f (ball z ↑r)
h0 : AnalyticOn ℂ f (closedBall z ↑(r / 2))
p : FormalMultilinearSeries ℂ ℂ ℂ
ph : HasFPowerSeriesOnBall f p z ↑(r / 2)
R : ENNReal := p.radius
t : ℝ≥0
tp : 0 < t
tr : ↑t < ↑r
ht : AnalyticOn ℂ f (closedBall z ↑t)
p' : FormalMultilinearSeries ℂ ℂ ℂ
hp' : HasFPowerSeriesOnBall f p' z ↑t
pp : p = p'
⊢ ↑t ≤ p.radius
Theorem: analyticOn_ball_radius
Proof state before:
case intro.refine_1.h.intro
f : ℂ → ℂ
z : ℂ
r : ℝ≥0
rp : r > 0
h : AnalyticOn ℂ f (ball z ↑r)
h0 : AnalyticOn ℂ f (closedBall z ↑(r / 2))
p : FormalMultilinearSeries ℂ ℂ ℂ
ph : HasFPowerSeriesOnBall f p z ↑(r / 2)
R : ENNReal := p.radius
t : ℝ≥0
tp : 0 < t
tr : ↑t < ↑r
ht : AnalyticOn ℂ f (closedBall z ↑t)
p' : FormalMultilinearSeries ℂ ℂ ℂ
hp' : HasFPowerSeriesOnBall f p' z ↑t
pp : p = p'
⊢ ↑t ≤ p.radius
Tactic:
rw [← pp] at hp'
Proof state after:
case intro.refine_1.h.intro
f : ℂ → ℂ
z : ℂ
r : ℝ≥0
rp : r > 0
h : AnalyticOn ℂ f (ball z ↑r)
h0 : AnalyticOn ℂ f (closedBall z ↑(r / 2))
p : FormalMultilinearSeries ℂ ℂ ℂ
ph : HasFPowerSeriesOnBall f p z ↑(r / 2)
R : ENNReal := p.radius
t : ℝ≥0
tp : 0 < t
tr : ↑t < ↑r
ht : AnalyticOn ℂ f (closedBall z ↑t)
p' : FormalMultilinearSeries ℂ ℂ ℂ
hp' : HasFPowerSeriesOnBall f p z ↑t
pp : p = p'
⊢ ↑t ≤ p.radius
Theorem: analyticOn_ball_radius
Proof state before:
case intro.refine_1.h.intro
f : ℂ → ℂ
z : ℂ
r : ℝ≥0
rp : r > 0
h : AnalyticOn ℂ f (ball z ↑r)
h0 : AnalyticOn ℂ f (closedBall z ↑(r / 2))
p : FormalMultilinearSeries ℂ ℂ ℂ
ph : HasFPowerSeriesOnBall f p z ↑(r / 2)
R : ENNReal := p.radius
t : ℝ≥0
tp : 0 < t
tr : ↑t < ↑r
ht : AnalyticOn ℂ f (closedBall z ↑t)
p' : FormalMultilinearSeries ℂ ℂ ℂ
hp' : HasFPowerSeriesOnBall f p z ↑t
pp : p = p'
⊢ ↑t ≤ p.radius
Tactic:
refine hp'.r_le
Proof state after:
no goals
Theorem: analyticOn_ball_radius
Proof state before:
case intro.refine_2
f : ℂ → ℂ
z : ℂ
r : ℝ≥0
rp : r > 0
h : AnalyticOn ℂ f (ball z ↑r)
h0 : AnalyticOn ℂ f (closedBall z ↑(r / 2))
p : FormalMultilinearSeries ℂ ℂ ℂ
ph : HasFPowerSeriesOnBall f p z ↑(r / 2)
R : ENNReal := p.radius
⊢ ∀ {y : ℂ}, y ∈ EMetric.ball 0 ↑r → HasSum (fun n => (p n) fun x => y) (f (z + y))
Tactic:
intro y yr
Proof state after:
case intro.refine_2
f : ℂ → ℂ
z : ℂ
r : ℝ≥0
rp : r > 0
h : AnalyticOn ℂ f (ball z ↑r)
h0 : AnalyticOn ℂ f (closedBall z ↑(r / 2))
p : FormalMultilinearSeries ℂ ℂ ℂ
ph : HasFPowerSeriesOnBall f p z ↑(r / 2)
R : ENNReal := p.radius
y : ℂ
yr : y ∈ EMetric.ball 0 ↑r
⊢ HasSum (fun n => (p n) fun x => y) (f (z + y))
Theorem: analyticOn_ball_radius
Proof state before:
case intro.refine_2
f : ℂ → ℂ
z : ℂ
r : ℝ≥0
rp : r > 0
h : AnalyticOn ℂ f (ball z ↑r)
h0 : AnalyticOn ℂ f (closedBall z ↑(r / 2))
p : FormalMultilinearSeries ℂ ℂ ℂ
ph : HasFPowerSeriesOnBall f p z ↑(r / 2)
R : ENNReal := p.radius
y : ℂ
yr : y ∈ EMetric.ball 0 ↑r
⊢ HasSum (fun n => (p n) fun x => y) (f (z + y))
Tactic:
rw [EMetric.ball, Set.mem_setOf] at yr
Proof state after:
case intro.refine_2
f : ℂ → ℂ
z : ℂ
r : ℝ≥0
rp : r > 0
h : AnalyticOn ℂ f (ball z ↑r)
h0 : AnalyticOn ℂ f (closedBall z ↑(r / 2))
p : FormalMultilinearSeries ℂ ℂ ℂ
ph : HasFPowerSeriesOnBall f p z ↑(r / 2)
R : ENNReal := p.radius
y : ℂ
yr : edist y 0 < ↑r
⊢ HasSum (fun n => (p n) fun x => y) (f (z + y))
Theorem: analyticOn_ball_radius
Proof state before:
case intro.refine_2
f : ℂ → ℂ
z : ℂ
r : ℝ≥0
rp : r > 0
h : AnalyticOn ℂ f (ball z ↑r)
h0 : AnalyticOn ℂ f (closedBall z ↑(r / 2))
p : FormalMultilinearSeries ℂ ℂ ℂ
ph : HasFPowerSeriesOnBall f p z ↑(r / 2)
R : ENNReal := p.radius
y : ℂ
yr : edist y 0 < ↑r
⊢ HasSum (fun n => (p n) fun x => y) (f (z + y))
Tactic:
rcases exists_between yr with ⟨t, t0, t1⟩
Proof state after:
case intro.refine_2.intro.intro
f : ℂ → ℂ
z : ℂ
r : ℝ≥0
rp : r > 0
h : AnalyticOn ℂ f (ball z ↑r)
h0 : AnalyticOn ℂ f (closedBall z ↑(r / 2))
p : FormalMultilinearSeries ℂ ℂ ℂ
ph : HasFPowerSeriesOnBall f p z ↑(r / 2)
R : ENNReal := p.radius
y : ℂ
yr : edist y 0 < ↑r
t : ENNReal
t0 : edist y 0 < t
t1 : t < ↑r
⊢ HasSum (fun n => (p n) fun x => y) (f (z + y))
Theorem: analyticOn_ball_radius
Proof state before:
case intro.refine_2.intro.intro
f : ℂ → ℂ
z : ℂ
r : ℝ≥0
rp : r > 0
h : AnalyticOn ℂ f (ball z ↑r)
h0 : AnalyticOn ℂ f (closedBall z ↑(r / 2))
p : FormalMultilinearSeries ℂ ℂ ℂ
ph : HasFPowerSeriesOnBall f p z ↑(r / 2)
R : ENNReal := p.radius
y : ℂ
yr : edist y 0 < ↑r
t : ENNReal
t0 : edist y 0 < t
t1 : t < ↑r
⊢ HasSum (fun n => (p n) fun x => y) (f (z + y))
Tactic:
have t1' : t.toNNReal < r := by
  rw [← WithTop.coe_lt_coe]; exact lt_of_le_of_lt ENNReal.coe_toNNReal_le_self t1
Proof state after:
case intro.refine_2.intro.intro
f : ℂ → ℂ
z : ℂ
r : ℝ≥0
rp : r > 0
h : AnalyticOn ℂ f (ball z ↑r)
h0 : AnalyticOn ℂ f (closedBall z ↑(r / 2))
p : FormalMultilinearSeries ℂ ℂ ℂ
ph : HasFPowerSeriesOnBall f p z ↑(r / 2)
R : ENNReal := p.radius
y : ℂ
yr : edist y 0 < ↑r
t : ENNReal
t0 : edist y 0 < t
t1 : t < ↑r
t1' : t.toNNReal < r
⊢ HasSum (fun n => (p n) fun x => y) (f (z + y))
Theorem: analyticOn_ball_radius
Proof state before:
case intro.refine_2.intro.intro
f : ℂ → ℂ
z : ℂ
r : ℝ≥0
rp : r > 0
h : AnalyticOn ℂ f (ball z ↑r)
h0 : AnalyticOn ℂ f (closedBall z ↑(r / 2))
p : FormalMultilinearSeries ℂ ℂ ℂ
ph : HasFPowerSeriesOnBall f p z ↑(r / 2)
R : ENNReal := p.radius
y : ℂ
yr : edist y 0 < ↑r
t : ENNReal
t0 : edist y 0 < t
t1 : t < ↑r
t1' : t.toNNReal < r
⊢ HasSum (fun n => (p n) fun x => y) (f (z + y))
Tactic:
have ht := analyticOn_small_cball h t.toNNReal t1'
Proof state after:
case intro.refine_2.intro.intro
f : ℂ → ℂ
z : ℂ
r : ℝ≥0
rp : r > 0
h : AnalyticOn ℂ f (ball z ↑r)
h0 : AnalyticOn ℂ f (closedBall z ↑(r / 2))
p : FormalMultilinearSeries ℂ ℂ ℂ
ph : HasFPowerSeriesOnBall f p z ↑(r / 2)
R : ENNReal := p.radius
y : ℂ
yr : edist y 0 < ↑r
t : ENNReal
t0 : edist y 0 < t
t1 : t < ↑r
t1' : t.toNNReal < r
ht : AnalyticOn ℂ f (closedBall z ↑t.toNNReal)
⊢ HasSum (fun n => (p n) fun x => y) (f (z + y))
Theorem: analyticOn_ball_radius
Proof state before:
case intro.refine_2.intro.intro
f : ℂ → ℂ
z : ℂ
r : ℝ≥0
rp : r > 0
h : AnalyticOn ℂ f (ball z ↑r)
h0 : AnalyticOn ℂ f (closedBall z ↑(r / 2))
p : FormalMultilinearSeries ℂ ℂ ℂ
ph : HasFPowerSeriesOnBall f p z ↑(r / 2)
R : ENNReal := p.radius
y : ℂ
yr : edist y 0 < ↑r
t : ENNReal
t0 : edist y 0 < t
t1 : t < ↑r
t1' : t.toNNReal < r
ht : AnalyticOn ℂ f (closedBall z ↑t.toNNReal)
⊢ HasSum (fun n => (p n) fun x => y) (f (z + y))
Tactic:
have tp : 0 < ENNReal.toNNReal t :=
  ENNReal.toNNReal_pos (ne_of_gt <| pos_of_gt t0) (ne_top_of_lt t1)
Proof state after:
case intro.refine_2.intro.intro
f : ℂ → ℂ
z : ℂ
r : ℝ≥0
rp : r > 0
h : AnalyticOn ℂ f (ball z ↑r)
h0 : AnalyticOn ℂ f (closedBall z ↑(r / 2))
p : FormalMultilinearSeries ℂ ℂ ℂ
ph : HasFPowerSeriesOnBall f p z ↑(r / 2)
R : ENNReal := p.radius
y : ℂ
yr : edist y 0 < ↑r
t : ENNReal
t0 : edist y 0 < t
t1 : t < ↑r
t1' : t.toNNReal < r
ht : AnalyticOn ℂ f (closedBall z ↑t.toNNReal)
tp : 0 < t.toNNReal
⊢ HasSum (fun n => (p n) fun x => y) (f (z + y))
Theorem: analyticOn_ball_radius
Proof state before:
case intro.refine_2.intro.intro
f : ℂ → ℂ
z : ℂ
r : ℝ≥0
rp : r > 0
h : AnalyticOn ℂ f (ball z ↑r)
h0 : AnalyticOn ℂ f (closedBall z ↑(r / 2))
p : FormalMultilinearSeries ℂ ℂ ℂ
ph : HasFPowerSeriesOnBall f p z ↑(r / 2)
R : ENNReal := p.radius
y : ℂ
yr : edist y 0 < ↑r
t : ENNReal
t0 : edist y 0 < t
t1 : t < ↑r
t1' : t.toNNReal < r
ht : AnalyticOn ℂ f (closedBall z ↑t.toNNReal)
tp : 0 < t.toNNReal
⊢ HasSum (fun n => (p n) fun x => y) (f (z + y))
Tactic:
rcases analyticOn_cball_radius tp ht with ⟨p', hp'⟩
Proof state after:
case intro.refine_2.intro.intro.intro
f : ℂ → ℂ
z : ℂ
r : ℝ≥0
rp : r > 0
h : AnalyticOn ℂ f (ball z ↑r)
h0 : AnalyticOn ℂ f (closedBall z ↑(r / 2))
p : FormalMultilinearSeries ℂ ℂ ℂ
ph : HasFPowerSeriesOnBall f p z ↑(r / 2)
R : ENNReal := p.radius
y : ℂ
yr : edist y 0 < ↑r
t : ENNReal
t0 : edist y 0 < t
t1 : t < ↑r
t1' : t.toNNReal < r
ht : AnalyticOn ℂ f (closedBall z ↑t.toNNReal)
tp : 0 < t.toNNReal
p' : FormalMultilinearSeries ℂ ℂ ℂ
hp' : HasFPowerSeriesOnBall f p' z ↑t.toNNReal
⊢ HasSum (fun n => (p n) fun x => y) (f (z + y))
Theorem: analyticOn_ball_radius
Proof state before:
case intro.refine_2.intro.intro.intro
f : ℂ → ℂ
z : ℂ
r : ℝ≥0
rp : r > 0
h : AnalyticOn ℂ f (ball z ↑r)
h0 : AnalyticOn ℂ f (closedBall z ↑(r / 2))
p : FormalMultilinearSeries ℂ ℂ ℂ
ph : HasFPowerSeriesOnBall f p z ↑(r / 2)
R : ENNReal := p.radius
y : ℂ
yr : edist y 0 < ↑r
t : ENNReal
t0 : edist y 0 < t
t1 : t < ↑r
t1' : t.toNNReal < r
ht : AnalyticOn ℂ f (closedBall z ↑t.toNNReal)
tp : 0 < t.toNNReal
p' : FormalMultilinearSeries ℂ ℂ ℂ
hp' : HasFPowerSeriesOnBall f p' z ↑t.toNNReal
⊢ HasSum (fun n => (p n) fun x => y) (f (z + y))
Tactic:
have pp : p = p' :=
  HasFPowerSeriesAt.eq_formalMultilinearSeries ⟨↑(r / 2), ph⟩ ⟨t.toNNReal, hp'⟩
Proof state after:
case intro.refine_2.intro.intro.intro
f : ℂ → ℂ
z : ℂ
r : ℝ≥0
rp : r > 0
h : AnalyticOn ℂ f (ball z ↑r)
h0 : AnalyticOn ℂ f (closedBall z ↑(r / 2))
p : FormalMultilinearSeries ℂ ℂ ℂ
ph : HasFPowerSeriesOnBall f p z ↑(r / 2)
R : ENNReal := p.radius
y : ℂ
yr : edist y 0 < ↑r
t : ENNReal
t0 : edist y 0 < t
t1 : t < ↑r
t1' : t.toNNReal < r
ht : AnalyticOn ℂ f (closedBall z ↑t.toNNReal)
tp : 0 < t.toNNReal
p' : FormalMultilinearSeries ℂ ℂ ℂ
hp' : HasFPowerSeriesOnBall f p' z ↑t.toNNReal
pp : p = p'
⊢ HasSum (fun n => (p n) fun x => y) (f (z + y))