OAI/MathematicalPhysics/Boltzmann/Compactness/WeakCapOuterBound.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Actual weak density and pair-product limits of the cap approximations

The equality of the pair limit with the product of density limits is the subsequent velocity-averaging step, not an assumption of this extraction.

  1. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.uniformIntegrable_comp line 23
  2. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.TightCapFamily.exists_weak_limits line 29
  3. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.CompactCapFamily.weak_limit_outer_bound line 75