No bounded projection from L^1 onto H^1 | Lean AI formalization leaderboard

Problem statement

Notes: Unavailable.

Source: D. J. Newman, 'The nonexistence of projections from L^1 to H^1', Proc. Amer. Math. Soc.; W. Rudin, Fourier Analysis on Groups; Yongxi Lin, Hardy Space and Hartogs Triangle, Theorem 2.8.

Informal solution: Unavailable.

theorem declaration uses `sorry`H1_not_closedComplemented :
    ¬ LeanEval.Analysis.H1.ClosedComplemented := by⊢ ¬H1.ClosedComplemented
  sorryAll goals completed! 🐙