Reverse Hölder inequality

AbbreviationLebesgue measure on the unit interval#✓fully proved

The measure on \(\mathbb{R}\) that assigns to each set \(A \subseteq \mathbb{R}\) the Lebesgue measure of \(A \cap [0,1]\).

noncomputable abbrev μIcc01 : Measure ℝ :=
  volume.restrict (Set.Icc (0 : ℝ) 1)

Used by 1

Used byUniformly large level sets under a reverse Hölder bound

TheoremUniformly large level sets under a reverse Hölder bound#●ready to prove

Let \(\mu\) be Lebesgue measure on \([0,1]\), and let \(f_0, f_1, f_2, \ldots : \mathbb{R} \to \mathbb{R}\) lie in \(L^2(\mu)\) with \(\|f_n\|_{L^2(\mu)} \le 2024\,\|f_n\|_{L^1(\mu)}\) for every \(n\) and \(\|f_n\|_{L^1(\mu)} \to \infty\) as \(n \to \infty\). Then there is a sequence of real numbers \(y_n \to \infty\) such that

\[ \inf_n \mu(\{x : |f_n(x)| \ge y_n\}) > 0. \]

The divergence hypothesis is the limit \(\|f_n\|_{L^1(\mu)} \to \infty\) in \([0,\infty]\); the formal source instead required \(\|f_n\|_{L^1(\mu)} = \infty\) for all large \(n\), which no function in \(L^2(\mu)\) satisfies, so its statement was vacuous.

public theorem_wanted exists_tendsto_atTop_inf_measure_levelSet_pos
    (f : ℕ → ℝ → ℝ)
    (hf_L2 : ∀ n : ℕ, MemLp (f n) 2 μIcc01)
    (hbound : ∀ n : ℕ,
      eLpNorm (f n) 2 μIcc01 ≤
        ENNReal.ofReal 2024 * eLpNorm (f n) 1 μIcc01)
    (hL1_div : Tendsto (fun n : ℕ => eLpNorm (f n) 1 μIcc01) atTop (nhds ⊤)) :
    ∃ y : ℕ → ℝ,
      Tendsto y atTop atTop ∧
      0 < sInf (Set.range (fun n : ℕ =>
        μIcc01 {x : ℝ | |f n x| ≥ y n}))

Sources

• MA-ProofBench (L. Pu et al., arXiv:2606.13782), Level II (Measure and integration; Classical measure theory), problem ma_proofbench_l2_04, with the change above.

Uses 1

Statement usesLebesgue measure on the unit interval

1 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.