OAI/MathematicalPhysics/Boltzmann/Branching/InverseFourierL2.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The inverse Fourier integral agrees with the inverse L2 transform

  1. theorem OAI.BoltzmannNonuniqueness.Published.inverseFourier_L2_pairing line 11
  2. theorem OAI.BoltzmannNonuniqueness.Published.inverseFourier_integral_pairing line 18
  3. theorem OAI.BoltzmannNonuniqueness.Published.inverseFourier_L2_ae_eq_integral line 37