OAI/MathematicalPhysics/Boltzmann/Jets/GeometricColdSource.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

The uniform source estimate for a dominated geometric cold family

  1. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.geometric_family_source line 19
  2. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.geometric_cold_sum_bound line 80
  3. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.geometric_hot_norm_source line 127
  4. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.geometric_hot_net_source line 222
  5. def OAI.BoltzmannNonuniqueness.JetCopyDatum.coldFamilySource line 312
  6. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.geometric_cold_source line 316