OAI/MathematicalPhysics/Boltzmann/Approximation/SubcapColdControl.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

Positive approximations below the cap

The cap upper bound suffices for compactness, without requiring the cap to be attained. Zero-hot approximations therefore satisfy the same bounds.

  1. structure OAI.BoltzmannNonuniqueness.JetCopyDatum.BelowCap.Approximation line 20
  2. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.BelowCap.cap_family_pairs_uniformIntegrable line 32
  3. def OAI.BoltzmannNonuniqueness.JetCopyDatum.BelowCap.Approximation.cold line 77
  4. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.BelowCap.Approximation.cold_properties line 83
  5. def OAI.BoltzmannNonuniqueness.JetCopyDatum.BelowCap.Approximation.coldTotal line 112
  6. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.BelowCap.Approximation.coldTotal_properties line 116
  7. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.BelowCap.Approximation.cold_envelope line 130
  8. def OAI.BoltzmannNonuniqueness.JetCopyDatum.BelowCap.Approximation.escapedTotal line 155
  9. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.BelowCap.Approximation.escapedTotal_measurable line 160
  10. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.BelowCap.Approximation.escapedTotal_nonneg line 189
  11. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.BelowCap.Approximation.escapedTotal_bound line 202
  12. def OAI.BoltzmannNonuniqueness.JetCopyDatum.BelowCap.Approximation.centralTotal line 233
  13. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.BelowCap.Approximation.centralTotal_measurable line 239
  14. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.BelowCap.Approximation.coldTotal_eq_central_add_escaped line 261
  15. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.BelowCap.Approximation.centralTotal_single line 302
  16. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.BelowCap.Approximation.cold_free_majorant_at_main line 321
  17. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.BelowCap.Approximation.coldTotal_eq_escaped_of_no_main line 344
  18. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.BelowCap.Approximation.escapedTotal_bound_global line 359