English
If a finite set s is pairwise distinct in norms of f(i), then the NNNorm of the product equals the supremum of the NNNorms of the factors.
Русский
Если в конечном наборе s нормы элементов f(i) попарно различны, то nnnorm произведения равна supremum норм элементов.
LaTeX
$$$\\text{If } s \\neq \\varnothing \\text{ and } (\\forall i \\neq j \\in s, \\|f(i)\\|_{+} \\neq \\|f(j)\\|_{+}):\\, \\|\\prod_{i \\in s} f(i)\\|_{nn} = s.sup' (\\|f(i)\\|_{nn})$$$
Lean4
@[to_additive]
theorem nnnorm_prod_eq_sup_of_pairwise_ne {s : Finset ι} {f : ι → M} (hs : Set.Pairwise s (fun i j ↦ ‖f i‖₊ ≠ ‖f j‖₊)) :
‖∏ i ∈ s, f i‖₊ = s.sup (fun i ↦ ‖f i‖₊) := by
induction s using Finset.cons_induction with
| empty => simp
| cons a s ha IH =>
rcases s.eq_empty_or_nonempty with rfl | hs'
· simp
specialize IH (hs.mono (by simp))
obtain ⟨j, hj, hj'⟩ : ∃ j ∈ s, ‖∏ i ∈ s, f i‖₊ = ‖f j‖₊ := by simpa [IH] using s.exists_mem_eq_sup hs' _
suffices ‖f a‖₊ ≠ ‖∏ x ∈ s, f x‖₊ by simp [← IH, nnnorm_mul_eq_max_of_nnnorm_ne_nnnorm this]
rw [hj']
apply hs <;> grind
