OAI/MathematicalPhysics/Boltzmann/Approximation/ColoredDifferenceAlgebra.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

The symmetric gain and colored collision algebra

The symmetric bilinear gain is defined from the paper's exact angular kernel. Integral additivity carries integrability hypotheses. The resulting algebra combines the cold and hot collision equations.

  1. def OAI.BoltzmannNonuniqueness.gainPairMeasure line 22
  2. def OAI.BoltzmannNonuniqueness.gainPairIntegrand line 25
  3. def OAI.BoltzmannNonuniqueness.symmetricGain line 32

    Source documentation

    The associated symmetric bilinear gain.

    def symmetricGain (f g : Density) (x : Position) (v : Velocity) : ℝ :=
…

    Mentions: OAI.BoltzmannNonuniqueness.Density, OAI.BoltzmannNonuniqueness.Position, OAI.BoltzmannNonuniqueness.Velocity

  4. theorem OAI.BoltzmannNonuniqueness.gainPairIntegrand_symm line 35
  5. theorem OAI.BoltzmannNonuniqueness.gainPairIntegrand_fun_symm line 41
  6. theorem OAI.BoltzmannNonuniqueness.symmetricGain_symm line 45
  7. theorem OAI.BoltzmannNonuniqueness.symmetricGain_self line 51
  8. theorem OAI.BoltzmannNonuniqueness.gainPairIntegrand_add_left line 58
  9. theorem OAI.BoltzmannNonuniqueness.gainPairIntegrand_fun_add_left line 65
  10. theorem OAI.BoltzmannNonuniqueness.symmetricGain_add_left line 70
  11. theorem OAI.BoltzmannNonuniqueness.symmetricGain_add_right line 78
  12. theorem OAI.BoltzmannNonuniqueness.cold_hot_gain_expansion line 90

    Source documentation

    Expansion into cold-cold, cold-hot, and hot-hot gains, before refining cold labels.

    theorem cold_hot_gain_expansion (c h : Density) (x : Position) (v : Velocity)
    (hcc : Integrable (gainPairIntegrand c c x v) gainPairMeasure)
    (hch : Integrable (gainPairIntegrand c h x v) gainPairMeasure)
    (hhh : Integrable (gainPairIntegrand h h x v) gainPairMeasure) :
    gain (c + h) x v = gain c x v + 2 * symmetricGain c h x v + gain h x v := by
…

    Mentions: OAI.BoltzmannNonuniqueness.Density, OAI.BoltzmannNonuniqueness.Position, OAI.BoltzmannNonuniqueness.Velocity, OAI.BoltzmannNonuniqueness.gainPairIntegrand, OAI.BoltzmannNonuniqueness.gainPairMeasure, OAI.BoltzmannNonuniqueness.gain, OAI.BoltzmannNonuniqueness.symmetricGain

  13. theorem OAI.BoltzmannNonuniqueness.ColoredAlgebra.sum_abs_product_difference_le line 125