Theorem: HasSum.antidiagonal_of_2d (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 : ℝ
f : ℕ × ℕ → E
a : E
h : HasSum f a
⊢ HasSum (fun n => (Finset.range (n + 1)).sum fun n1 => f (n1, n - n1)) a
Tactic:
generalize hg : (fun n ↦ (Finset.range (n + 1)).sum fun n1 ↦ f (n1, n - n1)) = g
State after:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f✝ : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r b : ℝ
f : ℕ × ℕ → E
a : E
h : HasSum f a
g : ℕ → E
hg : (fun n => (Finset.range (n + 1)).sum fun n1 => f (n1, n - n1)) = g
⊢ HasSum g a

State before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f✝ : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r b : ℝ
f : ℕ × ℕ → E
a : E
h : HasSum f a
g : ℕ → E
hg : (fun n => (Finset.range (n + 1)).sum fun n1 => f (n1, n - n1)) = g
⊢ HasSum g a
Tactic:
rw [←Finset.sigmaAntidiagonalEquivProd.hasSum_iff] at h
State after:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f✝ : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r b : ℝ
f : ℕ × ℕ → E
a : E
h : HasSum (f ∘ ⇑Finset.sigmaAntidiagonalEquivProd) a
g : ℕ → E
hg : (fun n => (Finset.range (n + 1)).sum fun n1 => f (n1, n - n1)) = g
⊢ HasSum g a

State before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f✝ : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r b : ℝ
f : ℕ × ℕ → E
a : E
h : HasSum (f ∘ ⇑Finset.sigmaAntidiagonalEquivProd) a
g : ℕ → E
hg : (fun n => (Finset.range (n + 1)).sum fun n1 => f (n1, n - n1)) = g
⊢ HasSum g a
Tactic:
have fg : ∀ n, HasSum (fun d : Finset.antidiagonal n ↦
    (f ∘ Finset.sigmaAntidiagonalEquivProd) ⟨n, d⟩) (g n) := by
  intro n; simp only [Function.comp_apply, Finset.sigmaAntidiagonalEquivProd_apply]
  have fs := hasSum_fintype fun d : ↥(Finset.antidiagonal n) ↦ f ↑d
  have e : (Finset.univ.sum fun d : ↥(Finset.antidiagonal n) ↦ f ↑d) = g n := by
    rw [Finset.sum_coe_sort, Finset.Nat.sum_antidiagonal_eq_sum_range_succ_mk, ← hg]
  rwa [← e]
State after:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f✝ : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r b : ℝ
f : ℕ × ℕ → E
a : E
h : HasSum (f ∘ ⇑Finset.sigmaAntidiagonalEquivProd) a
g : ℕ → E
hg : (fun n => (Finset.range (n + 1)).sum fun n1 => f (n1, n - n1)) = g
fg : ∀ (n : ℕ), HasSum (fun d => (f ∘ ⇑Finset.sigmaAntidiagonalEquivProd) ⟨n, d⟩) (g n)
⊢ HasSum g a

State before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f✝ : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r b : ℝ
f : ℕ × ℕ → E
a : E
h : HasSum (f ∘ ⇑Finset.sigmaAntidiagonalEquivProd) a
g : ℕ → E
hg : (fun n => (Finset.range (n + 1)).sum fun n1 => f (n1, n - n1)) = g
fg : ∀ (n : ℕ), HasSum (fun d => (f ∘ ⇑Finset.sigmaAntidiagonalEquivProd) ⟨n, d⟩) (g n)
⊢ HasSum g a
Tactic:
exact HasSum.sigma h fg
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 : ℝ
f : ℕ × ℕ → E
a : E
h : HasSum (f ∘ ⇑Finset.sigmaAntidiagonalEquivProd) a
g : ℕ → E
hg : (fun n => (Finset.range (n + 1)).sum fun n1 => f (n1, n - n1)) = g
⊢ ∀ (n : ℕ), HasSum (fun d => (f ∘ ⇑Finset.sigmaAntidiagonalEquivProd) ⟨n, d⟩) (g n)
Tactic:
intro n
State after:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f✝ : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r b : ℝ
f : ℕ × ℕ → E
a : E
h : HasSum (f ∘ ⇑Finset.sigmaAntidiagonalEquivProd) a
g : ℕ → E
hg : (fun n => (Finset.range (n + 1)).sum fun n1 => f (n1, n - n1)) = g
n : ℕ
⊢ HasSum (fun d => (f ∘ ⇑Finset.sigmaAntidiagonalEquivProd) ⟨n, d⟩) (g n)

State before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f✝ : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r b : ℝ
f : ℕ × ℕ → E
a : E
h : HasSum (f ∘ ⇑Finset.sigmaAntidiagonalEquivProd) a
g : ℕ → E
hg : (fun n => (Finset.range (n + 1)).sum fun n1 => f (n1, n - n1)) = g
n : ℕ
⊢ HasSum (fun d => (f ∘ ⇑Finset.sigmaAntidiagonalEquivProd) ⟨n, d⟩) (g n)
Tactic:
simp only [Function.comp_apply, Finset.sigmaAntidiagonalEquivProd_apply]
State after:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f✝ : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r b : ℝ
f : ℕ × ℕ → E
a : E
h : HasSum (f ∘ ⇑Finset.sigmaAntidiagonalEquivProd) a
g : ℕ → E
hg : (fun n => (Finset.range (n + 1)).sum fun n1 => f (n1, n - n1)) = g
n : ℕ
⊢ HasSum (fun d => f ↑d) (g n)

State before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f✝ : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r b : ℝ
f : ℕ × ℕ → E
a : E
h : HasSum (f ∘ ⇑Finset.sigmaAntidiagonalEquivProd) a
g : ℕ → E
hg : (fun n => (Finset.range (n + 1)).sum fun n1 => f (n1, n - n1)) = g
n : ℕ
⊢ HasSum (fun d => f ↑d) (g n)
Tactic:
have fs := hasSum_fintype fun d : ↥(Finset.antidiagonal n) ↦ f ↑d
State after:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f✝ : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r b : ℝ
f : ℕ × ℕ → E
a : E
h : HasSum (f ∘ ⇑Finset.sigmaAntidiagonalEquivProd) a
g : ℕ → E
hg : (fun n => (Finset.range (n + 1)).sum fun n1 => f (n1, n - n1)) = g
n : ℕ
fs : HasSum (fun d => f ↑d) (Finset.univ.sum fun b => f ↑b)
⊢ HasSum (fun d => f ↑d) (g n)

State before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f✝ : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r b : ℝ
f : ℕ × ℕ → E
a : E
h : HasSum (f ∘ ⇑Finset.sigmaAntidiagonalEquivProd) a
g : ℕ → E
hg : (fun n => (Finset.range (n + 1)).sum fun n1 => f (n1, n - n1)) = g
n : ℕ
fs : HasSum (fun d => f ↑d) (Finset.univ.sum fun b => f ↑b)
⊢ HasSum (fun d => f ↑d) (g n)
Tactic:
have e : (Finset.univ.sum fun d : ↥(Finset.antidiagonal n) ↦ f ↑d) = g n := by
  rw [Finset.sum_coe_sort, Finset.Nat.sum_antidiagonal_eq_sum_range_succ_mk, ← hg]
State after:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f✝ : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r b : ℝ
f : ℕ × ℕ → E
a : E
h : HasSum (f ∘ ⇑Finset.sigmaAntidiagonalEquivProd) a
g : ℕ → E
hg : (fun n => (Finset.range (n + 1)).sum fun n1 => f (n1, n - n1)) = g
n : ℕ
fs : HasSum (fun d => f ↑d) (Finset.univ.sum fun b => f ↑b)
e : (Finset.univ.sum fun d => f ↑d) = g n
⊢ HasSum (fun d => f ↑d) (g n)

State before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f✝ : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r b : ℝ
f : ℕ × ℕ → E
a : E
h : HasSum (f ∘ ⇑Finset.sigmaAntidiagonalEquivProd) a
g : ℕ → E
hg : (fun n => (Finset.range (n + 1)).sum fun n1 => f (n1, n - n1)) = g
n : ℕ
fs : HasSum (fun d => f ↑d) (Finset.univ.sum fun b => f ↑b)
e : (Finset.univ.sum fun d => f ↑d) = g n
⊢ HasSum (fun d => f ↑d) (g n)
Tactic:
rwa [← e]
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 : ℝ
f : ℕ × ℕ → E
a : E
h : HasSum (f ∘ ⇑Finset.sigmaAntidiagonalEquivProd) a
g : ℕ → E
hg : (fun n => (Finset.range (n + 1)).sum fun n1 => f (n1, n - n1)) = g
n : ℕ
fs : HasSum (fun d => f ↑d) (Finset.univ.sum fun b => f ↑b)
⊢ (Finset.univ.sum fun d => f ↑d) = g n
Tactic:
rw [Finset.sum_coe_sort, Finset.Nat.sum_antidiagonal_eq_sum_range_succ_mk, ← hg]
State after:
no goals