OAI/Combinatorics/Progressions/Estimates/BooleanAxisLogEnvelope.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.booleanAxisWeightCost line 12
  2. theorem OAI.Erdos3.booleanAxisWeightLog_nonneg line 21
  3. theorem OAI.Erdos3.booleanAxisWeightCost_le_exp line 28
  4. theorem OAI.Erdos3.jointBooleanWeightLog_nonneg line 80
  5. theorem OAI.Erdos3.jointBooleanWeightBudget_canonical_le_exp line 86
  6. def OAI.Erdos3.booleanMinorLogEnvelope line 116
  7. def OAI.Erdos3.booleanInverseLogEnvelope line 120
  8. def OAI.Erdos3.booleanDerivativeLogEnvelope line 123
  9. def OAI.Erdos3.booleanWeightLogEnvelope line 126
  10. theorem OAI.Erdos3.booleanAxisLogEnvelopes_nonneg line 132
  11. theorem OAI.Erdos3.canonicalBooleanMinorLog_le_envelope line 139
  12. theorem OAI.Erdos3.booleanAxisLogs_le_envelopes line 154