ThmDex – An index of mathematical definitions, results, and conjectures.
Result R3532 on D2948: Sublevel set
Tautological pointwise lower bound from indicator function on sublevel set
Formulation 0
Let $f : X \to [- \infty, \infty]$ be a D3180: Basic function.
Let $g : X \to [0, \infty]$ be an D4361: Unsigned basic function.
Then \begin{equation} f I_{\{ f < g \}} \leq g \end{equation}
Proofs
Proof 0
Let $f : X \to [- \infty, \infty]$ be a D3180: Basic function.
Let $g : X \to [0, \infty]$ be an D4361: Unsigned basic function.
Since $g$ is unsigned, result R3531: Pointwise product with indicator function is lower bound for unsigned basic function shows that $g I_{\{ f < g \}} \leq g$. Using R3529: Tautological pointwise inequality from indicator functions on sublevel sets, we then conclude \begin{equation} f I_{\{ f < g \}} \leq g I_{\{ f < g \}} \leq g \end{equation} $\square$