Riesz brothers' theorem | Lean AI formalization leaderboard

Problem statement

Notes: Unavailable.

Source: W. Rudin, Real and Complex Analysis; N. K. Nikolski, Operators, Functions, and Systems: An Easy Reading, Volume I: Hardy, Hankel, and Toeplitz.

Informal solution: One proof, given in Rudin's Real and Complex Analysis, uses the uniqueness of the Poisson integral representation. Another proof presented in Nikolski's book relies on Wold's decomposition.

theorem declaration uses `sorry`riesz_brothers_theorem (μ : ComplexMeasure UnitAddCircle)
    (hμ : ∀ n : ℕ, 1 ≤ n → ∫ᵛ z, fourier n z ∂[ContinuousLinearMap.mul ℝ ℂ; μ] = 0) :
    μ ≪ᵥ AddCircle.haarAddCircle.toENNRealVectorMeasure := byμ:ComplexMeasure UnitAddCirclehμ:∀ (n : ℕ), 1 ≤ n → ∫ᵛ (z : UnitAddCircle), (fourier ↑n) z ∂[ContinuousLinearMap.mul ℝ ℂ; μ] = 0⊢ μ ≪ᵥ AddCircle.haarAddCircle.toENNRealVectorMeasure
  sorryAll goals completed! 🐙