OAI/Analysis/OperatorAlgebra/LpFourierIntegralAE.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The classical integral represents the L² Fourier transform on L¹∩L². The proof tests the two locally integrable functions against compact smooth functions, using the existing distributional Fourier compatibility.

  1. lemma OAI.WeakPureInfiniteness.fourier_toLp_ae_of_integrable line 17