Prove2Me

Local scaled mass is bounded by the positive zero divisor

Proved
OAI.PiExponent.FormalInterpolation.polynomial_curve_mass_le_zero_divisor

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

For nonnegative mass on curve places, if each positive mass is locally bounded by r times the function’s order, then the total scaled mass is bounded by r times the total positive order, provided the positive-order support is finite.

Preamble
import Definitions.Def_OAI_PiExponent_LogarithmicWordContact

open scoped BigOperators
open OAI.PiExponent OAI.PiExponent.FormalInterpolation
Formal statement
theorem OAI.PiExponent.FormalInterpolation.polynomial_curve_mass_le_zero_divisor
    {E : Type} [Field E] [Algebra Complex E]
    (f : E) (a r : Real) (ha : 0 < a) (hr : 0 < r)
    (b : PolynomialCurvePlace E → Real) (hb : ∀ nu, 0 ≤ b nu)
    (hlocal : ∀ nu, 0 < b nu →
      a * b nu ≤ r * (polynomialCurveOrder nu f : Real))
    (hpositiveFinite :
      {nu : PolynomialCurvePlace E | 0 < polynomialCurveOrder nu f}.Finite) :
    a * (∑ᶠ nu : PolynomialCurvePlace E, b nu) ≤
      r * (∑ᶠ nu : PolynomialCurvePlace E,
        max (polynomialCurveOrder nu f : Real) 0) := by sorry

View graph