OAI/MathematicalPhysics/Boltzmann/Compactness/SelectedNonaxialLimit.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

The Gaussian remainder selected by the actual main-core regions

  1. def OAI.BoltzmannNonuniqueness.JetCopyDatum.copyRemainderDensity line 22
  2. def OAI.BoltzmannNonuniqueness.JetCopyDatum.selectedRemainderDensity line 28
  3. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.selectedCoreDensity_eq line 33
  4. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.selectedRemainderDensity_eq line 46
  5. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.selectedRemainderDensity_eq_zero line 59
  6. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.selectedRemainder_gain_bound line 84
  7. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.selected_five_nonaxial_tendsto line 149