OAI/MathematicalPhysics/Boltzmann/Branching/L2PairingBound.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Squared integral pairings for the velocity multiplier estimate

  1. theorem OAI.BoltzmannNonuniqueness.Published.L2_norm_sq_integral line 14
  2. theorem OAI.BoltzmannNonuniqueness.Published.L2_pairing_sq_le line 22