No bounded projection from L^1 onto H^1

H1_not_closedComplemented

Submitter: Yongxi Lin.

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! 🐙

Solved by

• @GanjinZero with Seed Prover (ByteDance) on Jun 24, 2026