English
For a family f : ι → M, the norm of the infinite tensor/finite product tprod is bounded by the supremum of the norms: ‖∏' i, f i‖ ≤ sup_i ‖f i‖.
Русский
Для семейства f: ι → M норма бесконечного/конечного произведения tprod не превосходит супремума норм: ‖∏' i, f i‖ ≤ sup_i ‖f i‖.
LaTeX
$$$\\|\\prod' i, f(i)\\| \\le \\big\\lVert \\sup_i \\|f(i)\\| \\big\\rVert$$$
Lean4
@[to_additive]
theorem norm_tprod_le (f : ι → M) : ‖∏' i, f i‖ ≤ ⨆ i, ‖f i‖ :=
by
rcases isEmpty_or_nonempty ι with hι | hι
· -- Silly case #1 : the index type is empty
simp only [tprod_empty, norm_one', Real.iSup_of_isEmpty, le_refl]
by_cases h : Multipliable f; swap
· -- Silly case #2 : the product is divergent
rw [tprod_eq_one_of_not_multipliable h, norm_one']
by_cases h_bd : BddAbove (Set.range fun i ↦ ‖f i‖)
· exact le_ciSup_of_le h_bd hι.some (norm_nonneg' _)
·
rw [Real.iSup_of_not_bddAbove h_bd]
-- now the interesting case
have h_bd : BddAbove (Set.range fun i ↦ ‖f i‖) := h.tendsto_cofinite_one.norm'.bddAbove_range_of_cofinite
refine le_of_tendsto' h.hasProd.norm' (fun s ↦ norm_prod_le_of_forall_le_of_nonneg ?_ ?_)
· exact le_ciSup_of_le h_bd hι.some (norm_nonneg' _)
· exact fun i _ ↦ le_ciSup h_bd i
