OAI/MathematicalPhysics/Boltzmann/Branching/WeightedNormalizedGainTranslation.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Bounded incoming weights preserve the actual normalized-gain translation estimate

  1. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.DoubleGain.weighted_normalizedGain_translation line 14