OAI/MathematicalPhysics/Boltzmann/Branching/LinearHotLocalization.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Localized GLPS resolvents for a bounded weighted linear mild equation

  1. def OAI.BoltzmannNonuniqueness.EuclideanFlight.linearSource line 16
  2. theorem OAI.BoltzmannNonuniqueness.EuclideanFlight.linearSource_along line 20
  3. theorem OAI.BoltzmannNonuniqueness.EuclideanFlight.smooth_linear_localized line 28
  4. theorem OAI.BoltzmannNonuniqueness.EuclideanFlight.linear_resolvent line 70