OAI/MathematicalPhysics/Boltzmann/Collision/MityaginDischarge.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Twenty-dimensional analytic zero-set nullity

One-dimensional isolated zeros, Fubini along lines through a nonzero point, and the analytic identity principle give the required specialization of Mityagin's Proposition 0.

  1. def OAI.BoltzmannNonuniqueness.Published.fiveGainParameterEquiv line 17
  2. theorem OAI.BoltzmannNonuniqueness.Published.mityagin2020FiveGainParameters line 22