Theorem: HasFPowerSeriesAt.along0 (Ray/Hartogs/Hartogs.lean)

State before:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f✝ : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0✝ c0' c1✝ z0 z1 w0 w1 : ℂ
r r0 r1 b e : ℝ
f : ℂ × ℂ → E
c0 c1 : ℂ
p : FormalMultilinearSeries ℂ (ℂ × ℂ) E
fp : HasFPowerSeriesAt f p (c0, c1)
⊢ HasFPowerSeriesAt (fun z0 => f (z0, c1)) p.along0 c0
Tactic:
rcases fp with ⟨r, fpr⟩
State after:
case intro
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f✝ : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0✝ c0' c1✝ z0 z1 w0 w1 : ℂ
r✝ r0 r1 b e : ℝ
f : ℂ × ℂ → E
c0 c1 : ℂ
p : FormalMultilinearSeries ℂ (ℂ × ℂ) E
r : ℝ≥0∞
fpr : HasFPowerSeriesOnBall f p (c0, c1) r
⊢ HasFPowerSeriesAt (fun z0 => f (z0, c1)) p.along0 c0

State before:
case intro
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f✝ : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0✝ c0' c1✝ z0 z1 w0 w1 : ℂ
r✝ r0 r1 b e : ℝ
f : ℂ × ℂ → E
c0 c1 : ℂ
p : FormalMultilinearSeries ℂ (ℂ × ℂ) E
r : ℝ≥0∞
fpr : HasFPowerSeriesOnBall f p (c0, c1) r
⊢ HasFPowerSeriesAt (fun z0 => f (z0, c1)) p.along0 c0
Tactic:
suffices h : HasFPowerSeriesOnBall (fun z0 ↦ f (z0, c1)) p.along0 c0 r by
  exact h.hasFPowerSeriesAt
State after:
case intro
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f✝ : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0✝ c0' c1✝ z0 z1 w0 w1 : ℂ
r✝ r0 r1 b e : ℝ
f : ℂ × ℂ → E
c0 c1 : ℂ
p : FormalMultilinearSeries ℂ (ℂ × ℂ) E
r : ℝ≥0∞
fpr : HasFPowerSeriesOnBall f p (c0, c1) r
⊢ HasFPowerSeriesOnBall (fun z0 => f (z0, c1)) p.along0 c0 r

State before:
case intro
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f✝ : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0✝ c0' c1✝ z0 z1 w0 w1 : ℂ
r✝ r0 r1 b e : ℝ
f : ℂ × ℂ → E
c0 c1 : ℂ
p : FormalMultilinearSeries ℂ (ℂ × ℂ) E
r : ℝ≥0∞
fpr : HasFPowerSeriesOnBall f p (c0, c1) r
⊢ HasFPowerSeriesOnBall (fun z0 => f (z0, c1)) p.along0 c0 r
Tactic:
refine
  { r_le := le_trans fpr.r_le (Along0.radius p)
    r_pos := fpr.r_pos
    hasSum := ?_ }
State after:
case intro
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f✝ : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0✝ c0' c1✝ z0 z1 w0 w1 : ℂ
r✝ r0 r1 b e : ℝ
f : ℂ × ℂ → E
c0 c1 : ℂ
p : FormalMultilinearSeries ℂ (ℂ × ℂ) E
r : ℝ≥0∞
fpr : HasFPowerSeriesOnBall f p (c0, c1) r
⊢ ∀ {y : ℂ}, y ∈ EMetric.ball 0 r → HasSum (fun n => (p.along0 n) fun x => y) (f (c0 + y, c1))

State before:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f✝ : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0✝ c0' c1✝ z0 z1 w0 w1 : ℂ
r✝ r0 r1 b e : ℝ
f : ℂ × ℂ → E
c0 c1 : ℂ
p : FormalMultilinearSeries ℂ (ℂ × ℂ) E
r : ℝ≥0∞
fpr : HasFPowerSeriesOnBall f p (c0, c1) r
h : HasFPowerSeriesOnBall (fun z0 => f (z0, c1)) p.along0 c0 r
⊢ HasFPowerSeriesAt (fun z0 => f (z0, c1)) p.along0 c0
Tactic:
exact h.hasFPowerSeriesAt
State after:
no goals

State before:
case intro
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f✝ : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0✝ c0' c1✝ z0 z1 w0 w1 : ℂ
r✝ r0 r1 b e : ℝ
f : ℂ × ℂ → E
c0 c1 : ℂ
p : FormalMultilinearSeries ℂ (ℂ × ℂ) E
r : ℝ≥0∞
fpr : HasFPowerSeriesOnBall f p (c0, c1) r
⊢ ∀ {y : ℂ}, y ∈ EMetric.ball 0 r → HasSum (fun n => (p.along0 n) fun x => y) (f (c0 + y, c1))
Tactic:
intro w0 w0r
State after:
case intro
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f✝ : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0✝ c0' c1✝ z0 z1 w0✝ w1 : ℂ
r✝ r0 r1 b e : ℝ
f : ℂ × ℂ → E
c0 c1 : ℂ
p : FormalMultilinearSeries ℂ (ℂ × ℂ) E
r : ℝ≥0∞
fpr : HasFPowerSeriesOnBall f p (c0, c1) r
w0 : ℂ
w0r : w0 ∈ EMetric.ball 0 r
⊢ HasSum (fun n => (p.along0 n) fun x => w0) (f (c0 + w0, c1))

State before:
case intro
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f✝ : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0✝ c0' c1✝ z0 z1 w0✝ w1 : ℂ
r✝ r0 r1 b e : ℝ
f : ℂ × ℂ → E
c0 c1 : ℂ
p : FormalMultilinearSeries ℂ (ℂ × ℂ) E
r : ℝ≥0∞
fpr : HasFPowerSeriesOnBall f p (c0, c1) r
w0 : ℂ
w0r : w0 ∈ EMetric.ball 0 r
⊢ HasSum (fun n => (p.along0 n) fun x => w0) (f (c0 + w0, c1))
Tactic:
simp_rw [FormalMultilinearSeries.along0, ContinuousMultilinearMap.along0, idZeroLm]
State after:
case intro
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f✝ : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0✝ c0' c1✝ z0 z1 w0✝ w1 : ℂ
r✝ r0 r1 b e : ℝ
f : ℂ × ℂ → E
c0 c1 : ℂ
p : FormalMultilinearSeries ℂ (ℂ × ℂ) E
r : ℝ≥0∞
fpr : HasFPowerSeriesOnBall f p (c0, c1) r
w0 : ℂ
w0r : w0 ∈ EMetric.ball 0 r
⊢ HasSum (fun n => ((p n).compContinuousLinearMap fun x => (ContinuousLinearMap.id ℂ ℂ).prod 0) fun x => w0)
    (f (c0 + w0, c1))

State before:
case intro
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f✝ : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0✝ c0' c1✝ z0 z1 w0✝ w1 : ℂ
r✝ r0 r1 b e : ℝ
f : ℂ × ℂ → E
c0 c1 : ℂ
p : FormalMultilinearSeries ℂ (ℂ × ℂ) E
r : ℝ≥0∞
fpr : HasFPowerSeriesOnBall f p (c0, c1) r
w0 : ℂ
w0r : w0 ∈ EMetric.ball 0 r
⊢ HasSum (fun n => ((p n).compContinuousLinearMap fun x => (ContinuousLinearMap.id ℂ ℂ).prod 0) fun x => w0)
    (f (c0 + w0, c1))
Tactic:
simp only [ContinuousMultilinearMap.compContinuousLinearMap_apply,
  ContinuousLinearMap.prod_apply, ContinuousLinearMap.coe_id', id_eq,
  ContinuousLinearMap.zero_apply]
State after:
case intro
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f✝ : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0✝ c0' c1✝ z0 z1 w0✝ w1 : ℂ
r✝ r0 r1 b e : ℝ
f : ℂ × ℂ → E
c0 c1 : ℂ
p : FormalMultilinearSeries ℂ (ℂ × ℂ) E
r : ℝ≥0∞
fpr : HasFPowerSeriesOnBall f p (c0, c1) r
w0 : ℂ
w0r : w0 ∈ EMetric.ball 0 r
⊢ HasSum (fun n => (p n) fun i => (w0, 0)) (f (c0 + w0, c1))

State before:
case intro
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f✝ : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0✝ c0' c1✝ z0 z1 w0✝ w1 : ℂ
r✝ r0 r1 b e : ℝ
f : ℂ × ℂ → E
c0 c1 : ℂ
p : FormalMultilinearSeries ℂ (ℂ × ℂ) E
r : ℝ≥0∞
fpr : HasFPowerSeriesOnBall f p (c0, c1) r
w0 : ℂ
w0r : w0 ∈ EMetric.ball 0 r
⊢ HasSum (fun n => (p n) fun i => (w0, 0)) (f (c0 + w0, c1))
Tactic:
have w01r : (w0, (0 : ℂ)) ∈ EMetric.ball (0 : ℂ × ℂ) r := by
  simpa only [Prod.edist_eq, EMetric.mem_ball, Prod.fst_zero, Prod.snd_zero, edist_self,
    ENNReal.max_zero_right] using w0r
State after:
case intro
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f✝ : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0✝ c0' c1✝ z0 z1 w0✝ w1 : ℂ
r✝ r0 r1 b e : ℝ
f : ℂ × ℂ → E
c0 c1 : ℂ
p : FormalMultilinearSeries ℂ (ℂ × ℂ) E
r : ℝ≥0∞
fpr : HasFPowerSeriesOnBall f p (c0, c1) r
w0 : ℂ
w0r : w0 ∈ EMetric.ball 0 r
w01r : (w0, 0) ∈ EMetric.ball 0 r
⊢ HasSum (fun n => (p n) fun i => (w0, 0)) (f (c0 + w0, c1))

State before:
case intro
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f✝ : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0✝ c0' c1✝ z0 z1 w0✝ w1 : ℂ
r✝ r0 r1 b e : ℝ
f : ℂ × ℂ → E
c0 c1 : ℂ
p : FormalMultilinearSeries ℂ (ℂ × ℂ) E
r : ℝ≥0∞
fpr : HasFPowerSeriesOnBall f p (c0, c1) r
w0 : ℂ
w0r : w0 ∈ EMetric.ball 0 r
w01r : (w0, 0) ∈ EMetric.ball 0 r
⊢ HasSum (fun n => (p n) fun i => (w0, 0)) (f (c0 + w0, c1))
Tactic:
convert fpr.hasSum w01r
State after:
case h.e'_6.h.e'_1.h.e'_4
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f✝ : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0✝ c0' c1✝ z0 z1 w0✝ w1 : ℂ
r✝ r0 r1 b e : ℝ
f : ℂ × ℂ → E
c0 c1 : ℂ
p : FormalMultilinearSeries ℂ (ℂ × ℂ) E
r : ℝ≥0∞
fpr : HasFPowerSeriesOnBall f p (c0, c1) r
w0 : ℂ
w0r : w0 ∈ EMetric.ball 0 r
w01r : (w0, 0) ∈ EMetric.ball 0 r
⊢ c1 = ((c0, c1) + (w0, 0)).2

State before:
case h.e'_6.h.e'_1.h.e'_4
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f✝ : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0✝ c0' c1✝ z0 z1 w0✝ w1 : ℂ
r✝ r0 r1 b e : ℝ
f : ℂ × ℂ → E
c0 c1 : ℂ
p : FormalMultilinearSeries ℂ (ℂ × ℂ) E
r : ℝ≥0∞
fpr : HasFPowerSeriesOnBall f p (c0, c1) r
w0 : ℂ
w0r : w0 ∈ EMetric.ball 0 r
w01r : (w0, 0) ∈ EMetric.ball 0 r
⊢ c1 = ((c0, c1) + (w0, 0)).2
Tactic:
rw [Prod.mk_add_mk, add_zero]
State after:
no goals

State before:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f✝ : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0✝ c0' c1✝ z0 z1 w0✝ w1 : ℂ
r✝ r0 r1 b e : ℝ
f : ℂ × ℂ → E
c0 c1 : ℂ
p : FormalMultilinearSeries ℂ (ℂ × ℂ) E
r : ℝ≥0∞
fpr : HasFPowerSeriesOnBall f p (c0, c1) r
w0 : ℂ
w0r : w0 ∈ EMetric.ball 0 r
⊢ (w0, 0) ∈ EMetric.ball 0 r
Tactic:
simpa only [Prod.edist_eq, EMetric.mem_ball, Prod.fst_zero, Prod.snd_zero, edist_self,
  ENNReal.max_zero_right] using w0r
State after:
no goals