OAI/MathematicalPhysics/Boltzmann/Branching/HotPhysicalSource.lean

GitHub source file

38 declarations, 0 contain sorry, 0 declared as axioms

A fixed negligible velocity set for the weighted local construction

The exceptional set depends only on H and its proved quadratic gain bound, not on a solution or an iterate. Setting the gain to zero there preserves its almost-everywhere collision meaning and gives pointwise bounded sources.

  1. def OAI.BoltzmannNonuniqueness.HotRepresentative.good line 29
  2. theorem OAI.BoltzmannNonuniqueness.HotRepresentative.measurable_nonnegativeGain line 33
  3. theorem OAI.BoltzmannNonuniqueness.HotRepresentative.measurableSet_good line 51
  4. theorem OAI.BoltzmannNonuniqueness.HotRepresentative.ae_good line 56
  5. theorem OAI.BoltzmannNonuniqueness.HotRepresentative.integrable_H_gain line 60
  6. theorem OAI.BoltzmannNonuniqueness.HotRepresentative.H_gain_bound line 64
  7. def OAI.BoltzmannNonuniqueness.HotRepresentative.density line 71
  8. def OAI.BoltzmannNonuniqueness.HotRepresentative.gain line 73
  9. def OAI.BoltzmannNonuniqueness.HotRepresentative.frequency line 77
  10. theorem OAI.BoltzmannNonuniqueness.HotRepresentative.measurable_density line 80
  11. theorem OAI.BoltzmannNonuniqueness.HotRepresentative.measurable_gain line 83
  12. theorem OAI.BoltzmannNonuniqueness.HotRepresentative.measurable_frequency line 89
  13. theorem OAI.BoltzmannNonuniqueness.HotRepresentative.actual_gain_bound line 110
  14. theorem OAI.BoltzmannNonuniqueness.HotRepresentative.actual_gain_upper_difference line 126
  15. theorem OAI.BoltzmannNonuniqueness.HotRepresentative.actual_gain_difference line 151
  16. theorem OAI.BoltzmannNonuniqueness.HotRepresentative.gain_nonneg line 169
  17. theorem OAI.BoltzmannNonuniqueness.HotRepresentative.gain_bound line 180
  18. theorem OAI.BoltzmannNonuniqueness.HotRepresentative.gain_difference line 193
  19. theorem OAI.BoltzmannNonuniqueness.HotRepresentative.density_bounds line 236
  20. theorem OAI.BoltzmannNonuniqueness.HotRepresentative.density_difference line 243
  21. theorem OAI.BoltzmannNonuniqueness.HotRepresentative.frequency_nonneg line 251
  22. theorem OAI.BoltzmannNonuniqueness.HotRepresentative.frequency_bound line 255
  23. theorem OAI.BoltzmannNonuniqueness.HotRepresentative.frequency_difference line 262
  24. theorem OAI.BoltzmannNonuniqueness.HotRepresentative.physical_gain_eq line 275
  25. theorem OAI.BoltzmannNonuniqueness.HotRepresentative.ae_physical_gain line 282
  26. def OAI.BoltzmannNonuniqueness.HotRepresentative.source line 307
  27. theorem OAI.BoltzmannNonuniqueness.HotRepresentative.measurable_source line 310
  28. theorem OAI.BoltzmannNonuniqueness.HotRepresentative.source_bounds line 314
  29. theorem OAI.BoltzmannNonuniqueness.HotRepresentative.source_difference line 332
  30. def OAI.BoltzmannNonuniqueness.GaussianLocal.hotRemainder line 393
  31. def OAI.BoltzmannNonuniqueness.GaussianLocal.hotForcing line 397
  32. theorem OAI.BoltzmannNonuniqueness.GaussianLocal.value_sub line 401
  33. theorem OAI.BoltzmannNonuniqueness.GaussianLocal.hotRemainder_solution line 422
  34. theorem OAI.BoltzmannNonuniqueness.PhaseEssSup.continuousOn_size_of_mildAE line 500
  35. theorem OAI.BoltzmannNonuniqueness.PhaseEssSup.zero_seed_bound_ae line 515
  36. theorem OAI.BoltzmannNonuniqueness.HotGainRemainder.gain_difference_le line 575

    Source documentation

    The loss-free gain of the remainder uses the mixed cold estimate, rather than the much larger pointwise norm of the cold color.

    theorem gain_difference_le {q R D M : ℝ} {v : Velocity}
    (hv : v ∈ HotRepresentative.good q) (hD : 0 ≤ D)
    {f c : Velocity → ℝ} (hfm : Measurable f) (hcm : Measurable c)
    (hc : ∀ w, 0 ≤ c w) (hcf : ∀ w, c w ≤ f w)
    (hf : ∀ w, f w ≤ R * H q w) (hrem : ∀ w, f w - c w ≤ D * H q w)
    (hci : Integrable (MixedRealGain.integrand c (H q) v) gainPairMeasure)
    (hcM : MixedRealGain.gain c (H q) v ≤ M * H q v) (b : ℝ) :
    CollisionCutoff.gain b f v - CollisionCutoff.gain b c v ≤
      (2 * D * M + D^2 * HotApplication.realBound q) * H q v := by
…

    Mentions: OAI.BoltzmannNonuniqueness.Velocity, OAI.BoltzmannNonuniqueness.HotRepresentative.good, OAI.BoltzmannNonuniqueness.MixedRealGain.integrand, OAI.BoltzmannNonuniqueness.gainPairMeasure, OAI.BoltzmannNonuniqueness.MixedRealGain.gain, OAI.BoltzmannNonuniqueness.CollisionCutoff.gain, OAI.BoltzmannNonuniqueness.HotApplication.realBound

  37. theorem OAI.BoltzmannNonuniqueness.HotRepresentative.physical_source_eq line 647
  38. theorem OAI.BoltzmannNonuniqueness.HotRepresentative.ae_physical_source line 658