OAI/MathematicalPhysics/Boltzmann/Jets/JetFiniteCap.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

The escaped-barrier estimate is uniform over all periodic cells

  1. theorem OAI.BoltzmannNonuniqueness.JetEscapedTotal.shifted_cell line 23
  2. theorem OAI.BoltzmannNonuniqueness.JetEscapedTotal.annulus_cell line 31
  3. theorem OAI.BoltzmannNonuniqueness.JetEscapedTotal.total_cell line 47
  4. theorem OAI.BoltzmannNonuniqueness.JetEscapedTotal.arbitrary_power_global line 54
  5. theorem OAI.BoltzmannNonuniqueness.JetEscapedEnvelope.arbitrary_power_global line 84
  6. theorem OAI.BoltzmannNonuniqueness.JetEscapedEnvelope.real_power_global line 115
  7. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.exists_uniform_cap_solution line 152