English
For a nonempty index type and a function f: indices → M, there exists i such that the norm of the product of the mapped multiset is bounded by ‖f(i)‖, with a conditional i ∈ t when t ≠ 0.
Русский
Для непустого типа индексов и функции f: индексы → M существует i, для которого ‖(s.map f).prod‖ ≤ ‖f(i)‖, при условии, что i ∈ s если s ≠ 0.
LaTeX
$$$\\exists i : ι, (s \\neq 0 \\rightarrow i \\in s) \\land \\left\\|\\left(s.map\\, f\\right).prod\\right\\| \\le \\|f(i)\\|$$$
Lean4
/-- Given a function `f : ι → M` and a multiset `t : Multiset ι`, we can always find `i : ι`, belonging
to `t` if `t` is nonempty, such that `‖(s.map f).prod‖ ≤ ‖f i‖`.
-/
@[to_additive /-- Given a function `f : ι → M` and a multiset `t : Multiset ι`, we can always find
`i : ι`, belonging to `t` if `t` is nonempty, such that `‖(s.map f).sum‖ ≤ ‖f i‖`. -/
]
theorem exists_norm_multiset_prod_le (s : Multiset ι) [Nonempty ι] {f : ι → M} :
∃ i : ι, (s ≠ 0 → i ∈ s) ∧ ‖(s.map f).prod‖ ≤ ‖f i‖ :=
by
inhabit ι
induction s using Multiset.induction_on with
| empty => simp
| cons a t hM =>
obtain ⟨M, hMs, hM⟩ := hM
by_cases hMa : ‖f M‖ ≤ ‖f a‖
· refine ⟨a, by simp, ?_⟩
· rw [Multiset.map_cons, Multiset.prod_cons]
exact le_trans (norm_mul_le_max _ _) (max_le (le_refl _) (le_trans hM hMa))
· rw [not_le] at hMa
rcases eq_or_ne t 0 with rfl | ht
· exact ⟨a, by simp, by simp⟩
· refine ⟨M, ?_, ?_⟩
· simp [hMs ht]
rw [Multiset.map_cons, Multiset.prod_cons]
exact le_trans (norm_mul_le_max _ _) (max_le hMa.le hM)
