OAI/MathematicalPhysics/Boltzmann/Compactness/SelectedTwoGainLimit.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Removing the large-scale remainder from the selected pair integral

  1. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.selected_pair_le_retained line 21
  2. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.selected_pair_axial_tendsto line 74
  3. def OAI.BoltzmannNonuniqueness.JetCopyDatum.selectedPairMass line 141
  4. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.selected_pair_uniform line 153
  5. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.retained_zero_of_transverse_far line 226
  6. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.selected_transverse_escape_small line 237
  7. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.selected_two_gain_axial_tendsto line 310