OAI/Analysis/PlanarEndpoint/FrequencyWeak.lean
9 declarations, 0 contain sorry, 0 declared as axioms
Gaussian regularization, Fourier evolution and endpoint maximal estimates.
- lemma
OAI.PlanarEndpoint.memLp_comp_real_smulline 13 - def
OAI.PlanarEndpoint.inverseFrequencyline 20 - lemma
OAI.PlanarEndpoint.fourier_inverseFrequency_aeline 25 - lemma
OAI.PlanarEndpoint.inverseFrequency_normline 35 - def
OAI.PlanarEndpoint.frequencyExtensionline 50 - lemma
OAI.PlanarEndpoint.evolution_inverseFrequencyline 53 - lemma
OAI.PlanarEndpoint.continuous_frequencyExtensionline 63 - lemma
OAI.PlanarEndpoint.norm_frequencyExtensionline 74 - lemma
OAI.PlanarEndpoint.frequency_weak_of_shortTimeline 81