English
For f: ι → α into a complete normed group with absolute value, the summability of |f| is equivalent to the summability of f itself.
Русский
Для f: ι → α в полной нормированной группе с модулем преобладающим, суммируемость |f| эквивалентна суммируемости f.
LaTeX
$$$\\\\mathrm{Multipliable}(i \\mapsto |f(i)|) \\\\iff \\\\mathrm{Multipliable}(f)$$$
Lean4
@[to_additive]
theorem multipliable_mabs_iff [CommGroup α] [LinearOrder α] [IsOrderedMonoid α] [UniformSpace α] [IsUniformGroup α]
[CompleteSpace α] {f : ι → α} : (Multipliable fun x ↦ mabs (f x)) ↔ Multipliable f :=
let s := {x | 1 ≤ f x}
have h1 : ∀ x : s, mabs (f x) = f x := fun x ↦ mabs_of_one_le x.2
have h2 : ∀ x : ↑sᶜ, mabs (f x) = (f x)⁻¹ := fun x ↦ mabs_of_lt_one (not_le.1 x.2)
calc
(Multipliable fun x ↦ mabs (f x)) ↔ (Multipliable fun x : s ↦ mabs (f x)) ∧ Multipliable fun x : ↑sᶜ ↦ mabs (f x) :=
multipliable_subtype_and_compl.symm
_ ↔ (Multipliable fun x : s ↦ f x) ∧ Multipliable fun x : ↑sᶜ ↦ (f x)⁻¹ := by simp only [h1, h2]
_ ↔ Multipliable f := by simp only [multipliable_inv_iff, multipliable_subtype_and_compl]
