apply_sum_le_sup_of_isNonarchimedean

English

Ultrametric inequality for Finite sums: f(∑_{i∈s} l(i)) ≤ sup'_{i∈s} f(l(i)).

Русский

Ультраметрическое неравенство для конечной суммы: f(∑ l(i)) ≤ sup_{i∈s} f(l(i)).

LaTeX

$$$f\\Big(\\sum_{i\\in s} l(i)\\Big) \\le s^{\\prime}\\!\\!\\! \\sup_{i\\in s} f(l(i))$$$

Lean4

/-- Ultrametric inequality with `Finset.sum`. -/
theorem apply_sum_le_sup_of_isNonarchimedean {α β : Type*} [AddCommMonoid α] {f : α → R} (nonarch : IsNonarchimedean f)
    {s : Finset β} (hnonempty : s.Nonempty) {l : β → α} : f (∑ i ∈ s, l i) ≤ s.sup' hnonempty fun i => f (l i) := by
  induction hnonempty using Nonempty.cons_induction with
  | singleton i => simp
  | cons i s _ hs hind =>
    simp only [sum_cons, le_sup'_iff, mem_cons, exists_eq_or_imp]
    rw [← le_sup'_iff hs]
    rcases le_max_iff.mp <| nonarch (l i) (∑ i ∈ s, l i) with h₁ | h₂
    · exact .inl h₁
    · exact .inr <| le_trans h₂ hind

Похожие утверждения