A $\sigma$ -finite measure has an everywhere positive measurable function in $L^p$ , $0<p<\infty$

Proved

CauchyRiemannIndex.exists_pos_memLp_weight

by Mazecto · Oct 13, 2026 · Mathlib 0df444a (Lean v4.33.1)

lp-spacesmeasure-theorysigma-finite

Let $\mu$ be a $\sigma$ -finite measure on $\alpha$ and $0<p<\infty$ . Then there is a measurable $w:\alpha\to\mathbb R$ with

w(x)>0\ \text{ for every } x\in\alpha,\qquad w\in L^p(\mu).

Such a weight turns a $\sigma$ -finite measure into the finite measure $|w|^p\mu$ with the same null sets. It is used to reduce statements about $\sigma$ -finite measures to finite ones.

Formalization Note. $p\in$ ℝ≥0∞ with $p\ne0$ , $p\ne\infty$ ; the conclusion is ∃ w : α → ℝ, (∀ x, 0 < w x) ∧ Measurable w ∧ MemLp w p μ.

Preamble

import Mathlib.MeasureTheory.Function.LpSpace.Basic
import Mathlib.MeasureTheory.Integral.Lebesgue.Countable
import Mathlib.MeasureTheory.Integral.Lebesgue.DominatedConvergence

Formal statement

namespace CauchyRiemannIndex

open MeasureTheory Filter Topology
open scoped ENNReal NNReal

/-- A σ-finite measure admits an everywhere positive measurable weight in `L^p`, `0 < p < ∞`. -/
theorem exists_pos_memLp_weight {α : Type*} [MeasurableSpace α] (μ : Measure α) [SigmaFinite μ]
    {p : ℝ≥0∞} (hp0 : p ≠ 0) (hp : p ≠ ⊤) :
    ∃ w : α → ℝ, (∀ x, 0 < w x) ∧ Measurable w ∧ MemLp w p μ := by
  sorry

end CauchyRiemannIndex

Source

G. B. Folland, Real Analysis, 2nd ed., Wiley 1999, Exercise 2.14 / proof of Theorem 6.15, p. 191

View graph

A σ\sigmaσ-finite measure has an everywhere positive measurable function in LpL^pLp, 0<p<∞0<p<\infty0<p<∞

A $\sigma$ -finite measure has an everywhere positive measurable function in $L^p$ , $0<p<\infty$