Uniform finite envelope for compactly supported nonnegative continuous tests

Proved

AvramDividend.Classical.compactTest_nnreal_uniformBound_finiteLintegral

by WillR · Oct 25, 2026 · Mathlib 0df444a (Lean v4.33.1)

compactly-supported-functionsfinite-measuresstrong-markovuniform-bound

Any compactly supported continuous NNReal-valued test function admits the explicit finite uniform bound given by its distance from zero in the bounded-continuous-function space; when the underlying measure has finite mass, this constant bound has finite lower integral.

Preamble

import Mathlib.MeasureTheory.Integral.BoundedContinuousFunction
import Mathlib.Topology.ContinuousMap.CompactlySupported
import Mathlib.MeasureTheory.Integral.Lebesgue.Basic

open MeasureTheory
open scoped NNReal ENNReal

Formal statement

theorem AvramDividend.Classical.compactTest_nnreal_uniformBound_finiteLintegral
    {Ω Y : Type*} [MeasurableSpace Ω] [TopologicalSpace Y]
    (P : Measure Ω) (hP : P Set.univ ≠ ⊤)
    (f : CompactlySupportedContinuousMap Y ℝ≥0) :
    (∀ y : Y,
      ((f y : ℝ≥0) : ℝ≥0∞) ≤
      ((nndist (0 : BoundedContinuousFunction Y ℝ≥0)
        f.toBoundedContinuousFunction : ℝ≥0) : ℝ≥0∞)) ∧
    (∫⁻ _ : Ω,
      ((nndist (0 : BoundedContinuousFunction Y ℝ≥0)
        f.toBoundedContinuousFunction : ℝ≥0) : ℝ≥0∞) ∂P) ≠ ⊤ := by
  sorry

Source

Supplies the bound and finite-envelope hypotheses needed to apply the accepted finite-stopping cylinder-reward scalar strong Markov theorem 923863b7-543e-4ddf-8e26-f7249d48d98c to the compact tests defining finite-coordinate path-law uniqueness.

View graph