OAI/MathematicalPhysics/Boltzmann/Branching/BoundedAverageCompactness.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Uniform L2 Fourier tails on each bounded-source class

  1. theorem OAI.BoltzmannNonuniqueness.Published.bounded_average_uniform_tails line 17
  2. def OAI.BoltzmannNonuniqueness.Published.boundedAverageL2 line 71
  3. theorem OAI.BoltzmannNonuniqueness.Published.bounded_average_compactness line 76