OAI/MathematicalPhysics/Boltzmann/Branching/MismatchSlices.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Slice bounds with a nonzero axial mismatch

  1. theorem OAI.BoltzmannNonuniqueness.MismatchSlices.lintegral_extendedPower_slope line 17
  2. theorem OAI.BoltzmannNonuniqueness.MismatchSlices.rectangleLineMass_slope_bound line 32
  3. theorem OAI.BoltzmannNonuniqueness.MismatchSlices.inverse_power_le line 59
  4. theorem OAI.BoltzmannNonuniqueness.MismatchSlices.inverse_slope_bound line 73
  5. def OAI.BoltzmannNonuniqueness.MismatchSlices.slopeCoefficient line 89
  6. def OAI.BoltzmannNonuniqueness.MismatchSlices.mismatchCoefficient line 92
  7. theorem OAI.BoltzmannNonuniqueness.MismatchSlices.slopeCoefficient_nonneg line 95
  8. theorem OAI.BoltzmannNonuniqueness.MismatchSlices.mismatchCoefficient_nonneg line 101
  9. theorem OAI.BoltzmannNonuniqueness.MismatchSlices.normalizedBallSlice_mismatch line 108