internlm/Lean-Github huggingface dataset:
Theorem: FormalMultilinearSeries.unshift_radius'
Proof state before:
case a
𝕜 : Type
inst✝¹² : NontriviallyNormedField 𝕜
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : CompleteSpace E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : CompleteSpace F
G : Type
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : CompleteSpace G
H : Type
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : CompleteSpace H
p : FormalMultilinearSeries 𝕜 𝕜 E
c : E
r : ℝ≥0
k : ℝ
h : ∀ (n : ℕ), ‖p n‖ * ↑r ^ n ≤ k
h' : ∀ (n : ℕ), ‖p.unshift' c n‖ * ↑r ^ n ≤ max ‖c‖ (k * ↑r)
⊢ ↑r ≤ ⨆ (_ : ∀ (n : ℕ), ‖p.unshift' c n‖ * ↑r ^ n ≤ max ‖c‖ (k * ↑r)), ↑r
Tactic:
convert le_iSup _ h'
Proof state after:
case h.e'_3
𝕜 : Type
inst✝¹² : NontriviallyNormedField 𝕜
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : CompleteSpace E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : CompleteSpace F
G : Type
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : CompleteSpace G
H : Type
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : CompleteSpace H
p : FormalMultilinearSeries 𝕜 𝕜 E
c : E
r : ℝ≥0
k : ℝ
h : ∀ (n : ℕ), ‖p n‖ * ↑r ^ n ≤ k
h' : ∀ (n : ℕ), ‖p.unshift' c n‖ * ↑r ^ n ≤ max ‖c‖ (k * ↑r)
⊢ ↑r = ↑r
Theorem: FormalMultilinearSeries.unshift_radius'
Proof state before:
case h.e'_3
𝕜 : Type
inst✝¹² : NontriviallyNormedField 𝕜
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : CompleteSpace E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : CompleteSpace F
G : Type
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : CompleteSpace G
H : Type
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : CompleteSpace H
p : FormalMultilinearSeries 𝕜 𝕜 E
c : E
r : ℝ≥0
k : ℝ
h : ∀ (n : ℕ), ‖p n‖ * ↑r ^ n ≤ k
h' : ∀ (n : ℕ), ‖p.unshift' c n‖ * ↑r ^ n ≤ max ‖c‖ (k * ↑r)
⊢ ↑r = ↑r
Tactic:
rfl
Proof state after:
no goals
Theorem: FormalMultilinearSeries.unshift_radius'
Proof state before:
𝕜 : Type
inst✝¹² : NontriviallyNormedField 𝕜
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : CompleteSpace E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : CompleteSpace F
G : Type
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : CompleteSpace G
H : Type
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : CompleteSpace H
p : FormalMultilinearSeries 𝕜 𝕜 E
c : E
r : ℝ≥0
k : ℝ
h : ∀ (n : ℕ), ‖p n‖ * ↑r ^ n ≤ k
⊢ ∀ (n : ℕ), ‖p.unshift' c n‖ * ↑r ^ n ≤ max ‖c‖ (k * ↑r)
Tactic:
intro n
Proof state after:
𝕜 : Type
inst✝¹² : NontriviallyNormedField 𝕜
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : CompleteSpace E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : CompleteSpace F
G : Type
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : CompleteSpace G
H : Type
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : CompleteSpace H
p : FormalMultilinearSeries 𝕜 𝕜 E
c : E
r : ℝ≥0
k : ℝ
h : ∀ (n : ℕ), ‖p n‖ * ↑r ^ n ≤ k
n : ℕ
⊢ ‖p.unshift' c n‖ * ↑r ^ n ≤ max ‖c‖ (k * ↑r)
Theorem: FormalMultilinearSeries.unshift_radius'
Proof state before:
𝕜 : Type
inst✝¹² : NontriviallyNormedField 𝕜
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : CompleteSpace E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : CompleteSpace F
G : Type
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : CompleteSpace G
H : Type
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : CompleteSpace H
p : FormalMultilinearSeries 𝕜 𝕜 E
c : E
r : ℝ≥0
k : ℝ
h : ∀ (n : ℕ), ‖p n‖ * ↑r ^ n ≤ k
n : ℕ
⊢ ‖p.unshift' c n‖ * ↑r ^ n ≤ max ‖c‖ (k * ↑r)
Tactic:
induction' n with n _
Proof state after:
case zero
𝕜 : Type
inst✝¹² : NontriviallyNormedField 𝕜
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : CompleteSpace E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : CompleteSpace F
G : Type
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : CompleteSpace G
H : Type
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : CompleteSpace H
p : FormalMultilinearSeries 𝕜 𝕜 E
c : E
r : ℝ≥0
k : ℝ
h : ∀ (n : ℕ), ‖p n‖ * ↑r ^ n ≤ k
⊢ ‖p.unshift' c 0‖ * ↑r ^ 0 ≤ max ‖c‖ (k * ↑r)

case succ
𝕜 : Type
inst✝¹² : NontriviallyNormedField 𝕜
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : CompleteSpace E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : CompleteSpace F
G : Type
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : CompleteSpace G
H : Type
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : CompleteSpace H
p : FormalMultilinearSeries 𝕜 𝕜 E
c : E
r : ℝ≥0
k : ℝ
h : ∀ (n : ℕ), ‖p n‖ * ↑r ^ n ≤ k
n : ℕ
a✝ : ‖p.unshift' c n‖ * ↑r ^ n ≤ max ‖c‖ (k * ↑r)
⊢ ‖p.unshift' c (n + 1)‖ * ↑r ^ (n + 1) ≤ max ‖c‖ (k * ↑r)
Theorem: FormalMultilinearSeries.unshift_radius'
Proof state before:
case zero
𝕜 : Type
inst✝¹² : NontriviallyNormedField 𝕜
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : CompleteSpace E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : CompleteSpace F
G : Type
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : CompleteSpace G
H : Type
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : CompleteSpace H
p : FormalMultilinearSeries 𝕜 𝕜 E
c : E
r : ℝ≥0
k : ℝ
h : ∀ (n : ℕ), ‖p n‖ * ↑r ^ n ≤ k
⊢ ‖p.unshift' c 0‖ * ↑r ^ 0 ≤ max ‖c‖ (k * ↑r)
Tactic:
simp only [FormalMultilinearSeries.unshift_coeff_zero,
  FormalMultilinearSeries.norm_apply_eq_norm_coef, pow_zero, mul_one, le_max_iff, le_refl,
  true_or_iff]
Proof state after:
no goals
Theorem: FormalMultilinearSeries.unshift_radius'
Proof state before:
case succ
𝕜 : Type
inst✝¹² : NontriviallyNormedField 𝕜
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : CompleteSpace E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : CompleteSpace F
G : Type
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : CompleteSpace G
H : Type
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : CompleteSpace H
p : FormalMultilinearSeries 𝕜 𝕜 E
c : E
r : ℝ≥0
k : ℝ
h : ∀ (n : ℕ), ‖p n‖ * ↑r ^ n ≤ k
n : ℕ
a✝ : ‖p.unshift' c n‖ * ↑r ^ n ≤ max ‖c‖ (k * ↑r)
⊢ ‖p.unshift' c (n + 1)‖ * ↑r ^ (n + 1) ≤ max ‖c‖ (k * ↑r)
Tactic:
simp only [FormalMultilinearSeries.norm_apply_eq_norm_coef] at h
Proof state after:
case succ
𝕜 : Type
inst✝¹² : NontriviallyNormedField 𝕜
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : CompleteSpace E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : CompleteSpace F
G : Type
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : CompleteSpace G
H : Type
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : CompleteSpace H
p : FormalMultilinearSeries 𝕜 𝕜 E
c : E
r : ℝ≥0
k : ℝ
n : ℕ
a✝ : ‖p.unshift' c n‖ * ↑r ^ n ≤ max ‖c‖ (k * ↑r)
h : ∀ (n : ℕ), ‖p.coeff n‖ * ↑r ^ n ≤ k
⊢ ‖p.unshift' c (n + 1)‖ * ↑r ^ (n + 1) ≤ max ‖c‖ (k * ↑r)
Theorem: FormalMultilinearSeries.unshift_radius'
Proof state before:
case succ
𝕜 : Type
inst✝¹² : NontriviallyNormedField 𝕜
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : CompleteSpace E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : CompleteSpace F
G : Type
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : CompleteSpace G
H : Type
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : CompleteSpace H
p : FormalMultilinearSeries 𝕜 𝕜 E
c : E
r : ℝ≥0
k : ℝ
n : ℕ
a✝ : ‖p.unshift' c n‖ * ↑r ^ n ≤ max ‖c‖ (k * ↑r)
h : ∀ (n : ℕ), ‖p.coeff n‖ * ↑r ^ n ≤ k
⊢ ‖p.unshift' c (n + 1)‖ * ↑r ^ (n + 1) ≤ max ‖c‖ (k * ↑r)
Tactic:
simp only [FormalMultilinearSeries.unshift_coeff_succ, pow_succ, ← mul_assoc,
  FormalMultilinearSeries.norm_apply_eq_norm_coef, le_max_iff]
Proof state after:
case succ
𝕜 : Type
inst✝¹² : NontriviallyNormedField 𝕜
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : CompleteSpace E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : CompleteSpace F
G : Type
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : CompleteSpace G
H : Type
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : CompleteSpace H
p : FormalMultilinearSeries 𝕜 𝕜 E
c : E
r : ℝ≥0
k : ℝ
n : ℕ
a✝ : ‖p.unshift' c n‖ * ↑r ^ n ≤ max ‖c‖ (k * ↑r)
h : ∀ (n : ℕ), ‖p.coeff n‖ * ↑r ^ n ≤ k
⊢ ‖p.coeff n‖ * ↑r ^ n * ↑r ≤ ‖c‖ ∨ ‖p.coeff n‖ * ↑r ^ n * ↑r ≤ k * ↑r
Theorem: FormalMultilinearSeries.unshift_radius'
Proof state before:
case succ
𝕜 : Type
inst✝¹² : NontriviallyNormedField 𝕜
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : CompleteSpace E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : CompleteSpace F
G : Type
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : CompleteSpace G
H : Type
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : CompleteSpace H
p : FormalMultilinearSeries 𝕜 𝕜 E
c : E
r : ℝ≥0
k : ℝ
n : ℕ
a✝ : ‖p.unshift' c n‖ * ↑r ^ n ≤ max ‖c‖ (k * ↑r)
h : ∀ (n : ℕ), ‖p.coeff n‖ * ↑r ^ n ≤ k
⊢ ‖p.coeff n‖ * ↑r ^ n * ↑r ≤ ‖c‖ ∨ ‖p.coeff n‖ * ↑r ^ n * ↑r ≤ k * ↑r
Tactic:
right
Proof state after:
case succ.h
𝕜 : Type
inst✝¹² : NontriviallyNormedField 𝕜
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : CompleteSpace E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : CompleteSpace F
G : Type
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : CompleteSpace G
H : Type
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : CompleteSpace H
p : FormalMultilinearSeries 𝕜 𝕜 E
c : E
r : ℝ≥0
k : ℝ
n : ℕ
a✝ : ‖p.unshift' c n‖ * ↑r ^ n ≤ max ‖c‖ (k * ↑r)
h : ∀ (n : ℕ), ‖p.coeff n‖ * ↑r ^ n ≤ k
⊢ ‖p.coeff n‖ * ↑r ^ n * ↑r ≤ k * ↑r
Theorem: FormalMultilinearSeries.unshift_radius'
Proof state before:
case succ.h
𝕜 : Type
inst✝¹² : NontriviallyNormedField 𝕜
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : CompleteSpace E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : CompleteSpace F
G : Type
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : CompleteSpace G
H : Type
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : CompleteSpace H
p : FormalMultilinearSeries 𝕜 𝕜 E
c : E
r : ℝ≥0
k : ℝ
n : ℕ
a✝ : ‖p.unshift' c n‖ * ↑r ^ n ≤ max ‖c‖ (k * ↑r)
h : ∀ (n : ℕ), ‖p.coeff n‖ * ↑r ^ n ≤ k
⊢ ‖p.coeff n‖ * ↑r ^ n * ↑r ≤ k * ↑r
Tactic:
exact mul_le_mul_of_nonneg_right (h n) (NNReal.coe_nonneg _)
Proof state after:
no goals
Theorem: HasFPowerSeriesOnBall.unshift
Proof state before:
𝕜 : Type
inst✝¹² : NontriviallyNormedField 𝕜
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : CompleteSpace E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : CompleteSpace F
G : Type
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : CompleteSpace G
H : Type
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : CompleteSpace H
f : 𝕜 → E
p : FormalMultilinearSeries 𝕜 𝕜 E
c : 𝕜
r : ℝ≥0∞
fp : HasFPowerSeriesOnBall f p c r
⊢ ∀ {y : 𝕜}, y ∈ EMetric.ball 0 r → HasSum (fun n => (p.unshift' 0 n) fun x => y) ((c + y - c) • f (c + y))
Tactic:
intro y yr
Proof state after:
𝕜 : Type
inst✝¹² : NontriviallyNormedField 𝕜
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : CompleteSpace E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : CompleteSpace F
G : Type
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : CompleteSpace G
H : Type
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : CompleteSpace H
f : 𝕜 → E
p : FormalMultilinearSeries 𝕜 𝕜 E
c : 𝕜
r : ℝ≥0∞
fp : HasFPowerSeriesOnBall f p c r
y : 𝕜
yr : y ∈ EMetric.ball 0 r
⊢ HasSum (fun n => (p.unshift' 0 n) fun x => y) ((c + y - c) • f (c + y))
Theorem: HasFPowerSeriesOnBall.unshift
Proof state before:
𝕜 : Type
inst✝¹² : NontriviallyNormedField 𝕜
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : CompleteSpace E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : CompleteSpace F
G : Type
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : CompleteSpace G
H : Type
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : CompleteSpace H
f : 𝕜 → E
p : FormalMultilinearSeries 𝕜 𝕜 E
c : 𝕜
r : ℝ≥0∞
fp : HasFPowerSeriesOnBall f p c r
y : 𝕜
yr : y ∈ EMetric.ball 0 r
⊢ HasSum (fun n => (p.unshift' 0 n) fun x => y) ((c + y - c) • f (c + y))
Tactic:
simp only [FormalMultilinearSeries.apply_eq_pow_smul_coeff, add_sub_cancel_left]
Proof state after:
𝕜 : Type
inst✝¹² : NontriviallyNormedField 𝕜
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : CompleteSpace E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : CompleteSpace F
G : Type
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : CompleteSpace G
H : Type
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : CompleteSpace H
f : 𝕜 → E
p : FormalMultilinearSeries 𝕜 𝕜 E
c : 𝕜
r : ℝ≥0∞
fp : HasFPowerSeriesOnBall f p c r
y : 𝕜
yr : y ∈ EMetric.ball 0 r
⊢ HasSum (fun n => y ^ n • (p.unshift' 0).coeff n) (y • f (c + y))
Theorem: HasFPowerSeriesOnBall.unshift
Proof state before:
𝕜 : Type
inst✝¹² : NontriviallyNormedField 𝕜
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : CompleteSpace E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : CompleteSpace F
G : Type
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : CompleteSpace G
H : Type
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : CompleteSpace H
f : 𝕜 → E
p : FormalMultilinearSeries 𝕜 𝕜 E
c : 𝕜
r : ℝ≥0∞
fp : HasFPowerSeriesOnBall f p c r
y : 𝕜
yr : y ∈ EMetric.ball 0 r
⊢ HasSum (fun n => y ^ n • (p.unshift' 0).coeff n) (y • f (c + y))
Tactic:
generalize hs : (fun n ↦ y ^ n • (p.unshift' 0).coeff n) = s
Proof state after:
𝕜 : Type
inst✝¹² : NontriviallyNormedField 𝕜
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : CompleteSpace E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : CompleteSpace F
G : Type
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : CompleteSpace G
H : Type
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : CompleteSpace H
f : 𝕜 → E
p : FormalMultilinearSeries 𝕜 𝕜 E
c : 𝕜
r : ℝ≥0∞
fp : HasFPowerSeriesOnBall f p c r
y : 𝕜
yr : y ∈ EMetric.ball 0 r
s : ℕ → E
hs : (fun n => y ^ n • (p.unshift' 0).coeff n) = s
⊢ HasSum s (y • f (c + y))
Theorem: HasFPowerSeriesOnBall.unshift
Proof state before:
𝕜 : Type
inst✝¹² : NontriviallyNormedField 𝕜
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : CompleteSpace E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : CompleteSpace F
G : Type
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : CompleteSpace G
H : Type
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : CompleteSpace H
f : 𝕜 → E
p : FormalMultilinearSeries 𝕜 𝕜 E
c : 𝕜
r : ℝ≥0∞
fp : HasFPowerSeriesOnBall f p c r
y : 𝕜
yr : y ∈ EMetric.ball 0 r
s : ℕ → E
hs : (fun n => y ^ n • (p.unshift' 0).coeff n) = s
⊢ HasSum s (y • f (c + y))
Tactic:
have s0 : y • f (c + y) = y • f (c + y) + (Finset.range 1).sum s := by
  simp only [← hs, p.unshift_coeff_zero, Finset.range_one, Finset.sum_singleton, smul_zero,
    add_zero]
Proof state after:
𝕜 : Type
inst✝¹² : NontriviallyNormedField 𝕜
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : CompleteSpace E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : CompleteSpace F
G : Type
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : CompleteSpace G
H : Type
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : CompleteSpace H
f : 𝕜 → E
p : FormalMultilinearSeries 𝕜 𝕜 E
c : 𝕜
r : ℝ≥0∞
fp : HasFPowerSeriesOnBall f p c r
y : 𝕜
yr : y ∈ EMetric.ball 0 r
s : ℕ → E
hs : (fun n => y ^ n • (p.unshift' 0).coeff n) = s
s0 : y • f (c + y) = y • f (c + y) + (Finset.range 1).sum s
⊢ HasSum s (y • f (c + y))
Theorem: HasFPowerSeriesOnBall.unshift
Proof state before:
𝕜 : Type
inst✝¹² : NontriviallyNormedField 𝕜
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : CompleteSpace E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : CompleteSpace F
G : Type
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : CompleteSpace G
H : Type
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : CompleteSpace H
f : 𝕜 → E
p : FormalMultilinearSeries 𝕜 𝕜 E
c : 𝕜
r : ℝ≥0∞
fp : HasFPowerSeriesOnBall f p c r
y : 𝕜
yr : y ∈ EMetric.ball 0 r
s : ℕ → E
hs : (fun n => y ^ n • (p.unshift' 0).coeff n) = s
s0 : y • f (c + y) = y • f (c + y) + (Finset.range 1).sum s
⊢ HasSum s (y • f (c + y))
Tactic:
rw [s0, ← hasSum_nat_add_iff, ← hs]
Proof state after:
𝕜 : Type
inst✝¹² : NontriviallyNormedField 𝕜
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : CompleteSpace E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : CompleteSpace F
G : Type
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : CompleteSpace G
H : Type
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : CompleteSpace H
f : 𝕜 → E
p : FormalMultilinearSeries 𝕜 𝕜 E
c : 𝕜
r : ℝ≥0∞
fp : HasFPowerSeriesOnBall f p c r
y : 𝕜
yr : y ∈ EMetric.ball 0 r
s : ℕ → E
hs : (fun n => y ^ n • (p.unshift' 0).coeff n) = s
s0 : y • f (c + y) = y • f (c + y) + (Finset.range 1).sum s
⊢ HasSum (fun n => (fun n => y ^ n • (p.unshift' 0).coeff n) (n + 1)) (y • f (c + y))
Theorem: HasFPowerSeriesOnBall.unshift
Proof state before:
𝕜 : Type
inst✝¹² : NontriviallyNormedField 𝕜
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : CompleteSpace E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : CompleteSpace F
G : Type
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : CompleteSpace G
H : Type
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : CompleteSpace H
f : 𝕜 → E
p : FormalMultilinearSeries 𝕜 𝕜 E
c : 𝕜
r : ℝ≥0∞
fp : HasFPowerSeriesOnBall f p c r
y : 𝕜
yr : y ∈ EMetric.ball 0 r
s : ℕ → E
hs : (fun n => y ^ n • (p.unshift' 0).coeff n) = s
s0 : y • f (c + y) = y • f (c + y) + (Finset.range 1).sum s
⊢ HasSum (fun n => (fun n => y ^ n • (p.unshift' 0).coeff n) (n + 1)) (y • f (c + y))
Tactic:
simp only [p.unshift_coeff_succ, pow_succ', ← smul_smul]
Proof state after:
𝕜 : Type
inst✝¹² : NontriviallyNormedField 𝕜
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : CompleteSpace E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : CompleteSpace F
G : Type
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : CompleteSpace G
H : Type
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : CompleteSpace H
f : 𝕜 → E
p : FormalMultilinearSeries 𝕜 𝕜 E
c : 𝕜
r : ℝ≥0∞
fp : HasFPowerSeriesOnBall f p c r
y : 𝕜
yr : y ∈ EMetric.ball 0 r
s : ℕ → E
hs : (fun n => y ^ n • (p.unshift' 0).coeff n) = s
s0 : y • f (c + y) = y • f (c + y) + (Finset.range 1).sum s
⊢ HasSum (fun n => y • y ^ n • p.coeff n) (y • f (c + y))
Theorem: HasFPowerSeriesOnBall.unshift
Proof state before:
𝕜 : Type
inst✝¹² : NontriviallyNormedField 𝕜
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : CompleteSpace E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : CompleteSpace F
G : Type
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : CompleteSpace G
H : Type
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : CompleteSpace H
f : 𝕜 → E
p : FormalMultilinearSeries 𝕜 𝕜 E
c : 𝕜
r : ℝ≥0∞
fp : HasFPowerSeriesOnBall f p c r
y : 𝕜
yr : y ∈ EMetric.ball 0 r
s : ℕ → E
hs : (fun n => y ^ n • (p.unshift' 0).coeff n) = s
s0 : y • f (c + y) = y • f (c + y) + (Finset.range 1).sum s
⊢ HasSum (fun n => y • y ^ n • p.coeff n) (y • f (c + y))
Tactic:
apply HasSum.const_smul
Proof state after:
case hf
𝕜 : Type
inst✝¹² : NontriviallyNormedField 𝕜
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : CompleteSpace E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : CompleteSpace F
G : Type
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : CompleteSpace G
H : Type
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : CompleteSpace H
f : 𝕜 → E
p : FormalMultilinearSeries 𝕜 𝕜 E
c : 𝕜
r : ℝ≥0∞
fp : HasFPowerSeriesOnBall f p c r
y : 𝕜
yr : y ∈ EMetric.ball 0 r
s : ℕ → E
hs : (fun n => y ^ n • (p.unshift' 0).coeff n) = s
s0 : y • f (c + y) = y • f (c + y) + (Finset.range 1).sum s
⊢ HasSum (fun i => y ^ i • p.coeff i) (f (c + y))
Theorem: HasFPowerSeriesOnBall.unshift
Proof state before:
case hf
𝕜 : Type
inst✝¹² : NontriviallyNormedField 𝕜
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : CompleteSpace E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : CompleteSpace F
G : Type
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : CompleteSpace G
H : Type
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : CompleteSpace H
f : 𝕜 → E
p : FormalMultilinearSeries 𝕜 𝕜 E
c : 𝕜
r : ℝ≥0∞
fp : HasFPowerSeriesOnBall f p c r
y : 𝕜
yr : y ∈ EMetric.ball 0 r
s : ℕ → E
hs : (fun n => y ^ n • (p.unshift' 0).coeff n) = s
s0 : y • f (c + y) = y • f (c + y) + (Finset.range 1).sum s
⊢ HasSum (fun i => y ^ i • p.coeff i) (f (c + y))
Tactic:
have h := fp.hasSum yr
Proof state after:
case hf
𝕜 : Type
inst✝¹² : NontriviallyNormedField 𝕜
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : CompleteSpace E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : CompleteSpace F
G : Type
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : CompleteSpace G
H : Type
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : CompleteSpace H
f : 𝕜 → E
p : FormalMultilinearSeries 𝕜 𝕜 E
c : 𝕜
r : ℝ≥0∞
fp : HasFPowerSeriesOnBall f p c r
y : 𝕜
yr : y ∈ EMetric.ball 0 r
s : ℕ → E
hs : (fun n => y ^ n • (p.unshift' 0).coeff n) = s
s0 : y • f (c + y) = y • f (c + y) + (Finset.range 1).sum s
h : HasSum (fun n => (p n) fun x => y) (f (c + y))
⊢ HasSum (fun i => y ^ i • p.coeff i) (f (c + y))
Theorem: HasFPowerSeriesOnBall.unshift
Proof state before:
case hf
𝕜 : Type
inst✝¹² : NontriviallyNormedField 𝕜
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : CompleteSpace E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : CompleteSpace F
G : Type
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : CompleteSpace G
H : Type
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : CompleteSpace H
f : 𝕜 → E
p : FormalMultilinearSeries 𝕜 𝕜 E
c : 𝕜
r : ℝ≥0∞
fp : HasFPowerSeriesOnBall f p c r
y : 𝕜
yr : y ∈ EMetric.ball 0 r
s : ℕ → E
hs : (fun n => y ^ n • (p.unshift' 0).coeff n) = s
s0 : y • f (c + y) = y • f (c + y) + (Finset.range 1).sum s
h : HasSum (fun n => (p n) fun x => y) (f (c + y))
⊢ HasSum (fun i => y ^ i • p.coeff i) (f (c + y))
Tactic:
simp only [FormalMultilinearSeries.apply_eq_pow_smul_coeff] at h
Proof state after:
case hf
𝕜 : Type
inst✝¹² : NontriviallyNormedField 𝕜
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : CompleteSpace E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : CompleteSpace F
G : Type
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : CompleteSpace G
H : Type
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : CompleteSpace H
f : 𝕜 → E
p : FormalMultilinearSeries 𝕜 𝕜 E
c : 𝕜
r : ℝ≥0∞
fp : HasFPowerSeriesOnBall f p c r
y : 𝕜
yr : y ∈ EMetric.ball 0 r
s : ℕ → E
hs : (fun n => y ^ n • (p.unshift' 0).coeff n) = s
s0 : y • f (c + y) = y • f (c + y) + (Finset.range 1).sum s
h : HasSum (fun n => y ^ n • p.coeff n) (f (c + y))
⊢ HasSum (fun i => y ^ i • p.coeff i) (f (c + y))