OAI/MathematicalPhysics/Boltzmann/Collision/WeightLocalL1.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

A positive lower bound for the hot weight on bounded velocity sets

  1. def OAI.BoltzmannNonuniqueness.VelocityWeight.compactLower line 15
  2. theorem OAI.BoltzmannNonuniqueness.VelocityWeight.compactLower_pos line 18
  3. theorem OAI.BoltzmannNonuniqueness.VelocityWeight.compactLower_le_H line 21
  4. theorem OAI.BoltzmannNonuniqueness.VelocityWeight.inv_H_le_compactLower line 34
  5. theorem OAI.BoltzmannNonuniqueness.VelocityWeight.H_le_offAxis line 52
  6. theorem OAI.BoltzmannNonuniqueness.VelocityWeight.H_ratio_le_offAxis line 70
  7. theorem OAI.BoltzmannNonuniqueness.Compactness.tendsto_L1_div_H_on_velocity_ball line 95