OAI/MathematicalPhysics/Boltzmann/Approximation/CapMixedPositiveBound.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

The actual cold density in the Euclidean dilation coordinates

  1. def OAI.BoltzmannNonuniqueness.JetCopyDatum.CapApproximation.dilatedCold line 25
  2. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.CapApproximation.dilatedCold_measurable line 29
  3. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.CapApproximation.dilatedCold_nonneg line 42
  4. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.HotLimitExtraction.damped_gain_hot_integral line 70
  5. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.euclidean_hot_collision line 109
  6. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.euclideanHotSource_le_gains line 163
  7. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.normalizedHotSource_le_gains line 178
  8. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.CapApproximation.mixed_gain_le_selected_action line 209
  9. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.CapApproximation.normalized_mixed_gain_le_positive line 254
  10. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.cold_gain_error_tendsto_zero line 282