OAI/Analysis/ModularRecovery/FourierLocalization.lean

GitHub source file

38 declarations, 0 contain sorry, 0 declared as axioms

Polar truncation and Fourier localization with a width-independent L1 bound.

  1. lemma OAI.BoundedRecovery.polarCutoff_vector_error_sq line 17
  2. lemma OAI.BoundedRecovery.norm_polarCutoff_vector_le line 24
  3. lemma OAI.BoundedRecovery.RealSpectralCalculus.norm_unitary_le_one line 37
  4. def OAI.BoundedRecovery.RealSpectralCalculus.integratedUnitary line 42
  5. lemma OAI.BoundedRecovery.RealSpectralCalculus.integral_character_mul line 45
  6. lemma OAI.BoundedRecovery.RealSpectralCalculus.calculus_eq_integratedUnitary line 68
  7. lemma OAI.BoundedRecovery.RealSpectralCalculus.calculus_apply_eq_integral line 91
  8. def OAI.BoundedRecovery.StandardModularData.fourierFilter line 101
  9. lemma OAI.BoundedRecovery.StandardModularData.norm_fourierFilter_le line 106
  10. lemma OAI.BoundedRecovery.StandardModularData.fourierFilter_mem line 110
  11. lemma OAI.BoundedRecovery.StandardModularData.fourierFilter_apply_xi line 127
  12. def OAI.BoundedRecovery.bump0 line 143
  13. def OAI.BoundedRecovery.bumpSchwartz line 145
  14. lemma OAI.BoundedRecovery.bumpSchwartz_apply line 153
  15. def OAI.BoundedRecovery.baseKernel line 156
  16. lemma OAI.BoundedRecovery.baseKernel_integrable line 158
  17. lemma OAI.BoundedRecovery.bump0_fourier line 160
  18. def OAI.BoundedRecovery.bandMultiplier line 179
  19. lemma OAI.BoundedRecovery.bandMultiplier_apply line 187
  20. lemma OAI.BoundedRecovery.norm_bandMultiplier_le line 190
  21. lemma OAI.BoundedRecovery.bandMultiplier_one line 196
  22. lemma OAI.BoundedRecovery.bandMultiplier_zero line 205
  23. def OAI.BoundedRecovery.bandKernel line 218
  24. lemma OAI.BoundedRecovery.norm_bandKernel line 221
  25. lemma OAI.BoundedRecovery.bandKernel_integrable line 225
  26. lemma OAI.BoundedRecovery.integral_norm_bandKernel line 233
  27. lemma OAI.BoundedRecovery.bandMultiplier_fourier line 240
  28. def OAI.BoundedRecovery.filterL1 line 270
  29. lemma OAI.BoundedRecovery.filterL1_nonneg line 271
  30. def OAI.BoundedRecovery.StandardModularData.bandFilter line 275
  31. lemma OAI.BoundedRecovery.StandardModularData.bandFilter_mem line 279
  32. lemma OAI.BoundedRecovery.StandardModularData.norm_bandFilter_le line 283
  33. lemma OAI.BoundedRecovery.StandardModularData.bandFilter_apply_xi line 289
  34. lemma OAI.BoundedRecovery.StandardModularData.bandFilter_support line 293
  35. lemma OAI.BoundedRecovery.StandardModularData.bandMultiplier_fixes line 299
  36. lemma OAI.BoundedRecovery.StandardModularData.bandMultiplier_contracts line 303
  37. lemma OAI.BoundedRecovery.StandardModularData.bandFilter_vector_error_le line 310
  38. lemma OAI.BoundedRecovery.StandardModularData.exists_band_representative line 317