Prove2Me

A function on [0,1)[0,1) whose pairings with periodic continuous functions are L1L^1-bounded is essentially bounded

Proved
CauchyRiemannIndex.abs_le_of_forall_abs_integral_mul_le

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

dualitymeasure-theoryreal-analysis

Let h:R→Rh:\mathbb R\to\mathbb R be integrable on [0,1)[0,1) and let K∈RK\in\mathbb R. Suppose that

∣∫01φ(t) h(t) dt∣≤K∫01∣φ(t)∣ dt\Big|\int_0^1\varphi(t)\,h(t)\,dt\Big|\le K\int_0^1|\varphi(t)|\,dt

for every continuous 11-periodic function φ:R→R\varphi:\mathbb R\to\mathbb R. Then

∣h(t)∣≤Kfor almost every t∈[0,1).|h(t)|\le K\qquad\text{for almost every }t\in[0,1).

This is the elementary half of the duality L1(S1)∗=L∞(S1)L^1(S^1)^*=L^\infty(S^1), phrased with continuous periodic test functions: an L1L^1-bounded linear functional given by an integrable density has an essentially bounded density with the same bound. It converts weak L1→L∞L^1\to L^\infty estimates for periodic problems into pointwise almost-everywhere bounds.

Formalization Note. Integrals over [0,1)[0,1) are Lebesgue integrals over Set.Ico 0 1; the conclusion is an almost-everywhere statement for Lebesgue measure restricted to Set.Ico 0 1. No sign condition on KK is assumed.

Preamble
import Mathlib.Analysis.Calculus.BumpFunction.Convolution
import Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension
import Mathlib.Topology.Algebra.Order.Floor
import Mathlib.MeasureTheory.Integral.IntegrableOn
import Mathlib.MeasureTheory.Group.Integral
Formal statement
namespace CauchyRiemannIndex

open MeasureTheory

/-- Let `h : ℝ → ℝ` be integrable on `[0, 1)` and `K : ℝ`. If
`|∫₀¹ φ h| ≤ K ∫₀¹ |φ|` for every continuous `1`-periodic `φ : ℝ → ℝ`, then `|h t| ≤ K`
for almost every `t ∈ [0, 1)`. -/
theorem abs_le_of_forall_abs_integral_mul_le (h : ℝ → ℝ) (K : ℝ)
    (hh : IntegrableOn h (Set.Ico 0 1))
    (hK : ∀ φ : ℝ → ℝ, Continuous φ → Function.Periodic φ 1 →
      |∫ t in Set.Ico (0 : ℝ) 1, φ t * h t| ≤ K * ∫ t in Set.Ico (0 : ℝ) 1, |φ t|) :
    ∀ᵐ t ∂(volume.restrict (Set.Ico (0 : ℝ) 1)), |h t| ≤ K := by
  sorry

end CauchyRiemannIndex
Source
Standard L^1-L^infinity duality on the circle; see e.g. W. Rudin, Real and Complex Analysis, 3rd ed., Theorem 6.16

View graph