OAI/MathematicalPhysics/Boltzmann/Branching/LinearCharacteristicBalance.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

A logarithmic gain estimate for a nonnegative characteristic path

  1. theorem OAI.BoltzmannNonuniqueness.TransportPrimitive.logarithmic_gain_bound line 14
  2. def OAI.BoltzmannNonuniqueness.TransportPrimitive.linearSolution line 81
  3. theorem OAI.BoltzmannNonuniqueness.TransportPrimitive.linearSolution_initial line 85
  4. theorem OAI.BoltzmannNonuniqueness.TransportPrimitive.linearSolution_formula line 88
  5. theorem OAI.BoltzmannNonuniqueness.TransportPrimitive.linearSolution_absolutelyContinuous line 100
  6. theorem OAI.BoltzmannNonuniqueness.TransportPrimitive.linearSolution_hasDerivAt_ae line 114
  7. theorem OAI.BoltzmannNonuniqueness.TransportPrimitive.linear_path_eq_solution line 153
  8. theorem OAI.BoltzmannNonuniqueness.TransportPrimitive.damped_path_abs_le line 171
  9. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.linearVelocityTest_integrable line 216
  10. theorem OAI.BoltzmannNonuniqueness.TransportPrimitive.linearSolution_balance line 242