OAI/Combinatorics/Progressions/Dynamics/JetOutputRadiusLogBudget.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.polynomialBoxLip_le_exp line 11
  2. theorem OAI.Erdos3.normalizedJetMass_le_exp line 17
  3. theorem OAI.Erdos3.normalizedJetColumnLip_le_exp line 33
  4. def OAI.Erdos3.jetOutputRadiusLog line 53
  5. theorem OAI.Erdos3.jetOutputRadiusLog_nonneg line 55
  6. theorem OAI.Erdos3.normalizedJetOutputRadius_le_exp line 58