OAI/MathematicalPhysics/Boltzmann/Branching/CompactCapFamily.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Strong local product convergence from pair uniform integrability

  1. theorem OAI.BoltzmannNonuniqueness.Compactness.uniformIntegrable_compact_average_product line 23
  2. theorem OAI.BoltzmannNonuniqueness.Compactness.local_average_product_convergence line 53
  3. structure OAI.BoltzmannNonuniqueness.JetCopyDatum.CompactCapFamily line 100
  4. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.CompactCapFamily.source_ui line 120
  5. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.exists_compact_cap_family line 130