OAI/MathematicalPhysics/Boltzmann/Branching/BackgroundCappedLoss.lean

GitHub source file

36 declarations, 0 contain sorry, 0 declared as axioms

Uniform polynomial velocity moments of the limiting background

  1. theorem OAI.BoltzmannNonuniqueness.AxialBackground.axial_velocity_norm_le line 21
  2. theorem OAI.BoltzmannNonuniqueness.AxialBackground.integral_cell_abs_le line 33
  3. theorem OAI.BoltzmannNonuniqueness.AxialBackground.moment_cell_bound line 53
  4. theorem OAI.BoltzmannNonuniqueness.GeometricBackground.moment_bound line 68
  5. theorem OAI.BoltzmannNonuniqueness.AxialBackground.clamped_weight_measurable line 103
  6. theorem OAI.BoltzmannNonuniqueness.AxialBackground.clamped_atom_test_measurable line 112
  7. theorem OAI.BoltzmannNonuniqueness.AxialBackground.clamped_cell_test_measurable line 128
  8. theorem OAI.BoltzmannNonuniqueness.GeometricBackground.clamped_background_test_measurable line 146
  9. def OAI.BoltzmannNonuniqueness.GeometricBackground.frequency line 187
  10. theorem OAI.BoltzmannNonuniqueness.GeometricBackground.frequency_nonneg line 190
  11. theorem OAI.BoltzmannNonuniqueness.GeometricBackground.integrable_test line 194
  12. theorem OAI.BoltzmannNonuniqueness.GeometricBackground.frequency_bound line 203
  13. theorem OAI.BoltzmannNonuniqueness.GeometricBackground.cell_distance_measurable line 234
  14. theorem OAI.BoltzmannNonuniqueness.GeometricBackground.clamped_frequency_measurable line 260
  15. theorem OAI.BoltzmannNonuniqueness.AxialBackground.compressed_scalar_error line 308
  16. def OAI.BoltzmannNonuniqueness.AxialBackground.relativeWeight line 329
  17. theorem OAI.BoltzmannNonuniqueness.AxialBackground.weight_eq_relative line 333
  18. theorem OAI.BoltzmannNonuniqueness.AxialBackground.relativeWeight_error line 343
  19. theorem OAI.BoltzmannNonuniqueness.AxialBackground.foot_abs_bound line 350
  20. theorem OAI.BoltzmannNonuniqueness.GeometricBackground.background_finite line 380
  21. theorem OAI.BoltzmannNonuniqueness.GeometricBackground.clamped_background_measurable line 385
  22. def OAI.BoltzmannNonuniqueness.GeometricBackground.slabKernel line 400
  23. theorem OAI.BoltzmannNonuniqueness.GeometricBackground.slabKernel_finite line 413
  24. def OAI.BoltzmannNonuniqueness.GeometricBackground.gainCoefficient line 450
  25. theorem OAI.BoltzmannNonuniqueness.GeometricBackground.gainCoefficient_lt_top line 454
  26. theorem OAI.BoltzmannNonuniqueness.GeometricBackground.capped_chartGain_bound line 458
  27. theorem OAI.BoltzmannNonuniqueness.GeometricBackground.capped_chartGain_ae_bound line 494
  28. theorem OAI.BoltzmannNonuniqueness.GeometricBackground.gaussian_moment_bound line 522
  29. theorem OAI.BoltzmannNonuniqueness.AxialBackground.S_lower_of_abs_le line 569
  30. def OAI.BoltzmannNonuniqueness.AxialBackground.compactWeightLower line 577
  31. theorem OAI.BoltzmannNonuniqueness.AxialBackground.compactWeightLower_pos line 580
  32. theorem OAI.BoltzmannNonuniqueness.AxialBackground.compactWeightLower_le line 587
  33. def OAI.BoltzmannNonuniqueness.GeometricBackground.lossCoefficient line 633
  34. theorem OAI.BoltzmannNonuniqueness.GeometricBackground.lossCoefficient_nonneg line 636
  35. theorem OAI.BoltzmannNonuniqueness.GeometricBackground.capped_loss_bound line 641
  36. theorem OAI.BoltzmannNonuniqueness.GeometricBackground.frequency_slab_bound line 657