Theorem: sum_cons (Ray/Analytic/Series.lean)

State before:
X : Type
inst✝ : NormedAddCommGroup X
a g : X
f : ℕ → X
h : HasSum f g
⊢ HasSum (Stream'.cons a f) (a + g)
Tactic:
rw [HasSum] at h ⊢
State after:
X : Type
inst✝ : NormedAddCommGroup X
a g : X
f : ℕ → X
h : Filter.Tendsto (fun s => s.sum fun b => f b) atTop (𝓝 g)
⊢ Filter.Tendsto (fun s => s.sum fun b => Stream'.cons a f b) atTop (𝓝 (a + g))

State before:
X : Type
inst✝ : NormedAddCommGroup X
a g : X
f : ℕ → X
h : Filter.Tendsto (fun s => s.sum fun b => f b) atTop (𝓝 g)
⊢ Filter.Tendsto (fun s => s.sum fun b => Stream'.cons a f b) atTop (𝓝 (a + g))
Tactic:
have ha := Filter.Tendsto.comp (Continuous.tendsto (continuous_add_left a) g) h
State after:
X : Type
inst✝ : NormedAddCommGroup X
a g : X
f : ℕ → X
h : Filter.Tendsto (fun s => s.sum fun b => f b) atTop (𝓝 g)
ha : Filter.Tendsto ((fun b => a + b) ∘ fun s => s.sum fun b => f b) atTop (𝓝 (a + g))
⊢ Filter.Tendsto (fun s => s.sum fun b => Stream'.cons a f b) atTop (𝓝 (a + g))

State before:
X : Type
inst✝ : NormedAddCommGroup X
a g : X
f : ℕ → X
h : Filter.Tendsto (fun s => s.sum fun b => f b) atTop (𝓝 g)
ha : Filter.Tendsto ((fun b => a + b) ∘ fun s => s.sum fun b => f b) atTop (𝓝 (a + g))
⊢ Filter.Tendsto (fun s => s.sum fun b => Stream'.cons a f b) atTop (𝓝 (a + g))
Tactic:
have s : ((fun z ↦ a + z) ∘ fun N : Finset ℕ ↦ N.sum f) =
    (fun N : Finset ℕ ↦ N.sum (Stream'.cons a f)) ∘ push := by
  apply funext; intro N; simp; exact push_sum
State after:
X : Type
inst✝ : NormedAddCommGroup X
a g : X
f : ℕ → X
h : Filter.Tendsto (fun s => s.sum fun b => f b) atTop (𝓝 g)
ha : Filter.Tendsto ((fun b => a + b) ∘ fun s => s.sum fun b => f b) atTop (𝓝 (a + g))
s : ((fun z => a + z) ∘ fun N => N.sum f) = (fun N => N.sum (Stream'.cons a f)) ∘ push
⊢ Filter.Tendsto (fun s => s.sum fun b => Stream'.cons a f b) atTop (𝓝 (a + g))

State before:
X : Type
inst✝ : NormedAddCommGroup X
a g : X
f : ℕ → X
h : Filter.Tendsto (fun s => s.sum fun b => f b) atTop (𝓝 g)
ha : Filter.Tendsto ((fun b => a + b) ∘ fun s => s.sum fun b => f b) atTop (𝓝 (a + g))
s : ((fun z => a + z) ∘ fun N => N.sum f) = (fun N => N.sum (Stream'.cons a f)) ∘ push
⊢ Filter.Tendsto (fun s => s.sum fun b => Stream'.cons a f b) atTop (𝓝 (a + g))
Tactic:
rw [s] at ha
State after:
X : Type
inst✝ : NormedAddCommGroup X
a g : X
f : ℕ → X
h : Filter.Tendsto (fun s => s.sum fun b => f b) atTop (𝓝 g)
ha : Filter.Tendsto ((fun N => N.sum (Stream'.cons a f)) ∘ push) atTop (𝓝 (a + g))
s : ((fun z => a + z) ∘ fun N => N.sum f) = (fun N => N.sum (Stream'.cons a f)) ∘ push
⊢ Filter.Tendsto (fun s => s.sum fun b => Stream'.cons a f b) atTop (𝓝 (a + g))

State before:
X : Type
inst✝ : NormedAddCommGroup X
a g : X
f : ℕ → X
h : Filter.Tendsto (fun s => s.sum fun b => f b) atTop (𝓝 g)
ha : Filter.Tendsto ((fun N => N.sum (Stream'.cons a f)) ∘ push) atTop (𝓝 (a + g))
s : ((fun z => a + z) ∘ fun N => N.sum f) = (fun N => N.sum (Stream'.cons a f)) ∘ push
⊢ Filter.Tendsto (fun s => s.sum fun b => Stream'.cons a f b) atTop (𝓝 (a + g))
Tactic:
exact tendsto_comp_push.mp ha
State after:
no goals

State before:
X : Type
inst✝ : NormedAddCommGroup X
a g : X
f : ℕ → X
h : Filter.Tendsto (fun s => s.sum fun b => f b) atTop (𝓝 g)
ha : Filter.Tendsto ((fun b => a + b) ∘ fun s => s.sum fun b => f b) atTop (𝓝 (a + g))
⊢ ((fun z => a + z) ∘ fun N => N.sum f) = (fun N => N.sum (Stream'.cons a f)) ∘ push
Tactic:
apply funext
State after:
case h
X : Type
inst✝ : NormedAddCommGroup X
a g : X
f : ℕ → X
h : Filter.Tendsto (fun s => s.sum fun b => f b) atTop (𝓝 g)
ha : Filter.Tendsto ((fun b => a + b) ∘ fun s => s.sum fun b => f b) atTop (𝓝 (a + g))
⊢ ∀ (x : Finset ℕ), ((fun z => a + z) ∘ fun N => N.sum f) x = ((fun N => N.sum (Stream'.cons a f)) ∘ push) x

State before:
case h
X : Type
inst✝ : NormedAddCommGroup X
a g : X
f : ℕ → X
h : Filter.Tendsto (fun s => s.sum fun b => f b) atTop (𝓝 g)
ha : Filter.Tendsto ((fun b => a + b) ∘ fun s => s.sum fun b => f b) atTop (𝓝 (a + g))
⊢ ∀ (x : Finset ℕ), ((fun z => a + z) ∘ fun N => N.sum f) x = ((fun N => N.sum (Stream'.cons a f)) ∘ push) x
Tactic:
intro N
State after:
case h
X : Type
inst✝ : NormedAddCommGroup X
a g : X
f : ℕ → X
h : Filter.Tendsto (fun s => s.sum fun b => f b) atTop (𝓝 g)
ha : Filter.Tendsto ((fun b => a + b) ∘ fun s => s.sum fun b => f b) atTop (𝓝 (a + g))
N : Finset ℕ
⊢ ((fun z => a + z) ∘ fun N => N.sum f) N = ((fun N => N.sum (Stream'.cons a f)) ∘ push) N

State before:
case h
X : Type
inst✝ : NormedAddCommGroup X
a g : X
f : ℕ → X
h : Filter.Tendsto (fun s => s.sum fun b => f b) atTop (𝓝 g)
ha : Filter.Tendsto ((fun b => a + b) ∘ fun s => s.sum fun b => f b) atTop (𝓝 (a + g))
N : Finset ℕ
⊢ ((fun z => a + z) ∘ fun N => N.sum f) N = ((fun N => N.sum (Stream'.cons a f)) ∘ push) N
Tactic:
simp
State after:
case h
X : Type
inst✝ : NormedAddCommGroup X
a g : X
f : ℕ → X
h : Filter.Tendsto (fun s => s.sum fun b => f b) atTop (𝓝 g)
ha : Filter.Tendsto ((fun b => a + b) ∘ fun s => s.sum fun b => f b) atTop (𝓝 (a + g))
N : Finset ℕ
⊢ a + N.sum f = (push N).sum (Stream'.cons a f)

State before:
case h
X : Type
inst✝ : NormedAddCommGroup X
a g : X
f : ℕ → X
h : Filter.Tendsto (fun s => s.sum fun b => f b) atTop (𝓝 g)
ha : Filter.Tendsto ((fun b => a + b) ∘ fun s => s.sum fun b => f b) atTop (𝓝 (a + g))
N : Finset ℕ
⊢ a + N.sum f = (push N).sum (Stream'.cons a f)
Tactic:
exact push_sum
State after:
no goals