English
For real vector spaces, FiniteDimensional.proper holds, giving proper spaces for real finite-dimensional vector spaces.
Русский
Для вещественных пространств конечномерность гарантирует корректность пространства.
LaTeX
$$$[FiniteDimensional \\; Real \\; E] \\\\Rightarrow ProperSpace E$$$
Lean4
/-- In a finite-dimensional vector space over `ℝ`, the series `∑ x, ‖f x‖` is unconditionally
summable if and only if the series `∑ x, f x` is unconditionally summable. One implication holds in
any complete normed space, while the other holds only in finite-dimensional spaces. -/
theorem summable_norm_iff {α E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {f : α → E} :
(Summable fun x => ‖f x‖) ↔ Summable f :=
by
refine
⟨Summable.of_norm, fun hf ↦ ?_⟩
-- First we use a finite basis to reduce the problem to the case `E = Fin N → ℝ`
suffices ∀ {N : ℕ} {g : α → Fin N → ℝ}, Summable g → Summable fun x => ‖g x‖
by
obtain v := Module.finBasis ℝ E
set e := v.equivFunL
have H : Summable fun x => ‖e (f x)‖ := this (e.summable.2 hf)
refine .of_norm_bounded (H.mul_left ↑‖(e.symm : (Fin (finrank ℝ E) → ℝ) →L[ℝ] E)‖₊) fun i ↦ ?_
simpa using (e.symm : (Fin (finrank ℝ E) → ℝ) →L[ℝ] E).le_opNorm (e <| f i)
clear! E
intro N g hg
have : ∀ i, Summable fun x => ‖g x i‖ := fun i => (Pi.summable.1 hg i).abs
refine .of_norm_bounded (summable_sum fun i (_ : i ∈ Finset.univ) => this i) fun x => ?_
rw [norm_norm, pi_norm_le_iff_of_nonneg]
· refine fun i => Finset.single_le_sum (f := fun i => ‖g x i‖) (fun i _ => ?_) (Finset.mem_univ i)
exact norm_nonneg (g x i)
· exact Finset.sum_nonneg fun _ _ => norm_nonneg _
