OAI/MathematicalPhysics/Boltzmann/Branching/RegularChart.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Regular chart volume and transverse inverse-distance averaging

  1. def OAI.BoltzmannNonuniqueness.RegularChart.ballMass line 20
  2. theorem OAI.BoltzmannNonuniqueness.RegularChart.ballMass_le line 23
  3. theorem OAI.BoltzmannNonuniqueness.RegularChart.inverse_norm_le_extendedKernel line 65
  4. theorem OAI.BoltzmannNonuniqueness.RegularChart.transverseLaw_inverse_norm_bound line 80
  5. theorem OAI.BoltzmannNonuniqueness.RegularChart.sheet_inverse_norm_bound line 90
  6. theorem OAI.BoltzmannNonuniqueness.RegularChart.one_ball_sheet_bound line 104