Theorem: series2Coeff_bound (Ray/Hartogs/Osgood.lean)

State before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r b : ℝ
h : Separate f c0 c1 r b s
n0 n1 : ℕ
⊢ ‖h.series2Coeff n0 n1‖ ≤ b * r⁻¹ ^ (n0 + n1)
Tactic:
have inner_c :
  ContinuousOn
    (fun z0 ↦ (2 * π * I : ℂ)⁻¹ • ∮ z1 in C(c1, r), (z1 - c1)⁻¹ ^ n1 • (z1 - c1)⁻¹ • f (z0, z1))
    (sphere c0 r) :=
  ContinuousOn.smul continuousOn_const (ContinuousOn.cauchy1 h.rp (ContinuousOn.mono h.fc h.rs'))
State after:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r b : ℝ
h : Separate f c0 c1 r b s
n0 n1 : ℕ
inner_c :
  ContinuousOn (fun z0 => (2 * ↑π * I)⁻¹ • ∮ (z1 : ℂ) in C(c1, r), (z1 - c1)⁻¹ ^ n1 • (z1 - c1)⁻¹ • f (z0, z1))
    (sphere c0 r)
⊢ ‖h.series2Coeff n0 n1‖ ≤ b * r⁻¹ ^ (n0 + n1)

State before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r b : ℝ
h : Separate f c0 c1 r b s
n0 n1 : ℕ
inner_c :
  ContinuousOn (fun z0 => (2 * ↑π * I)⁻¹ • ∮ (z1 : ℂ) in C(c1, r), (z1 - c1)⁻¹ ^ n1 • (z1 - c1)⁻¹ • f (z0, z1))
    (sphere c0 r)
⊢ ‖h.series2Coeff n0 n1‖ ≤ b * r⁻¹ ^ (n0 + n1)
Tactic:
have inner_b : ∀ z0 _, ‖(2*π*I : ℂ)⁻¹ • ∮ z1 in C(c1, r),
    (z1 - c1)⁻¹ ^ n1 • (z1 - c1)⁻¹ • f (z0,z1)‖ ≤ b * r⁻¹ ^ n1 :=
  fun z0 z0s ↦ cauchy1_bound' h.rp b
    (ContinuousOn.mono (h.fc1 (mem_sphere_closed z0s)) Metric.sphere_subset_closedBall)
    (fun z1 ↦ h.fb z0s) n1
State after:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r b : ℝ
h : Separate f c0 c1 r b s
n0 n1 : ℕ
inner_c :
  ContinuousOn (fun z0 => (2 * ↑π * I)⁻¹ • ∮ (z1 : ℂ) in C(c1, r), (z1 - c1)⁻¹ ^ n1 • (z1 - c1)⁻¹ • f (z0, z1))
    (sphere c0 r)
inner_b :
  ∀ z0 ∈ sphere c0 r,
    ‖(2 * ↑π * I)⁻¹ • ∮ (z1 : ℂ) in C(c1, r), (z1 - c1)⁻¹ ^ n1 • (z1 - c1)⁻¹ • f (z0, z1)‖ ≤ b * r⁻¹ ^ n1
⊢ ‖h.series2Coeff n0 n1‖ ≤ b * r⁻¹ ^ (n0 + n1)

State before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r b : ℝ
h : Separate f c0 c1 r b s
n0 n1 : ℕ
inner_c :
  ContinuousOn (fun z0 => (2 * ↑π * I)⁻¹ • ∮ (z1 : ℂ) in C(c1, r), (z1 - c1)⁻¹ ^ n1 • (z1 - c1)⁻¹ • f (z0, z1))
    (sphere c0 r)
inner_b :
  ∀ z0 ∈ sphere c0 r,
    ‖(2 * ↑π * I)⁻¹ • ∮ (z1 : ℂ) in C(c1, r), (z1 - c1)⁻¹ ^ n1 • (z1 - c1)⁻¹ • f (z0, z1)‖ ≤ b * r⁻¹ ^ n1
⊢ ‖h.series2Coeff n0 n1‖ ≤ b * r⁻¹ ^ (n0 + n1)
Tactic:
have outer := cauchy1_bound' h.rp _ inner_c inner_b n0
State after:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r b : ℝ
h : Separate f c0 c1 r b s
n0 n1 : ℕ
inner_c :
  ContinuousOn (fun z0 => (2 * ↑π * I)⁻¹ • ∮ (z1 : ℂ) in C(c1, r), (z1 - c1)⁻¹ ^ n1 • (z1 - c1)⁻¹ • f (z0, z1))
    (sphere c0 r)
inner_b :
  ∀ z0 ∈ sphere c0 r,
    ‖(2 * ↑π * I)⁻¹ • ∮ (z1 : ℂ) in C(c1, r), (z1 - c1)⁻¹ ^ n1 • (z1 - c1)⁻¹ • f (z0, z1)‖ ≤ b * r⁻¹ ^ n1
outer :
  ‖(2 * ↑π * I)⁻¹ •
        ∮ (z : ℂ) in C(c0, r),
          (z - c0)⁻¹ ^ n0 •
            (z - c0)⁻¹ • (2 * ↑π * I)⁻¹ • ∮ (z1 : ℂ) in C(c1, r), (z1 - c1)⁻¹ ^ n1 • (z1 - c1)⁻¹ • f (z, z1)‖ ≤
    b * r⁻¹ ^ n1 * r⁻¹ ^ n0
⊢ ‖h.series2Coeff n0 n1‖ ≤ b * r⁻¹ ^ (n0 + n1)

State before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r b : ℝ
h : Separate f c0 c1 r b s
n0 n1 : ℕ
inner_c :
  ContinuousOn (fun z0 => (2 * ↑π * I)⁻¹ • ∮ (z1 : ℂ) in C(c1, r), (z1 - c1)⁻¹ ^ n1 • (z1 - c1)⁻¹ • f (z0, z1))
    (sphere c0 r)
inner_b :
  ∀ z0 ∈ sphere c0 r,
    ‖(2 * ↑π * I)⁻¹ • ∮ (z1 : ℂ) in C(c1, r), (z1 - c1)⁻¹ ^ n1 • (z1 - c1)⁻¹ • f (z0, z1)‖ ≤ b * r⁻¹ ^ n1
outer :
  ‖(2 * ↑π * I)⁻¹ •
        ∮ (z : ℂ) in C(c0, r),
          (z - c0)⁻¹ ^ n0 •
            (z - c0)⁻¹ • (2 * ↑π * I)⁻¹ • ∮ (z1 : ℂ) in C(c1, r), (z1 - c1)⁻¹ ^ n1 • (z1 - c1)⁻¹ • f (z, z1)‖ ≤
    b * r⁻¹ ^ n1 * r⁻¹ ^ n0
⊢ ‖h.series2Coeff n0 n1‖ ≤ b * r⁻¹ ^ (n0 + n1)
Tactic:
have e : b * r⁻¹ ^ n1 * r⁻¹ ^ n0 = b * r⁻¹ ^ (n0 + n1) := by
  rw [mul_assoc, ← pow_add, add_comm n0 _]
State after:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r b : ℝ
h : Separate f c0 c1 r b s
n0 n1 : ℕ
inner_c :
  ContinuousOn (fun z0 => (2 * ↑π * I)⁻¹ • ∮ (z1 : ℂ) in C(c1, r), (z1 - c1)⁻¹ ^ n1 • (z1 - c1)⁻¹ • f (z0, z1))
    (sphere c0 r)
inner_b :
  ∀ z0 ∈ sphere c0 r,
    ‖(2 * ↑π * I)⁻¹ • ∮ (z1 : ℂ) in C(c1, r), (z1 - c1)⁻¹ ^ n1 • (z1 - c1)⁻¹ • f (z0, z1)‖ ≤ b * r⁻¹ ^ n1
outer :
  ‖(2 * ↑π * I)⁻¹ •
        ∮ (z : ℂ) in C(c0, r),
          (z - c0)⁻¹ ^ n0 •
            (z - c0)⁻¹ • (2 * ↑π * I)⁻¹ • ∮ (z1 : ℂ) in C(c1, r), (z1 - c1)⁻¹ ^ n1 • (z1 - c1)⁻¹ • f (z, z1)‖ ≤
    b * r⁻¹ ^ n1 * r⁻¹ ^ n0
e : b * r⁻¹ ^ n1 * r⁻¹ ^ n0 = b * r⁻¹ ^ (n0 + n1)
⊢ ‖h.series2Coeff n0 n1‖ ≤ b * r⁻¹ ^ (n0 + n1)

State before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r b : ℝ
h : Separate f c0 c1 r b s
n0 n1 : ℕ
inner_c :
  ContinuousOn (fun z0 => (2 * ↑π * I)⁻¹ • ∮ (z1 : ℂ) in C(c1, r), (z1 - c1)⁻¹ ^ n1 • (z1 - c1)⁻¹ • f (z0, z1))
    (sphere c0 r)
inner_b :
  ∀ z0 ∈ sphere c0 r,
    ‖(2 * ↑π * I)⁻¹ • ∮ (z1 : ℂ) in C(c1, r), (z1 - c1)⁻¹ ^ n1 • (z1 - c1)⁻¹ • f (z0, z1)‖ ≤ b * r⁻¹ ^ n1
outer :
  ‖(2 * ↑π * I)⁻¹ •
        ∮ (z : ℂ) in C(c0, r),
          (z - c0)⁻¹ ^ n0 •
            (z - c0)⁻¹ • (2 * ↑π * I)⁻¹ • ∮ (z1 : ℂ) in C(c1, r), (z1 - c1)⁻¹ ^ n1 • (z1 - c1)⁻¹ • f (z, z1)‖ ≤
    b * r⁻¹ ^ n1 * r⁻¹ ^ n0
e : b * r⁻¹ ^ n1 * r⁻¹ ^ n0 = b * r⁻¹ ^ (n0 + n1)
⊢ ‖h.series2Coeff n0 n1‖ ≤ b * r⁻¹ ^ (n0 + n1)
Tactic:
rw [Separate.series2Coeff]
State after:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r b : ℝ
h : Separate f c0 c1 r b s
n0 n1 : ℕ
inner_c :
  ContinuousOn (fun z0 => (2 * ↑π * I)⁻¹ • ∮ (z1 : ℂ) in C(c1, r), (z1 - c1)⁻¹ ^ n1 • (z1 - c1)⁻¹ • f (z0, z1))
    (sphere c0 r)
inner_b :
  ∀ z0 ∈ sphere c0 r,
    ‖(2 * ↑π * I)⁻¹ • ∮ (z1 : ℂ) in C(c1, r), (z1 - c1)⁻¹ ^ n1 • (z1 - c1)⁻¹ • f (z0, z1)‖ ≤ b * r⁻¹ ^ n1
outer :
  ‖(2 * ↑π * I)⁻¹ •
        ∮ (z : ℂ) in C(c0, r),
          (z - c0)⁻¹ ^ n0 •
            (z - c0)⁻¹ • (2 * ↑π * I)⁻¹ • ∮ (z1 : ℂ) in C(c1, r), (z1 - c1)⁻¹ ^ n1 • (z1 - c1)⁻¹ • f (z, z1)‖ ≤
    b * r⁻¹ ^ n1 * r⁻¹ ^ n0
e : b * r⁻¹ ^ n1 * r⁻¹ ^ n0 = b * r⁻¹ ^ (n0 + n1)
⊢ ‖(2 * ↑π * I)⁻¹ •
        ∮ (z0 : ℂ) in C(c0, r),
          (z0 - c0)⁻¹ ^ n0 •
            (z0 - c0)⁻¹ • (2 * ↑π * I)⁻¹ • ∮ (z1 : ℂ) in C(c1, r), (z1 - c1)⁻¹ ^ n1 • (z1 - c1)⁻¹ • f (z0, z1)‖ ≤
    b * r⁻¹ ^ (n0 + n1)

State before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r b : ℝ
h : Separate f c0 c1 r b s
n0 n1 : ℕ
inner_c :
  ContinuousOn (fun z0 => (2 * ↑π * I)⁻¹ • ∮ (z1 : ℂ) in C(c1, r), (z1 - c1)⁻¹ ^ n1 • (z1 - c1)⁻¹ • f (z0, z1))
    (sphere c0 r)
inner_b :
  ∀ z0 ∈ sphere c0 r,
    ‖(2 * ↑π * I)⁻¹ • ∮ (z1 : ℂ) in C(c1, r), (z1 - c1)⁻¹ ^ n1 • (z1 - c1)⁻¹ • f (z0, z1)‖ ≤ b * r⁻¹ ^ n1
outer :
  ‖(2 * ↑π * I)⁻¹ •
        ∮ (z : ℂ) in C(c0, r),
          (z - c0)⁻¹ ^ n0 •
            (z - c0)⁻¹ • (2 * ↑π * I)⁻¹ • ∮ (z1 : ℂ) in C(c1, r), (z1 - c1)⁻¹ ^ n1 • (z1 - c1)⁻¹ • f (z, z1)‖ ≤
    b * r⁻¹ ^ n1 * r⁻¹ ^ n0
e : b * r⁻¹ ^ n1 * r⁻¹ ^ n0 = b * r⁻¹ ^ (n0 + n1)
⊢ ‖(2 * ↑π * I)⁻¹ •
        ∮ (z0 : ℂ) in C(c0, r),
          (z0 - c0)⁻¹ ^ n0 •
            (z0 - c0)⁻¹ • (2 * ↑π * I)⁻¹ • ∮ (z1 : ℂ) in C(c1, r), (z1 - c1)⁻¹ ^ n1 • (z1 - c1)⁻¹ • f (z0, z1)‖ ≤
    b * r⁻¹ ^ (n0 + n1)
Tactic:
rw [e] at outer
State after:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r b : ℝ
h : Separate f c0 c1 r b s
n0 n1 : ℕ
inner_c :
  ContinuousOn (fun z0 => (2 * ↑π * I)⁻¹ • ∮ (z1 : ℂ) in C(c1, r), (z1 - c1)⁻¹ ^ n1 • (z1 - c1)⁻¹ • f (z0, z1))
    (sphere c0 r)
inner_b :
  ∀ z0 ∈ sphere c0 r,
    ‖(2 * ↑π * I)⁻¹ • ∮ (z1 : ℂ) in C(c1, r), (z1 - c1)⁻¹ ^ n1 • (z1 - c1)⁻¹ • f (z0, z1)‖ ≤ b * r⁻¹ ^ n1
outer :
  ‖(2 * ↑π * I)⁻¹ •
        ∮ (z : ℂ) in C(c0, r),
          (z - c0)⁻¹ ^ n0 •
            (z - c0)⁻¹ • (2 * ↑π * I)⁻¹ • ∮ (z1 : ℂ) in C(c1, r), (z1 - c1)⁻¹ ^ n1 • (z1 - c1)⁻¹ • f (z, z1)‖ ≤
    b * r⁻¹ ^ (n0 + n1)
e : b * r⁻¹ ^ n1 * r⁻¹ ^ n0 = b * r⁻¹ ^ (n0 + n1)
⊢ ‖(2 * ↑π * I)⁻¹ •
        ∮ (z0 : ℂ) in C(c0, r),
          (z0 - c0)⁻¹ ^ n0 •
            (z0 - c0)⁻¹ • (2 * ↑π * I)⁻¹ • ∮ (z1 : ℂ) in C(c1, r), (z1 - c1)⁻¹ ^ n1 • (z1 - c1)⁻¹ • f (z0, z1)‖ ≤
    b * r⁻¹ ^ (n0 + n1)

State before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r b : ℝ
h : Separate f c0 c1 r b s
n0 n1 : ℕ
inner_c :
  ContinuousOn (fun z0 => (2 * ↑π * I)⁻¹ • ∮ (z1 : ℂ) in C(c1, r), (z1 - c1)⁻¹ ^ n1 • (z1 - c1)⁻¹ • f (z0, z1))
    (sphere c0 r)
inner_b :
  ∀ z0 ∈ sphere c0 r,
    ‖(2 * ↑π * I)⁻¹ • ∮ (z1 : ℂ) in C(c1, r), (z1 - c1)⁻¹ ^ n1 • (z1 - c1)⁻¹ • f (z0, z1)‖ ≤ b * r⁻¹ ^ n1
outer :
  ‖(2 * ↑π * I)⁻¹ •
        ∮ (z : ℂ) in C(c0, r),
          (z - c0)⁻¹ ^ n0 •
            (z - c0)⁻¹ • (2 * ↑π * I)⁻¹ • ∮ (z1 : ℂ) in C(c1, r), (z1 - c1)⁻¹ ^ n1 • (z1 - c1)⁻¹ • f (z, z1)‖ ≤
    b * r⁻¹ ^ (n0 + n1)
e : b * r⁻¹ ^ n1 * r⁻¹ ^ n0 = b * r⁻¹ ^ (n0 + n1)
⊢ ‖(2 * ↑π * I)⁻¹ •
        ∮ (z0 : ℂ) in C(c0, r),
          (z0 - c0)⁻¹ ^ n0 •
            (z0 - c0)⁻¹ • (2 * ↑π * I)⁻¹ • ∮ (z1 : ℂ) in C(c1, r), (z1 - c1)⁻¹ ^ n1 • (z1 - c1)⁻¹ • f (z0, z1)‖ ≤
    b * r⁻¹ ^ (n0 + n1)
Tactic:
exact outer
State after:
no goals

State before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r b : ℝ
h : Separate f c0 c1 r b s
n0 n1 : ℕ
inner_c :
  ContinuousOn (fun z0 => (2 * ↑π * I)⁻¹ • ∮ (z1 : ℂ) in C(c1, r), (z1 - c1)⁻¹ ^ n1 • (z1 - c1)⁻¹ • f (z0, z1))
    (sphere c0 r)
inner_b :
  ∀ z0 ∈ sphere c0 r,
    ‖(2 * ↑π * I)⁻¹ • ∮ (z1 : ℂ) in C(c1, r), (z1 - c1)⁻¹ ^ n1 • (z1 - c1)⁻¹ • f (z0, z1)‖ ≤ b * r⁻¹ ^ n1
outer :
  ‖(2 * ↑π * I)⁻¹ •
        ∮ (z : ℂ) in C(c0, r),
          (z - c0)⁻¹ ^ n0 •
            (z - c0)⁻¹ • (2 * ↑π * I)⁻¹ • ∮ (z1 : ℂ) in C(c1, r), (z1 - c1)⁻¹ ^ n1 • (z1 - c1)⁻¹ • f (z, z1)‖ ≤
    b * r⁻¹ ^ n1 * r⁻¹ ^ n0
⊢ b * r⁻¹ ^ n1 * r⁻¹ ^ n0 = b * r⁻¹ ^ (n0 + n1)
Tactic:
rw [mul_assoc, ← pow_add, add_comm n0 _]
State after:
no goals