OAI/MathematicalPhysics/Boltzmann/Collision/FourierCompactness.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

Finite-measure cutoffs of L2 Fourier data

  1. def OAI.BoltzmannNonuniqueness.Published.complexL2Cutoff line 16
  2. theorem OAI.BoltzmannNonuniqueness.Published.complexL2Cutoff_ae line 20
  3. theorem OAI.BoltzmannNonuniqueness.Published.complexL2Cutoff_norm_le line 25
  4. theorem OAI.BoltzmannNonuniqueness.Published.complexL2Cutoff_integrable line 32
  5. def OAI.BoltzmannNonuniqueness.Published.fourierBandApprox line 39
  6. theorem OAI.BoltzmannNonuniqueness.Published.fourierBandApprox_ae line 43
  7. def OAI.BoltzmannNonuniqueness.Published.fourierBandTest line 64
  8. theorem OAI.BoltzmannNonuniqueness.Published.fourierBandTest_memLp line 67
  9. theorem OAI.BoltzmannNonuniqueness.Published.fourierBandApprox_pairing line 78
  10. theorem OAI.BoltzmannNonuniqueness.Published.fourierBandApprox_tendsto line 92
  11. theorem OAI.BoltzmannNonuniqueness.Published.fourierBandTest_norm_sq line 118
  12. theorem OAI.BoltzmannNonuniqueness.Published.fourierBandApprox_norm_le line 130
  13. theorem OAI.BoltzmannNonuniqueness.Published.fourierBandApprox_continuous line 142
  14. theorem OAI.BoltzmannNonuniqueness.Published.fourierBandApprox_local_convergence line 162
  15. theorem OAI.BoltzmannNonuniqueness.Published.complexL2Cutoff_error line 211
  16. theorem OAI.BoltzmannNonuniqueness.Published.fourierBand_error line 221
  17. theorem OAI.BoltzmannNonuniqueness.Published.inverseFourier_norm line 250
  18. theorem OAI.BoltzmannNonuniqueness.Published.inverseFourier_sub line 253
  19. theorem OAI.BoltzmannNonuniqueness.Published.fourierReconstruction_error line 257
  20. theorem OAI.BoltzmannNonuniqueness.Published.fourierReconstruction_local_band_sq line 263
  21. theorem OAI.BoltzmannNonuniqueness.Published.fourierReconstruction_local_band_tendsto line 277
  22. theorem OAI.BoltzmannNonuniqueness.Published.complexL2Cutoff_inner line 306
  23. theorem OAI.BoltzmannNonuniqueness.Published.complexL2Cutoff_weak_tendsto line 315
  24. theorem OAI.BoltzmannNonuniqueness.Published.complexL2Cutoff_limit_bound line 324
  25. theorem OAI.BoltzmannNonuniqueness.Published.complexL2Cutoff_compl line 332
  26. theorem OAI.BoltzmannNonuniqueness.Published.inverseFourier_local_strong_of_weak_and_tails line 356
  27. theorem OAI.BoltzmannNonuniqueness.Published.fourier_velocity_integral line 421
  28. theorem OAI.BoltzmannNonuniqueness.Published.fourier_velocityLineAverage line 445
  29. theorem OAI.BoltzmannNonuniqueness.Published.fourierSource_uniformIntegrable line 470
  30. theorem OAI.BoltzmannNonuniqueness.Published.fourierSource_congr_ae line 485