OAI/Analysis/PlanarEndpoint/UnitScaling.lean
8 declarations, 0 contain sorry, 0 declared as axioms
Gaussian regularization, Fourier evolution and endpoint maximal estimates.
- def
OAI.PlanarEndpoint.unitFrequencyInputline 16 - lemma
OAI.PlanarEndpoint.unitFrequencyInput_memLpline 19 - lemma
OAI.PlanarEndpoint.norm_unitFrequencyInputline 28 - lemma
OAI.PlanarEndpoint.unitFrequencyInput_supportline 32 - lemma
OAI.PlanarEndpoint.unitFrequencyInput_normline 47 - lemma
OAI.PlanarEndpoint.phase_unitFrequency_scalingline 64 - lemma
OAI.PlanarEndpoint.evolution_unitFrequency_scalingline 75 - lemma
OAI.PlanarEndpoint.norm_evolution_unitFrequency_scalingline 95