OAI/MathematicalPhysics/Boltzmann/Approximation/CapHotSourceIntegrability.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

Lower source and loss bounds for the actual finite cap solutions

  1. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.CapApproximation.hot_net_lower line 24
  2. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.CapApproximation.loss_bound line 56
  3. def OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.lossEnvelope line 121
  4. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.eventually_rescaledHotSource_lower line 125
  5. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.lossEnvelope_nonneg line 194
  6. def OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.sourceEnvelope line 206
  7. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.eventually_rescaledHotSource_abs line 210
  8. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.CapApproximation.loss_scale_bound line 263
  9. theorem OAI.BoltzmannNonuniqueness.Compactness.uniformIntegrable_of_abs_le line 326
  10. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.sourceEnvelope_integrable line 344
  11. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.sourceEnvelope_window_integrable line 360
  12. def OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.hotSourceDensity line 389
  13. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.hotSourceDensity_measurable line 394
  14. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.eventually_hotSourceDensity_bound line 403
  15. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.hotSourceDensity_uniformIntegrable_tail line 440