Borel sets in Lp spaces

DefinitionFunctions with vanishing integrals over \((0, L)\)#✓fully proved

For \(0 \le p \le \infty\), this is the set of real-valued \(f \in L^p(\mathbb{R})\) (with respect to Lebesgue measure) such that \(\int_{[0, L]} f(x)\,dx \to 0\) as \(L \to +\infty\), where the integral of a function that is not integrable on \([0, L]\) counts as \(0\).

def vanishingIntegralSet (p : ENNReal) : Set (Lp ℝ p (volume : Measure ℝ)) :=
  {f |
    Tendsto
      (fun L : ℝ => ∫ x in Set.Icc (0 : ℝ) L, f x ∂(volume : Measure ℝ))
      atTop (nhds 0)}

Used by 1

Used by\(L^p\) functions whose integrals over \((0, L)\) tend to \(0\) form a Borel set

Theorem\(L^p\) functions whose integrals over \((0, L)\) tend to \(0\) form a Borel set#●ready to prove

Let \(1 \le p \le \infty\). The set of real-valued \(f \in L^p(\mathbb{R})\) (with respect to Lebesgue measure) such that \(\int_0^L f(x)\,dx \to 0\) as \(L \to +\infty\) is a Borel subset of \(L^p(\mathbb{R})\).

public theorem_wanted measurableSet_vanishingIntegralSet
  (p : ENNReal)
  [Fact ((1 : ENNReal) ≤ p)] :
  @MeasurableSet (Lp ℝ p (volume : Measure ℝ))
    (borel (Lp ℝ p (volume : Measure ℝ)))
    (vanishingIntegralSet p)

Sources

• MA-ProofBench (L. Pu et al., arXiv:2606.13782), Level II (Measure and integration; Set functions, measures and integrals with values in abstract spaces), problem ma_proofbench_l2_25.

Uses 1

Statement usesFunctions with vanishing integrals over \((0, L)\)

1 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.