OAI/MeasureTheory/Falconer/Estimates/PolicyFarCoefficients.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Exact collision coefficients and their branch payments

  1. def OAI.Falconer.PolicyJetData.farWeight line 14
  2. def OAI.Falconer.PolicyJetData.collisionCoefficient line 19
  3. theorem OAI.Falconer.PolicyJetData.collisionTerm_eq line 25
  4. theorem OAI.Falconer.eventual_policy_far_coefficient line 40
  5. theorem OAI.Falconer.eventual_policy_collisionTerm_payment line 73