internlm/Lean-Github huggingface dataset:
Theorem: cauchy_sub
Proof state before:
f g : ℂ → ℂ
c : ℂ
r : ℝ≥0
n : ℕ
w : ℂ
rp : r > 0
cf : ContinuousOn f (closedBall c ↑r)
cg : ContinuousOn g (closedBall c ↑r)
⊢ (((2 * ↑π * I)⁻¹ • ∮ (z : ℂ) in C(c, ↑r), (w / (z - c)) ^ n • (z - c)⁻¹ • f z) -
      (2 * ↑π * I)⁻¹ • ∮ (z : ℂ) in C(c, ↑r), (w / (z - c)) ^ n • (z - c)⁻¹ • g z) =
    (2 * ↑π * I)⁻¹ • ∮ (z : ℂ) in C(c, ↑r), (w / (z - c)) ^ n • (z - c)⁻¹ • (f - g) z
Tactic:
set s : ℂ := (2 * π * I)⁻¹
Proof state after:
f g : ℂ → ℂ
c : ℂ
r : ℝ≥0
n : ℕ
w : ℂ
rp : r > 0
cf : ContinuousOn f (closedBall c ↑r)
cg : ContinuousOn g (closedBall c ↑r)
s : ℂ := (2 * ↑π * I)⁻¹
⊢ ((s • ∮ (z : ℂ) in C(c, ↑r), (w / (z - c)) ^ n • (z - c)⁻¹ • f z) -
      s • ∮ (z : ℂ) in C(c, ↑r), (w / (z - c)) ^ n • (z - c)⁻¹ • g z) =
    s • ∮ (z : ℂ) in C(c, ↑r), (w / (z - c)) ^ n • (z - c)⁻¹ • (f - g) z
Theorem: cauchy_sub
Proof state before:
f g : ℂ → ℂ
c : ℂ
r : ℝ≥0
n : ℕ
w : ℂ
rp : r > 0
cf : ContinuousOn f (closedBall c ↑r)
cg : ContinuousOn g (closedBall c ↑r)
s : ℂ := (2 * ↑π * I)⁻¹
⊢ ((s • ∮ (z : ℂ) in C(c, ↑r), (w / (z - c)) ^ n • (z - c)⁻¹ • f z) -
      s • ∮ (z : ℂ) in C(c, ↑r), (w / (z - c)) ^ n • (z - c)⁻¹ • g z) =
    s • ∮ (z : ℂ) in C(c, ↑r), (w / (z - c)) ^ n • (z - c)⁻¹ • (f - g) z
Tactic:
simp only [div_pow, Algebra.id.smul_eq_mul, Pi.sub_apply]
Proof state after:
f g : ℂ → ℂ
c : ℂ
r : ℝ≥0
n : ℕ
w : ℂ
rp : r > 0
cf : ContinuousOn f (closedBall c ↑r)
cg : ContinuousOn g (closedBall c ↑r)
s : ℂ := (2 * ↑π * I)⁻¹
⊢ ((s * ∮ (z : ℂ) in C(c, ↑r), w ^ n / (z - c) ^ n * ((z - c)⁻¹ * f z)) -
      s * ∮ (z : ℂ) in C(c, ↑r), w ^ n / (z - c) ^ n * ((z - c)⁻¹ * g z)) =
    s * ∮ (z : ℂ) in C(c, ↑r), w ^ n / (z - c) ^ n * ((z - c)⁻¹ * (f z - g z))
Theorem: cauchy_sub
Proof state before:
f g : ℂ → ℂ
c : ℂ
r : ℝ≥0
n : ℕ
w : ℂ
rp : r > 0
cf : ContinuousOn f (closedBall c ↑r)
cg : ContinuousOn g (closedBall c ↑r)
s : ℂ := (2 * ↑π * I)⁻¹
⊢ ((s * ∮ (z : ℂ) in C(c, ↑r), w ^ n / (z - c) ^ n * ((z - c)⁻¹ * f z)) -
      s * ∮ (z : ℂ) in C(c, ↑r), w ^ n / (z - c) ^ n * ((z - c)⁻¹ * g z)) =
    s * ∮ (z : ℂ) in C(c, ↑r), w ^ n / (z - c) ^ n * ((z - c)⁻¹ * (f z - g z))
Tactic:
have fi := cauchy_is_circleIntegrable n w rp cf
Proof state after:
f g : ℂ → ℂ
c : ℂ
r : ℝ≥0
n : ℕ
w : ℂ
rp : r > 0
cf : ContinuousOn f (closedBall c ↑r)
cg : ContinuousOn g (closedBall c ↑r)
s : ℂ := (2 * ↑π * I)⁻¹
fi : CircleIntegrable (fun z => w ^ n / (z - c) ^ n * ((z - c)⁻¹ * f z)) c ↑r
⊢ ((s * ∮ (z : ℂ) in C(c, ↑r), w ^ n / (z - c) ^ n * ((z - c)⁻¹ * f z)) -
      s * ∮ (z : ℂ) in C(c, ↑r), w ^ n / (z - c) ^ n * ((z - c)⁻¹ * g z)) =
    s * ∮ (z : ℂ) in C(c, ↑r), w ^ n / (z - c) ^ n * ((z - c)⁻¹ * (f z - g z))
Theorem: cauchy_sub
Proof state before:
f g : ℂ → ℂ
c : ℂ
r : ℝ≥0
n : ℕ
w : ℂ
rp : r > 0
cf : ContinuousOn f (closedBall c ↑r)
cg : ContinuousOn g (closedBall c ↑r)
s : ℂ := (2 * ↑π * I)⁻¹
fi : CircleIntegrable (fun z => w ^ n / (z - c) ^ n * ((z - c)⁻¹ * f z)) c ↑r
⊢ ((s * ∮ (z : ℂ) in C(c, ↑r), w ^ n / (z - c) ^ n * ((z - c)⁻¹ * f z)) -
      s * ∮ (z : ℂ) in C(c, ↑r), w ^ n / (z - c) ^ n * ((z - c)⁻¹ * g z)) =
    s * ∮ (z : ℂ) in C(c, ↑r), w ^ n / (z - c) ^ n * ((z - c)⁻¹ * (f z - g z))
Tactic:
have gi := cauchy_is_circleIntegrable n w rp cg
Proof state after:
f g : ℂ → ℂ
c : ℂ
r : ℝ≥0
n : ℕ
w : ℂ
rp : r > 0
cf : ContinuousOn f (closedBall c ↑r)
cg : ContinuousOn g (closedBall c ↑r)
s : ℂ := (2 * ↑π * I)⁻¹
fi : CircleIntegrable (fun z => w ^ n / (z - c) ^ n * ((z - c)⁻¹ * f z)) c ↑r
gi : CircleIntegrable (fun z => w ^ n / (z - c) ^ n * ((z - c)⁻¹ * g z)) c ↑r
⊢ ((s * ∮ (z : ℂ) in C(c, ↑r), w ^ n / (z - c) ^ n * ((z - c)⁻¹ * f z)) -
      s * ∮ (z : ℂ) in C(c, ↑r), w ^ n / (z - c) ^ n * ((z - c)⁻¹ * g z)) =
    s * ∮ (z : ℂ) in C(c, ↑r), w ^ n / (z - c) ^ n * ((z - c)⁻¹ * (f z - g z))
Theorem: cauchy_sub
Proof state before:
f g : ℂ → ℂ
c : ℂ
r : ℝ≥0
n : ℕ
w : ℂ
rp : r > 0
cf : ContinuousOn f (closedBall c ↑r)
cg : ContinuousOn g (closedBall c ↑r)
s : ℂ := (2 * ↑π * I)⁻¹
fi : CircleIntegrable (fun z => w ^ n / (z - c) ^ n * ((z - c)⁻¹ * f z)) c ↑r
gi : CircleIntegrable (fun z => w ^ n / (z - c) ^ n * ((z - c)⁻¹ * g z)) c ↑r
⊢ ((s * ∮ (z : ℂ) in C(c, ↑r), w ^ n / (z - c) ^ n * ((z - c)⁻¹ * f z)) -
      s * ∮ (z : ℂ) in C(c, ↑r), w ^ n / (z - c) ^ n * ((z - c)⁻¹ * g z)) =
    s * ∮ (z : ℂ) in C(c, ↑r), w ^ n / (z - c) ^ n * ((z - c)⁻¹ * (f z - g z))
Tactic:
have cia := circleIntegral_sub fi gi
Proof state after:
f g : ℂ → ℂ
c : ℂ
r : ℝ≥0
n : ℕ
w : ℂ
rp : r > 0
cf : ContinuousOn f (closedBall c ↑r)
cg : ContinuousOn g (closedBall c ↑r)
s : ℂ := (2 * ↑π * I)⁻¹
fi : CircleIntegrable (fun z => w ^ n / (z - c) ^ n * ((z - c)⁻¹ * f z)) c ↑r
gi : CircleIntegrable (fun z => w ^ n / (z - c) ^ n * ((z - c)⁻¹ * g z)) c ↑r
cia :
  ((∮ (z : ℂ) in C(c, ↑r), w ^ n / (z - c) ^ n * ((z - c)⁻¹ * f z)) -
      ∮ (z : ℂ) in C(c, ↑r), w ^ n / (z - c) ^ n * ((z - c)⁻¹ * g z)) =
    circleIntegral
      ((fun z => w ^ n / (z - c) ^ n * ((z - c)⁻¹ * f z)) - fun z => w ^ n / (z - c) ^ n * ((z - c)⁻¹ * g z)) c ↑r
⊢ ((s * ∮ (z : ℂ) in C(c, ↑r), w ^ n / (z - c) ^ n * ((z - c)⁻¹ * f z)) -
      s * ∮ (z : ℂ) in C(c, ↑r), w ^ n / (z - c) ^ n * ((z - c)⁻¹ * g z)) =
    s * ∮ (z : ℂ) in C(c, ↑r), w ^ n / (z - c) ^ n * ((z - c)⁻¹ * (f z - g z))
Theorem: cauchy_sub
Proof state before:
f g : ℂ → ℂ
c : ℂ
r : ℝ≥0
n : ℕ
w : ℂ
rp : r > 0
cf : ContinuousOn f (closedBall c ↑r)
cg : ContinuousOn g (closedBall c ↑r)
s : ℂ := (2 * ↑π * I)⁻¹
fi : CircleIntegrable (fun z => w ^ n / (z - c) ^ n * ((z - c)⁻¹ * f z)) c ↑r
gi : CircleIntegrable (fun z => w ^ n / (z - c) ^ n * ((z - c)⁻¹ * g z)) c ↑r
cia :
  ((∮ (z : ℂ) in C(c, ↑r), w ^ n / (z - c) ^ n * ((z - c)⁻¹ * f z)) -
      ∮ (z : ℂ) in C(c, ↑r), w ^ n / (z - c) ^ n * ((z - c)⁻¹ * g z)) =
    circleIntegral
      ((fun z => w ^ n / (z - c) ^ n * ((z - c)⁻¹ * f z)) - fun z => w ^ n / (z - c) ^ n * ((z - c)⁻¹ * g z)) c ↑r
⊢ ((s * ∮ (z : ℂ) in C(c, ↑r), w ^ n / (z - c) ^ n * ((z - c)⁻¹ * f z)) -
      s * ∮ (z : ℂ) in C(c, ↑r), w ^ n / (z - c) ^ n * ((z - c)⁻¹ * g z)) =
    s * ∮ (z : ℂ) in C(c, ↑r), w ^ n / (z - c) ^ n * ((z - c)⁻¹ * (f z - g z))
Tactic:
rw [← mul_sub_left_distrib, cia]
Proof state after:
f g : ℂ → ℂ
c : ℂ
r : ℝ≥0
n : ℕ
w : ℂ
rp : r > 0
cf : ContinuousOn f (closedBall c ↑r)
cg : ContinuousOn g (closedBall c ↑r)
s : ℂ := (2 * ↑π * I)⁻¹
fi : CircleIntegrable (fun z => w ^ n / (z - c) ^ n * ((z - c)⁻¹ * f z)) c ↑r
gi : CircleIntegrable (fun z => w ^ n / (z - c) ^ n * ((z - c)⁻¹ * g z)) c ↑r
cia :
  ((∮ (z : ℂ) in C(c, ↑r), w ^ n / (z - c) ^ n * ((z - c)⁻¹ * f z)) -
      ∮ (z : ℂ) in C(c, ↑r), w ^ n / (z - c) ^ n * ((z - c)⁻¹ * g z)) =
    circleIntegral
      ((fun z => w ^ n / (z - c) ^ n * ((z - c)⁻¹ * f z)) - fun z => w ^ n / (z - c) ^ n * ((z - c)⁻¹ * g z)) c ↑r
⊢ s *
      circleIntegral
        ((fun z => w ^ n / (z - c) ^ n * ((z - c)⁻¹ * f z)) - fun z => w ^ n / (z - c) ^ n * ((z - c)⁻¹ * g z)) c ↑r =
    s * ∮ (z : ℂ) in C(c, ↑r), w ^ n / (z - c) ^ n * ((z - c)⁻¹ * (f z - g z))
Theorem: cauchy_sub
Proof state before:
f g : ℂ → ℂ
c : ℂ
r : ℝ≥0
n : ℕ
w : ℂ
rp : r > 0
cf : ContinuousOn f (closedBall c ↑r)
cg : ContinuousOn g (closedBall c ↑r)
s : ℂ := (2 * ↑π * I)⁻¹
fi : CircleIntegrable (fun z => w ^ n / (z - c) ^ n * ((z - c)⁻¹ * f z)) c ↑r
gi : CircleIntegrable (fun z => w ^ n / (z - c) ^ n * ((z - c)⁻¹ * g z)) c ↑r
cia :
  ((∮ (z : ℂ) in C(c, ↑r), w ^ n / (z - c) ^ n * ((z - c)⁻¹ * f z)) -
      ∮ (z : ℂ) in C(c, ↑r), w ^ n / (z - c) ^ n * ((z - c)⁻¹ * g z)) =
    circleIntegral
      ((fun z => w ^ n / (z - c) ^ n * ((z - c)⁻¹ * f z)) - fun z => w ^ n / (z - c) ^ n * ((z - c)⁻¹ * g z)) c ↑r
⊢ s *
      circleIntegral
        ((fun z => w ^ n / (z - c) ^ n * ((z - c)⁻¹ * f z)) - fun z => w ^ n / (z - c) ^ n * ((z - c)⁻¹ * g z)) c ↑r =
    s * ∮ (z : ℂ) in C(c, ↑r), w ^ n / (z - c) ^ n * ((z - c)⁻¹ * (f z - g z))
Tactic:
clear cia fi gi cf cg rp
Proof state after:
f g : ℂ → ℂ
c : ℂ
r : ℝ≥0
n : ℕ
w : ℂ
s : ℂ := (2 * ↑π * I)⁻¹
⊢ s *
      circleIntegral
        ((fun z => w ^ n / (z - c) ^ n * ((z - c)⁻¹ * f z)) - fun z => w ^ n / (z - c) ^ n * ((z - c)⁻¹ * g z)) c ↑r =
    s * ∮ (z : ℂ) in C(c, ↑r), w ^ n / (z - c) ^ n * ((z - c)⁻¹ * (f z - g z))
Theorem: cauchy_sub
Proof state before:
f g : ℂ → ℂ
c : ℂ
r : ℝ≥0
n : ℕ
w : ℂ
s : ℂ := (2 * ↑π * I)⁻¹
⊢ s *
      circleIntegral
        ((fun z => w ^ n / (z - c) ^ n * ((z - c)⁻¹ * f z)) - fun z => w ^ n / (z - c) ^ n * ((z - c)⁻¹ * g z)) c ↑r =
    s * ∮ (z : ℂ) in C(c, ↑r), w ^ n / (z - c) ^ n * ((z - c)⁻¹ * (f z - g z))
Tactic:
have flip :
  ((fun z ↦ w ^ n / (z - c) ^ n * ((z - c)⁻¹ * f z)) - fun z ↦
      w ^ n / (z - c) ^ n * ((z - c)⁻¹ * g z)) =
    fun z ↦ w ^ n / (z - c) ^ n * ((z - c)⁻¹ * f z) - w ^ n / (z - c) ^ n * ((z - c)⁻¹ * g z) :=
  rfl
Proof state after:
f g : ℂ → ℂ
c : ℂ
r : ℝ≥0
n : ℕ
w : ℂ
s : ℂ := (2 * ↑π * I)⁻¹
flip :
  ((fun z => w ^ n / (z - c) ^ n * ((z - c)⁻¹ * f z)) - fun z => w ^ n / (z - c) ^ n * ((z - c)⁻¹ * g z)) = fun z =>
    w ^ n / (z - c) ^ n * ((z - c)⁻¹ * f z) - w ^ n / (z - c) ^ n * ((z - c)⁻¹ * g z)
⊢ s *
      circleIntegral
        ((fun z => w ^ n / (z - c) ^ n * ((z - c)⁻¹ * f z)) - fun z => w ^ n / (z - c) ^ n * ((z - c)⁻¹ * g z)) c ↑r =
    s * ∮ (z : ℂ) in C(c, ↑r), w ^ n / (z - c) ^ n * ((z - c)⁻¹ * (f z - g z))
Theorem: cauchy_sub
Proof state before:
f g : ℂ → ℂ
c : ℂ
r : ℝ≥0
n : ℕ
w : ℂ
s : ℂ := (2 * ↑π * I)⁻¹
flip :
  ((fun z => w ^ n / (z - c) ^ n * ((z - c)⁻¹ * f z)) - fun z => w ^ n / (z - c) ^ n * ((z - c)⁻¹ * g z)) = fun z =>
    w ^ n / (z - c) ^ n * ((z - c)⁻¹ * f z) - w ^ n / (z - c) ^ n * ((z - c)⁻¹ * g z)
⊢ s *
      circleIntegral
        ((fun z => w ^ n / (z - c) ^ n * ((z - c)⁻¹ * f z)) - fun z => w ^ n / (z - c) ^ n * ((z - c)⁻¹ * g z)) c ↑r =
    s * ∮ (z : ℂ) in C(c, ↑r), w ^ n / (z - c) ^ n * ((z - c)⁻¹ * (f z - g z))
Tactic:
simp only [flip, mul_sub_left_distrib]
Proof state after:
no goals
Theorem: cauchy_dist
Proof state before:
f g : ℂ → ℂ
c : ℂ
r d : ℝ≥0
n : ℕ
w : ℂ
rp : r > 0
cf : ContinuousOn f (closedBall c ↑r)
cg : ContinuousOn g (closedBall c ↑r)
h : ∀ z ∈ closedBall c ↑r, Complex.abs (f z - g z) ≤ ↑d
⊢ dist ((cauchyPowerSeries f c (↑r) n) fun x => w) ((cauchyPowerSeries g c (↑r) n) fun x => w) ≤
    Complex.abs w ^ n * ↑r⁻¹ ^ n * ↑d
Tactic:
rw [Complex.dist_eq, cauchy_sub n w rp cf cg]
Proof state after:
f g : ℂ → ℂ
c : ℂ
r d : ℝ≥0
n : ℕ
w : ℂ
rp : r > 0
cf : ContinuousOn f (closedBall c ↑r)
cg : ContinuousOn g (closedBall c ↑r)
h : ∀ z ∈ closedBall c ↑r, Complex.abs (f z - g z) ≤ ↑d
⊢ Complex.abs ((cauchyPowerSeries (f - g) c (↑r) n) fun x => w) ≤ Complex.abs w ^ n * ↑r⁻¹ ^ n * ↑d
Theorem: cauchy_dist
Proof state before:
f g : ℂ → ℂ
c : ℂ
r d : ℝ≥0
n : ℕ
w : ℂ
rp : r > 0
cf : ContinuousOn f (closedBall c ↑r)
cg : ContinuousOn g (closedBall c ↑r)
h : ∀ z ∈ closedBall c ↑r, Complex.abs (f z - g z) ≤ ↑d
⊢ Complex.abs ((cauchyPowerSeries (f - g) c (↑r) n) fun x => w) ≤ Complex.abs w ^ n * ↑r⁻¹ ^ n * ↑d
Tactic:
refine cauchy_bound rp ?_
Proof state after:
f g : ℂ → ℂ
c : ℂ
r d : ℝ≥0
n : ℕ
w : ℂ
rp : r > 0
cf : ContinuousOn f (closedBall c ↑r)
cg : ContinuousOn g (closedBall c ↑r)
h : ∀ z ∈ closedBall c ↑r, Complex.abs (f z - g z) ≤ ↑d
⊢ ∀ w ∈ closedBall c ↑r, Complex.abs ((f - g) w) ≤ ↑d
Theorem: cauchy_dist
Proof state before:
f g : ℂ → ℂ
c : ℂ
r d : ℝ≥0
n : ℕ
w : ℂ
rp : r > 0
cf : ContinuousOn f (closedBall c ↑r)
cg : ContinuousOn g (closedBall c ↑r)
h : ∀ z ∈ closedBall c ↑r, Complex.abs (f z - g z) ≤ ↑d
⊢ ∀ w ∈ closedBall c ↑r, Complex.abs ((f - g) w) ≤ ↑d
Tactic:
intro z zr
Proof state after:
f g : ℂ → ℂ
c : ℂ
r d : ℝ≥0
n : ℕ
w : ℂ
rp : r > 0
cf : ContinuousOn f (closedBall c ↑r)
cg : ContinuousOn g (closedBall c ↑r)
h : ∀ z ∈ closedBall c ↑r, Complex.abs (f z - g z) ≤ ↑d
z : ℂ
zr : z ∈ closedBall c ↑r
⊢ Complex.abs ((f - g) z) ≤ ↑d
Theorem: cauchy_dist
Proof state before:
f g : ℂ → ℂ
c : ℂ
r d : ℝ≥0
n : ℕ
w : ℂ
rp : r > 0
cf : ContinuousOn f (closedBall c ↑r)
cg : ContinuousOn g (closedBall c ↑r)
h : ∀ z ∈ closedBall c ↑r, Complex.abs (f z - g z) ≤ ↑d
z : ℂ
zr : z ∈ closedBall c ↑r
⊢ Complex.abs ((f - g) z) ≤ ↑d
Tactic:
simp at h zr
Proof state after:
f g : ℂ → ℂ
c : ℂ
r d : ℝ≥0
n : ℕ
w : ℂ
rp : r > 0
cf : ContinuousOn f (closedBall c ↑r)
cg : ContinuousOn g (closedBall c ↑r)
z : ℂ
h : ∀ (z : ℂ), nndist z c ≤ r → Complex.abs (f z - g z) ≤ ↑d
zr : nndist z c ≤ r
⊢ Complex.abs ((f - g) z) ≤ ↑d
Theorem: cauchy_dist
Proof state before:
f g : ℂ → ℂ
c : ℂ
r d : ℝ≥0
n : ℕ
w : ℂ
rp : r > 0
cf : ContinuousOn f (closedBall c ↑r)
cg : ContinuousOn g (closedBall c ↑r)
z : ℂ
h : ∀ (z : ℂ), nndist z c ≤ r → Complex.abs (f z - g z) ≤ ↑d
zr : nndist z c ≤ r
⊢ Complex.abs ((f - g) z) ≤ ↑d
Tactic:
refine h z zr
Proof state after:
no goals
Theorem: uniform_analytic_lim
Proof state before:
I : Type
inst✝¹ : Lattice I
inst✝ : Nonempty I
f : I → ℂ → ℂ
g : ℂ → ℂ
s : Set ℂ
o : IsOpen s
h : ∀ (n : I), AnalyticOn ℂ (f n) s
u : TendstoUniformlyOn f g atTop s
⊢ AnalyticOn ℂ g s
Tactic:
intro c hc
Proof state after:
I : Type
inst✝¹ : Lattice I
inst✝ : Nonempty I
f : I → ℂ → ℂ
g : ℂ → ℂ
s : Set ℂ
o : IsOpen s
h : ∀ (n : I), AnalyticOn ℂ (f n) s
u : TendstoUniformlyOn f g atTop s
c : ℂ
hc : c ∈ s
⊢ AnalyticAt ℂ g c
Theorem: uniform_analytic_lim
Proof state before:
I : Type
inst✝¹ : Lattice I
inst✝ : Nonempty I
f : I → ℂ → ℂ
g : ℂ → ℂ
s : Set ℂ
o : IsOpen s
h : ∀ (n : I), AnalyticOn ℂ (f n) s
u : TendstoUniformlyOn f g atTop s
c : ℂ
hc : c ∈ s
⊢ AnalyticAt ℂ g c
Tactic:
rcases Metric.nhds_basis_closedBall.mem_iff.mp (o.mem_nhds hc) with ⟨r, rp, cb⟩
Proof state after:
case intro.intro
I : Type
inst✝¹ : Lattice I
inst✝ : Nonempty I
f : I → ℂ → ℂ
g : ℂ → ℂ
s : Set ℂ
o : IsOpen s
h : ∀ (n : I), AnalyticOn ℂ (f n) s
u : TendstoUniformlyOn f g atTop s
c : ℂ
hc : c ∈ s
r : ℝ
rp : 0 < r
cb : closedBall c r ⊆ s
⊢ AnalyticAt ℂ g c
Theorem: uniform_analytic_lim
Proof state before:
case intro.intro
I : Type
inst✝¹ : Lattice I
inst✝ : Nonempty I
f : I → ℂ → ℂ
g : ℂ → ℂ
s : Set ℂ
o : IsOpen s
h : ∀ (n : I), AnalyticOn ℂ (f n) s
u : TendstoUniformlyOn f g atTop s
c : ℂ
hc : c ∈ s
r : ℝ
rp : 0 < r
cb : closedBall c r ⊆ s
⊢ AnalyticAt ℂ g c
Tactic:
lift r to ℝ≥0 using rp.le
Proof state after:
case intro.intro.intro
I : Type
inst✝¹ : Lattice I
inst✝ : Nonempty I
f : I → ℂ → ℂ
g : ℂ → ℂ
s : Set ℂ
o : IsOpen s
h : ∀ (n : I), AnalyticOn ℂ (f n) s
u : TendstoUniformlyOn f g atTop s
c : ℂ
hc : c ∈ s
r : ℝ≥0
rp : 0 < ↑r
cb : closedBall c ↑r ⊆ s
⊢ AnalyticAt ℂ g c
Theorem: uniform_analytic_lim
Proof state before:
case intro.intro.intro
I : Type
inst✝¹ : Lattice I
inst✝ : Nonempty I
f : I → ℂ → ℂ
g : ℂ → ℂ
s : Set ℂ
o : IsOpen s
h : ∀ (n : I), AnalyticOn ℂ (f n) s
u : TendstoUniformlyOn f g atTop s
c : ℂ
hc : c ∈ s
r : ℝ≥0
rp : 0 < ↑r
cb : closedBall c ↑r ⊆ s
⊢ AnalyticAt ℂ g c
Tactic:
simp only [NNReal.coe_pos] at rp
Proof state after:
case intro.intro.intro
I : Type
inst✝¹ : Lattice I
inst✝ : Nonempty I
f : I → ℂ → ℂ
g : ℂ → ℂ
s : Set ℂ
o : IsOpen s
h : ∀ (n : I), AnalyticOn ℂ (f n) s
u : TendstoUniformlyOn f g atTop s
c : ℂ
hc : c ∈ s
r : ℝ≥0
cb : closedBall c ↑r ⊆ s
rp : 0 < r
⊢ AnalyticAt ℂ g c
Theorem: uniform_analytic_lim
Proof state before:
case intro.intro.intro
I : Type
inst✝¹ : Lattice I
inst✝ : Nonempty I
f : I → ℂ → ℂ
g : ℂ → ℂ
s : Set ℂ
o : IsOpen s
h : ∀ (n : I), AnalyticOn ℂ (f n) s
u : TendstoUniformlyOn f g atTop s
c : ℂ
hc : c ∈ s
r : ℝ≥0
cb : closedBall c ↑r ⊆ s
rp : 0 < r
⊢ AnalyticAt ℂ g c
Tactic:
have hb : ∀ n, AnalyticOn ℂ (f n) (closedBall c r) := fun n ↦ (h n).mono cb
Proof state after:
case intro.intro.intro
I : Type
inst✝¹ : Lattice I
inst✝ : Nonempty I
f : I → ℂ → ℂ
g : ℂ → ℂ
s : Set ℂ
o : IsOpen s
h : ∀ (n : I), AnalyticOn ℂ (f n) s
u : TendstoUniformlyOn f g atTop s
c : ℂ
hc : c ∈ s
r : ℝ≥0
cb : closedBall c ↑r ⊆ s
rp : 0 < r
hb : ∀ (n : I), AnalyticOn ℂ (f n) (closedBall c ↑r)
⊢ AnalyticAt ℂ g c
Theorem: uniform_analytic_lim
Proof state before:
case intro.intro.intro
I : Type
inst✝¹ : Lattice I
inst✝ : Nonempty I
f : I → ℂ → ℂ
g : ℂ → ℂ
s : Set ℂ
o : IsOpen s
h : ∀ (n : I), AnalyticOn ℂ (f n) s
u : TendstoUniformlyOn f g atTop s
c : ℂ
hc : c ∈ s
r : ℝ≥0
cb : closedBall c ↑r ⊆ s
rp : 0 < r
hb : ∀ (n : I), AnalyticOn ℂ (f n) (closedBall c ↑r)
⊢ AnalyticAt ℂ g c
Tactic:
set pr := fun n ↦ cauchyPowerSeries (f n) c r
Proof state after:
case intro.intro.intro
I : Type
inst✝¹ : Lattice I
inst✝ : Nonempty I
f : I → ℂ → ℂ
g : ℂ → ℂ
s : Set ℂ
o : IsOpen s
h : ∀ (n : I), AnalyticOn ℂ (f n) s
u : TendstoUniformlyOn f g atTop s
c : ℂ
hc : c ∈ s
r : ℝ≥0
cb : closedBall c ↑r ⊆ s
rp : 0 < r
hb : ∀ (n : I), AnalyticOn ℂ (f n) (closedBall c ↑r)
pr : I → FormalMultilinearSeries ℂ ℂ ℂ := fun n => cauchyPowerSeries (f n) c ↑r
⊢ AnalyticAt ℂ g c
Theorem: uniform_analytic_lim
Proof state before:
case intro.intro.intro
I : Type
inst✝¹ : Lattice I
inst✝ : Nonempty I
f : I → ℂ → ℂ
g : ℂ → ℂ
s : Set ℂ
o : IsOpen s
h : ∀ (n : I), AnalyticOn ℂ (f n) s
u : TendstoUniformlyOn f g atTop s
c : ℂ
hc : c ∈ s
r : ℝ≥0
cb : closedBall c ↑r ⊆ s
rp : 0 < r
hb : ∀ (n : I), AnalyticOn ℂ (f n) (closedBall c ↑r)
pr : I → FormalMultilinearSeries ℂ ℂ ℂ := fun n => cauchyPowerSeries (f n) c ↑r
⊢ AnalyticAt ℂ g c
Tactic:
have hpf : ∀ n, HasFPowerSeriesOnBall (f n) (pr n) c r := by
  intro n
  have cs := cauchy_on_cball_radius rp (hb n)
  have pn : pr n = cauchyPowerSeries (f n) c r := rfl
  rw [← pn] at cs; exact cs
Proof state after:
case intro.intro.intro
I : Type
inst✝¹ : Lattice I
inst✝ : Nonempty I
f : I → ℂ → ℂ
g : ℂ → ℂ
s : Set ℂ
o : IsOpen s
h : ∀ (n : I), AnalyticOn ℂ (f n) s
u : TendstoUniformlyOn f g atTop s
c : ℂ
hc : c ∈ s
r : ℝ≥0
cb : closedBall c ↑r ⊆ s
rp : 0 < r
hb : ∀ (n : I), AnalyticOn ℂ (f n) (closedBall c ↑r)
pr : I → FormalMultilinearSeries ℂ ℂ ℂ := fun n => cauchyPowerSeries (f n) c ↑r
hpf : ∀ (n : I), HasFPowerSeriesOnBall (f n) (pr n) c ↑r
⊢ AnalyticAt ℂ g c
Theorem: uniform_analytic_lim
Proof state before:
case intro.intro.intro
I : Type
inst✝¹ : Lattice I
inst✝ : Nonempty I
f : I → ℂ → ℂ
g : ℂ → ℂ
s : Set ℂ
o : IsOpen s
h : ∀ (n : I), AnalyticOn ℂ (f n) s
u : TendstoUniformlyOn f g atTop s
c : ℂ
hc : c ∈ s
r : ℝ≥0
cb : closedBall c ↑r ⊆ s
rp : 0 < r
hb : ∀ (n : I), AnalyticOn ℂ (f n) (closedBall c ↑r)
pr : I → FormalMultilinearSeries ℂ ℂ ℂ := fun n => cauchyPowerSeries (f n) c ↑r
hpf : ∀ (n : I), HasFPowerSeriesOnBall (f n) (pr n) c ↑r
⊢ AnalyticAt ℂ g c
Tactic:
have cfs : ∀ n, ContinuousOn (f n) s := fun n ↦ AnalyticOn.continuousOn (h n)
Proof state after:
case intro.intro.intro
I : Type
inst✝¹ : Lattice I
inst✝ : Nonempty I
f : I → ℂ → ℂ
g : ℂ → ℂ
s : Set ℂ
o : IsOpen s
h : ∀ (n : I), AnalyticOn ℂ (f n) s
u : TendstoUniformlyOn f g atTop s
c : ℂ
hc : c ∈ s
r : ℝ≥0
cb : closedBall c ↑r ⊆ s
rp : 0 < r
hb : ∀ (n : I), AnalyticOn ℂ (f n) (closedBall c ↑r)
pr : I → FormalMultilinearSeries ℂ ℂ ℂ := fun n => cauchyPowerSeries (f n) c ↑r
hpf : ∀ (n : I), HasFPowerSeriesOnBall (f n) (pr n) c ↑r
cfs : ∀ (n : I), ContinuousOn (f n) s
⊢ AnalyticAt ℂ g c
Theorem: uniform_analytic_lim
Proof state before:
case intro.intro.intro
I : Type
inst✝¹ : Lattice I
inst✝ : Nonempty I
f : I → ℂ → ℂ
g : ℂ → ℂ
s : Set ℂ
o : IsOpen s
h : ∀ (n : I), AnalyticOn ℂ (f n) s
u : TendstoUniformlyOn f g atTop s
c : ℂ
hc : c ∈ s
r : ℝ≥0
cb : closedBall c ↑r ⊆ s
rp : 0 < r
hb : ∀ (n : I), AnalyticOn ℂ (f n) (closedBall c ↑r)
pr : I → FormalMultilinearSeries ℂ ℂ ℂ := fun n => cauchyPowerSeries (f n) c ↑r
hpf : ∀ (n : I), HasFPowerSeriesOnBall (f n) (pr n) c ↑r
cfs : ∀ (n : I), ContinuousOn (f n) s
⊢ AnalyticAt ℂ g c
Tactic:
have cf : ∀ n, ContinuousOn (f n) (closedBall c r) := fun n ↦ ContinuousOn.mono (cfs n) cb
Proof state after:
case intro.intro.intro
I : Type
inst✝¹ : Lattice I
inst✝ : Nonempty I
f : I → ℂ → ℂ
g : ℂ → ℂ
s : Set ℂ
o : IsOpen s
h : ∀ (n : I), AnalyticOn ℂ (f n) s
u : TendstoUniformlyOn f g atTop s
c : ℂ
hc : c ∈ s
r : ℝ≥0
cb : closedBall c ↑r ⊆ s
rp : 0 < r
hb : ∀ (n : I), AnalyticOn ℂ (f n) (closedBall c ↑r)
pr : I → FormalMultilinearSeries ℂ ℂ ℂ := fun n => cauchyPowerSeries (f n) c ↑r
hpf : ∀ (n : I), HasFPowerSeriesOnBall (f n) (pr n) c ↑r
cfs : ∀ (n : I), ContinuousOn (f n) s
cf : ∀ (n : I), ContinuousOn (f n) (closedBall c ↑r)
⊢ AnalyticAt ℂ g c
Theorem: uniform_analytic_lim
Proof state before:
case intro.intro.intro
I : Type
inst✝¹ : Lattice I
inst✝ : Nonempty I
f : I → ℂ → ℂ
g : ℂ → ℂ
s : Set ℂ
o : IsOpen s
h : ∀ (n : I), AnalyticOn ℂ (f n) s
u : TendstoUniformlyOn f g atTop s
c : ℂ
hc : c ∈ s
r : ℝ≥0
cb : closedBall c ↑r ⊆ s
rp : 0 < r
hb : ∀ (n : I), AnalyticOn ℂ (f n) (closedBall c ↑r)
pr : I → FormalMultilinearSeries ℂ ℂ ℂ := fun n => cauchyPowerSeries (f n) c ↑r
hpf : ∀ (n : I), HasFPowerSeriesOnBall (f n) (pr n) c ↑r
cfs : ∀ (n : I), ContinuousOn (f n) s
cf : ∀ (n : I), ContinuousOn (f n) (closedBall c ↑r)
⊢ AnalyticAt ℂ g c
Tactic:
have cg : ContinuousOn g (closedBall c r) :=
  ContinuousOn.mono (TendstoUniformlyOn.continuousOn u (Filter.eventually_of_forall cfs)) cb
Proof state after:
case intro.intro.intro
I : Type
inst✝¹ : Lattice I
inst✝ : Nonempty I
f : I → ℂ → ℂ
g : ℂ → ℂ
s : Set ℂ
o : IsOpen s
h : ∀ (n : I), AnalyticOn ℂ (f n) s
u : TendstoUniformlyOn f g atTop s
c : ℂ
hc : c ∈ s
r : ℝ≥0
cb : closedBall c ↑r ⊆ s
rp : 0 < r
hb : ∀ (n : I), AnalyticOn ℂ (f n) (closedBall c ↑r)
pr : I → FormalMultilinearSeries ℂ ℂ ℂ := fun n => cauchyPowerSeries (f n) c ↑r
hpf : ∀ (n : I), HasFPowerSeriesOnBall (f n) (pr n) c ↑r
cfs : ∀ (n : I), ContinuousOn (f n) s
cf : ∀ (n : I), ContinuousOn (f n) (closedBall c ↑r)
cg : ContinuousOn g (closedBall c ↑r)
⊢ AnalyticAt ℂ g c
Theorem: uniform_analytic_lim
Proof state before:
case intro.intro.intro
I : Type
inst✝¹ : Lattice I
inst✝ : Nonempty I
f : I → ℂ → ℂ
g : ℂ → ℂ
s : Set ℂ
o : IsOpen s
h : ∀ (n : I), AnalyticOn ℂ (f n) s
u : TendstoUniformlyOn f g atTop s
c : ℂ
hc : c ∈ s
r : ℝ≥0
cb : closedBall c ↑r ⊆ s
rp : 0 < r
hb : ∀ (n : I), AnalyticOn ℂ (f n) (closedBall c ↑r)
pr : I → FormalMultilinearSeries ℂ ℂ ℂ := fun n => cauchyPowerSeries (f n) c ↑r
hpf : ∀ (n : I), HasFPowerSeriesOnBall (f n) (pr n) c ↑r
cfs : ∀ (n : I), ContinuousOn (f n) s
cf : ∀ (n : I), ContinuousOn (f n) (closedBall c ↑r)
cg : ContinuousOn g (closedBall c ↑r)
⊢ AnalyticAt ℂ g c
Tactic:
clear h hb hc o cfs
Proof state after:
case intro.intro.intro
I : Type
inst✝¹ : Lattice I
inst✝ : Nonempty I
f : I → ℂ → ℂ
g : ℂ → ℂ
s : Set ℂ
u : TendstoUniformlyOn f g atTop s
c : ℂ
r : ℝ≥0
cb : closedBall c ↑r ⊆ s
rp : 0 < r
pr : I → FormalMultilinearSeries ℂ ℂ ℂ := fun n => cauchyPowerSeries (f n) c ↑r
hpf : ∀ (n : I), HasFPowerSeriesOnBall (f n) (pr n) c ↑r
cf : ∀ (n : I), ContinuousOn (f n) (closedBall c ↑r)
cg : ContinuousOn g (closedBall c ↑r)
⊢ AnalyticAt ℂ g c
Theorem: uniform_analytic_lim
Proof state before:
case intro.intro.intro
I : Type
inst✝¹ : Lattice I
inst✝ : Nonempty I
f : I → ℂ → ℂ
g : ℂ → ℂ
s : Set ℂ
u : TendstoUniformlyOn f g atTop s
c : ℂ
r : ℝ≥0
cb : closedBall c ↑r ⊆ s
rp : 0 < r
pr : I → FormalMultilinearSeries ℂ ℂ ℂ := fun n => cauchyPowerSeries (f n) c ↑r
hpf : ∀ (n : I), HasFPowerSeriesOnBall (f n) (pr n) c ↑r
cf : ∀ (n : I), ContinuousOn (f n) (closedBall c ↑r)
cg : ContinuousOn g (closedBall c ↑r)
⊢ AnalyticAt ℂ g c
Tactic:
set p := cauchyPowerSeries g c r
Proof state after:
case intro.intro.intro
I : Type
inst✝¹ : Lattice I
inst✝ : Nonempty I
f : I → ℂ → ℂ
g : ℂ → ℂ
s : Set ℂ
u : TendstoUniformlyOn f g atTop s
c : ℂ
r : ℝ≥0
cb : closedBall c ↑r ⊆ s
rp : 0 < r
pr : I → FormalMultilinearSeries ℂ ℂ ℂ := fun n => cauchyPowerSeries (f n) c ↑r
hpf : ∀ (n : I), HasFPowerSeriesOnBall (f n) (pr n) c ↑r
cf : ∀ (n : I), ContinuousOn (f n) (closedBall c ↑r)
cg : ContinuousOn g (closedBall c ↑r)
p : FormalMultilinearSeries ℂ ℂ ℂ := cauchyPowerSeries g c ↑r
⊢ AnalyticAt ℂ g c