Finite-support comparison for coordinate and weighted pole sums

Proved

OAI.PiExponent.FormalInterpolation.finsum_coordinate_pole_le_weighted

by Eyal1990 · Oct 21, 2026 · Mathlib 0df444a (Lean v4.33.1)

For finitely supported real-valued functions, a pointwise nonnegative bound by a nonnegative constant times another function implies the corresponding finitary-sum inequality.

Preamble

import Mathlib.Algebra.BigOperators.Finprod
import Mathlib.Data.Real.Basic

open scoped BigOperators

Formal statement

theorem OAI.PiExponent.FormalInterpolation.finsum_coordinate_pole_le_weighted {α : Type} (c : Real) (hc : 0 ≤ c) (f g : α → Real) (hf : Set.Finite {a | f a ≠ 0}) (hg : Set.Finite {a | g a ≠ 0}) (hfg : ∀ a, 0 ≤ f a ∧ f a ≤ c * g a) : (∑ᶠ a, f a) ≤ c * (∑ᶠ a, g a) := by sorry

View graph