internlm/Lean-Github huggingface dataset:
Theorem: Along0.radius
Proof 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 : ℝ
p : FormalMultilinearSeries ℂ (ℂ × ℂ) E
r : ℝ≥0
⊢ ∀ (i : ℝ), ⨆ (_ : ∀ (n : ℕ), ‖p n‖ * ↑r ^ n ≤ i), ↑r ≤ ⨆ (_ : ∀ (n : ℕ), ‖p.along0 n‖ * ↑r ^ n ≤ i), ↑r
Tactic:
intro C
Proof state after:
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 : ℝ
p : FormalMultilinearSeries ℂ (ℂ × ℂ) E
r : ℝ≥0
C : ℝ
⊢ ⨆ (_ : ∀ (n : ℕ), ‖p n‖ * ↑r ^ n ≤ C), ↑r ≤ ⨆ (_ : ∀ (n : ℕ), ‖p.along0 n‖ * ↑r ^ n ≤ C), ↑r
Theorem: Along0.radius
Proof 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 : ℝ
p : FormalMultilinearSeries ℂ (ℂ × ℂ) E
r : ℝ≥0
C : ℝ
⊢ ⨆ (_ : ∀ (n : ℕ), ‖p n‖ * ↑r ^ n ≤ C), ↑r ≤ ⨆ (_ : ∀ (n : ℕ), ‖p.along0 n‖ * ↑r ^ n ≤ C), ↑r
Tactic:
refine iSup_mono' ?_
Proof state after:
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 : ℝ
p : FormalMultilinearSeries ℂ (ℂ × ℂ) E
r : ℝ≥0
C : ℝ
⊢ (∀ (n : ℕ), ‖p n‖ * ↑r ^ n ≤ C) → ∃ (_ : ∀ (n : ℕ), ‖p.along0 n‖ * ↑r ^ n ≤ C), ↑r ≤ ↑r
Theorem: Along0.radius
Proof 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 : ℝ
p : FormalMultilinearSeries ℂ (ℂ × ℂ) E
r : ℝ≥0
C : ℝ
⊢ (∀ (n : ℕ), ‖p n‖ * ↑r ^ n ≤ C) → ∃ (_ : ∀ (n : ℕ), ‖p.along0 n‖ * ↑r ^ n ≤ C), ↑r ≤ ↑r
Tactic:
intro h
Proof state after:
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 : ℝ
p : FormalMultilinearSeries ℂ (ℂ × ℂ) E
r : ℝ≥0
C : ℝ
h : ∀ (n : ℕ), ‖p n‖ * ↑r ^ n ≤ C
⊢ ∃ (_ : ∀ (n : ℕ), ‖p.along0 n‖ * ↑r ^ n ≤ C), ↑r ≤ ↑r
Theorem: Along0.radius
Proof 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 : ℝ
p : FormalMultilinearSeries ℂ (ℂ × ℂ) E
r : ℝ≥0
C : ℝ
h : ∀ (n : ℕ), ‖p n‖ * ↑r ^ n ≤ C
⊢ ∃ (_ : ∀ (n : ℕ), ‖p.along0 n‖ * ↑r ^ n ≤ C), ↑r ≤ ↑r
Tactic:
have h' : ∀ n, ‖p.along0 n‖ * (r:ℝ)^n ≤ C := by
  intro n; refine le_trans ?_ (h n); apply mul_le_mul_of_nonneg_right
  exact Along0.norm (p n); bound
Proof state after:
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 : ℝ
p : FormalMultilinearSeries ℂ (ℂ × ℂ) E
r : ℝ≥0
C : ℝ
h : ∀ (n : ℕ), ‖p n‖ * ↑r ^ n ≤ C
h' : ∀ (n : ℕ), ‖p.along0 n‖ * ↑r ^ n ≤ C
⊢ ∃ (_ : ∀ (n : ℕ), ‖p.along0 n‖ * ↑r ^ n ≤ C), ↑r ≤ ↑r
Theorem: Along0.radius
Proof 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 : ℝ
p : FormalMultilinearSeries ℂ (ℂ × ℂ) E
r : ℝ≥0
C : ℝ
h : ∀ (n : ℕ), ‖p n‖ * ↑r ^ n ≤ C
h' : ∀ (n : ℕ), ‖p.along0 n‖ * ↑r ^ n ≤ C
⊢ ∃ (_ : ∀ (n : ℕ), ‖p.along0 n‖ * ↑r ^ n ≤ C), ↑r ≤ ↑r
Tactic:
use h'
Proof state after:
no goals
Theorem: Along0.radius
Proof 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 : ℝ
p : FormalMultilinearSeries ℂ (ℂ × ℂ) E
r : ℝ≥0
C : ℝ
h : ∀ (n : ℕ), ‖p n‖ * ↑r ^ n ≤ C
⊢ ∀ (n : ℕ), ‖p.along0 n‖ * ↑r ^ n ≤ C
Tactic:
intro n
Proof state after:
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 : ℝ
p : FormalMultilinearSeries ℂ (ℂ × ℂ) E
r : ℝ≥0
C : ℝ
h : ∀ (n : ℕ), ‖p n‖ * ↑r ^ n ≤ C
n : ℕ
⊢ ‖p.along0 n‖ * ↑r ^ n ≤ C
Theorem: Along0.radius
Proof 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 : ℝ
p : FormalMultilinearSeries ℂ (ℂ × ℂ) E
r : ℝ≥0
C : ℝ
h : ∀ (n : ℕ), ‖p n‖ * ↑r ^ n ≤ C
n : ℕ
⊢ ‖p.along0 n‖ * ↑r ^ n ≤ C
Tactic:
refine le_trans ?_ (h n)
Proof state after:
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 : ℝ
p : FormalMultilinearSeries ℂ (ℂ × ℂ) E
r : ℝ≥0
C : ℝ
h : ∀ (n : ℕ), ‖p n‖ * ↑r ^ n ≤ C
n : ℕ
⊢ ‖p.along0 n‖ * ↑r ^ n ≤ ‖p n‖ * ↑r ^ n
Theorem: Along0.radius
Proof 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 : ℝ
p : FormalMultilinearSeries ℂ (ℂ × ℂ) E
r : ℝ≥0
C : ℝ
h : ∀ (n : ℕ), ‖p n‖ * ↑r ^ n ≤ C
n : ℕ
⊢ ‖p.along0 n‖ * ↑r ^ n ≤ ‖p n‖ * ↑r ^ n
Tactic:
apply mul_le_mul_of_nonneg_right
Proof state after:
case h
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 : ℝ
p : FormalMultilinearSeries ℂ (ℂ × ℂ) E
r : ℝ≥0
C : ℝ
h : ∀ (n : ℕ), ‖p n‖ * ↑r ^ n ≤ C
n : ℕ
⊢ ‖p.along0 n‖ ≤ ‖p n‖

case a0
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 : ℝ
p : FormalMultilinearSeries ℂ (ℂ × ℂ) E
r : ℝ≥0
C : ℝ
h : ∀ (n : ℕ), ‖p n‖ * ↑r ^ n ≤ C
n : ℕ
⊢ 0 ≤ ↑r ^ n
Theorem: Along0.radius
Proof state before:
case h
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 : ℝ
p : FormalMultilinearSeries ℂ (ℂ × ℂ) E
r : ℝ≥0
C : ℝ
h : ∀ (n : ℕ), ‖p n‖ * ↑r ^ n ≤ C
n : ℕ
⊢ ‖p.along0 n‖ ≤ ‖p n‖

case a0
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 : ℝ
p : FormalMultilinearSeries ℂ (ℂ × ℂ) E
r : ℝ≥0
C : ℝ
h : ∀ (n : ℕ), ‖p n‖ * ↑r ^ n ≤ C
n : ℕ
⊢ 0 ≤ ↑r ^ n
Tactic:
exact Along0.norm (p n)
Proof state after:
case a0
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 : ℝ
p : FormalMultilinearSeries ℂ (ℂ × ℂ) E
r : ℝ≥0
C : ℝ
h : ∀ (n : ℕ), ‖p n‖ * ↑r ^ n ≤ C
n : ℕ
⊢ 0 ≤ ↑r ^ n
Theorem: Along0.radius
Proof state before:
case a0
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 : ℝ
p : FormalMultilinearSeries ℂ (ℂ × ℂ) E
r : ℝ≥0
C : ℝ
h : ∀ (n : ℕ), ‖p n‖ * ↑r ^ n ≤ C
n : ℕ
⊢ 0 ≤ ↑r ^ n
Tactic:
bound
Proof state after:
no goals
Theorem: HasFPowerSeriesAt.along0
Proof 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⟩
Proof 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
Theorem: HasFPowerSeriesAt.along0
Proof 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
Proof 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
Theorem: HasFPowerSeriesAt.along0
Proof 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 := ?_ }
Proof 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))
Theorem: HasFPowerSeriesAt.along0
Proof 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
Proof state after:
no goals
Theorem: HasFPowerSeriesAt.along0
Proof 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
Proof 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))
Theorem: HasFPowerSeriesAt.along0
Proof 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]
Proof 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))
Theorem: HasFPowerSeriesAt.along0
Proof 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]
Proof 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))
Theorem: HasFPowerSeriesAt.along0
Proof 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
Proof 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))
Theorem: HasFPowerSeriesAt.along0
Proof 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
Proof 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
Theorem: HasFPowerSeriesAt.along0
Proof 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]
Proof state after:
no goals
Theorem: HasFPowerSeriesAt.along0
Proof 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
Proof state after:
no goals
Theorem: Along0.analyticAt
Proof 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 : ℝ
n : ℕ
⊢ ∀ {p : ContinuousMultilinearMap ℂ (fun x => ℂ × ℂ) E}, AnalyticAt ℂ (fun p => p.along0) p
Tactic:
intro p
Proof state after:
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 : ℝ
n : ℕ
p : ContinuousMultilinearMap ℂ (fun x => ℂ × ℂ) E
⊢ AnalyticAt ℂ (fun p => p.along0) p
Theorem: Along0.analyticAt
Proof 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 : ℝ
n : ℕ
p : ContinuousMultilinearMap ℂ (fun x => ℂ × ℂ) E
⊢ AnalyticAt ℂ (fun p => p.along0) p
Tactic:
have e : (fun p : ContinuousMultilinearMap ℂ (fun _ : Fin n ↦ ℂ × ℂ) E => p.along0) =ᶠ[𝓝 p]
    (Along0.continuousLinearMap n : (ContinuousMultilinearMap ℂ (fun _ : Fin n ↦ ℂ × ℂ) E →
      ContinuousMultilinearMap ℂ (fun _ : Fin n ↦ ℂ) E)) := by
  apply eventually_of_forall; intro _; rfl
Proof state after:
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✝ : ℝ
n : ℕ
p : ContinuousMultilinearMap ℂ (fun x => ℂ × ℂ) E
e : (𝓝 p).EventuallyEq (fun p => p.along0) ⇑(continuousLinearMap n)
⊢ AnalyticAt ℂ (fun p => p.along0) p
Theorem: Along0.analyticAt
Proof 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✝ : ℝ
n : ℕ
p : ContinuousMultilinearMap ℂ (fun x => ℂ × ℂ) E
e : (𝓝 p).EventuallyEq (fun p => p.along0) ⇑(continuousLinearMap n)
⊢ AnalyticAt ℂ (fun p => p.along0) p
Tactic:
rw [analyticAt_congr e]
Proof state after:
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✝ : ℝ
n : ℕ
p : ContinuousMultilinearMap ℂ (fun x => ℂ × ℂ) E
e : (𝓝 p).EventuallyEq (fun p => p.along0) ⇑(continuousLinearMap n)
⊢ AnalyticAt ℂ (⇑(continuousLinearMap n)) p
Theorem: Along0.analyticAt
Proof 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✝ : ℝ
n : ℕ
p : ContinuousMultilinearMap ℂ (fun x => ℂ × ℂ) E
e : (𝓝 p).EventuallyEq (fun p => p.along0) ⇑(continuousLinearMap n)
⊢ AnalyticAt ℂ (⇑(continuousLinearMap n)) p
Tactic:
apply ContinuousLinearMap.analyticAt
Proof state after:
no goals
Theorem: Along0.analyticAt
Proof 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 : ℝ
n : ℕ
p : ContinuousMultilinearMap ℂ (fun x => ℂ × ℂ) E
⊢ (𝓝 p).EventuallyEq (fun p => p.along0) ⇑(continuousLinearMap n)
Tactic:
apply eventually_of_forall
Proof state after:
case hp
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 : ℝ
n : ℕ
p : ContinuousMultilinearMap ℂ (fun x => ℂ × ℂ) E
⊢ ∀ (x : ContinuousMultilinearMap ℂ (fun x => ℂ × ℂ) E), (fun p => p.along0) x = (continuousLinearMap n) x
Theorem: Along0.analyticAt
Proof state before:
case hp
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 : ℝ
n : ℕ
p : ContinuousMultilinearMap ℂ (fun x => ℂ × ℂ) E
⊢ ∀ (x : ContinuousMultilinearMap ℂ (fun x => ℂ × ℂ) E), (fun p => p.along0) x = (continuousLinearMap n) x
Tactic:
intro _
Proof state after:
case hp
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 : ℝ
n : ℕ
p x✝ : ContinuousMultilinearMap ℂ (fun x => ℂ × ℂ) E
⊢ (fun p => p.along0) x✝ = (continuousLinearMap n) x✝
Theorem: Along0.analyticAt
Proof state before:
case hp
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 : ℝ
n : ℕ
p x✝ : ContinuousMultilinearMap ℂ (fun x => ℂ × ℂ) E
⊢ (fun p => p.along0) x✝ = (continuousLinearMap n) x✝
Tactic:
rfl
Proof state after:
no goals
Theorem: unevenSeries_analytic
Proof 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 : ℝ
u : Uneven f c0 c1 r0 r1
n : ℕ
⊢ AnalyticOn ℂ (fun z1 => unevenSeries u z1 n) (ball c1 r1)
Tactic:
intro z1 z1s
Proof state after:
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 : ℝ
u : Uneven f c0 c1 r0 r1
n : ℕ
z1 : ℂ
z1s : z1 ∈ ball c1 r1
⊢ AnalyticAt ℂ (fun z1 => unevenSeries u z1 n) z1
Theorem: unevenSeries_analytic
Proof 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 : ℝ
u : Uneven f c0 c1 r0 r1
n : ℕ
z1 : ℂ
z1s : z1 ∈ ball c1 r1
⊢ AnalyticAt ℂ (fun z1 => unevenSeries u z1 n) z1
Tactic:
rcases u.a (c0, z1) (Set.mk_mem_prod (Metric.mem_ball_self u.r0p) z1s) with ⟨p, r, hp⟩
Proof state after:
case intro.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 : ℝ
u : Uneven f c0 c1 r0 r1
n : ℕ
z1 : ℂ
z1s : z1 ∈ ball c1 r1
p : FormalMultilinearSeries ℂ (ℂ × ℂ) E
r : ℝ≥0∞
hp : HasFPowerSeriesOnBall f p (c0, z1) r
⊢ AnalyticAt ℂ (fun z1 => unevenSeries u z1 n) z1