English
For a continuous linear equivalence e and f, the equation tsum_L (e ∘ f) = y holds iff tsum_L f = e.symm y.
Русский
Для непрерывного линейного эквивалента e и функции f выражение tsum_L( e ∘ f ) = y эквивалентно tsum_L f = e.symm y.
LaTeX
$$$\\forall f:\\, ι \\to M\\; (e:\\, M \\simeq\\!\u2060SL[σ] M₂),\\; \\forall y:\\, M₂,\\ (\\operatorname{tsum}_L (λ z, e(f(z)))) = y \\\\iff \\operatorname{tsum}_L f = e.symm y$$$
Lean4
theorem tsum_eq_iff [T2Space M] [T2Space M₂] {f : ι → M} (e : M ≃SL[σ] M₂) {y : M₂} :
(∑'[L] z, e (f z)) = y ↔ ∑'[L] z, f z = e.symm y :=
by
by_cases hf : Summable f L
· by_cases hL : L.NeBot
·
exact
⟨fun h ↦ (e.hasSum.mp ((e.summable.mpr hf).hasSum_iff.mpr h)).tsum_eq, fun h ↦
(e.hasSum.mpr (hf.hasSum_iff.mpr h)).tsum_eq⟩
· simp only [tsum_bot hL, eq_symm_apply]
constructor <;> rintro rfl
exacts [e.map_finsum f, (e.map_finsum f).symm]
· have hf' : ¬Summable (fun z ↦ e (f z)) L := fun h ↦ hf (e.summable.mp h)
rw [tsum_eq_zero_of_not_summable hf, tsum_eq_zero_of_not_summable hf']
refine ⟨?_, fun H ↦ ?_⟩
· rintro rfl
simp
· simpa using congr_arg (fun z ↦ e z) H
