OAI/MathematicalPhysics/Boltzmann/Branching/RealL1ApproximationLimit.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Completing real L1 sequences with uniformly convergent approximations

  1. theorem OAI.BoltzmannNonuniqueness.Compactness.real_sub_triangle line 14
  2. theorem OAI.BoltzmannNonuniqueness.Compactness.l1_limit_of_uniform_approximation line 20