OAI/Combinatorics/Progressions/Lattices/PartitionedAffineLogEnvelope.lean

GitHub source file

57 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.canonicalAffineMinorLog line 11
  2. theorem OAI.Erdos3.canonicalAffineMinorLog_nonneg line 17
  3. theorem OAI.Erdos3.canonicalAffineCubeMinorThreshold_inverse_le_exp line 22
  4. def OAI.Erdos3.jointAffineInverseLog line 51
  5. theorem OAI.Erdos3.jointAffineInverseLog_nonneg line 56
  6. theorem OAI.Erdos3.jointAffineBooleanInverseBudget_le_exp line 67
  7. def OAI.Erdos3.affineBooleanAxisWeightLog line 108
  8. def OAI.Erdos3.jointAffineBooleanWeightLog line 115
  9. def OAI.Erdos3.affineBooleanAxisWeightCost line 120
  10. theorem OAI.Erdos3.affineBooleanAxisWeightLog_nonneg line 129
  11. theorem OAI.Erdos3.affineBooleanAxisWeightCost_le_exp line 136
  12. theorem OAI.Erdos3.jointAffineBooleanWeightLog_nonneg line 188
  13. theorem OAI.Erdos3.jointAffineBooleanWeightBudget_canonical_le_exp line 194
  14. def OAI.Erdos3.affineMinorVariableEnvelope line 226
  15. def OAI.Erdos3.affineMinorDegreeEnvelope line 227
  16. def OAI.Erdos3.affineMinorConstantEnvelope line 228
  17. def OAI.Erdos3.affineMinorLogEnvelope line 232
  18. theorem OAI.Erdos3.affineMinorVariableEnvelope_nonneg line 239
  19. theorem OAI.Erdos3.affineMinorDegreeEnvelope_nonneg line 241
  20. theorem OAI.Erdos3.affineMinorConstantEnvelope_nonneg line 243
  21. theorem OAI.Erdos3.affineMinorLogEnvelope_nonneg line 249
  22. theorem OAI.Erdos3.cubeMinor_counts_le_envelope line 258
  23. theorem OAI.Erdos3.canonicalAffineMinorLog_le_envelope line 273
  24. def OAI.Erdos3.jointAffineTranslationLog line 306
  25. def OAI.Erdos3.jointAffinePerturbationLog line 312
  26. theorem OAI.Erdos3.jointAffineDivergence_le_exp line 318
  27. def OAI.Erdos3.affineInverseAxisEnvelope line 365
  28. def OAI.Erdos3.affineDerivativeAxisEnvelope line 368
  29. def OAI.Erdos3.affineWeightAxisEnvelope line 371
  30. theorem OAI.Erdos3.affineInverseAxisEnvelope_nonneg line 378
  31. theorem OAI.Erdos3.affineDerivativeAxisEnvelope_nonneg line 384
  32. theorem OAI.Erdos3.affineWeightAxisEnvelope_nonneg line 389
  33. theorem OAI.Erdos3.affineBlockParameter_card_le line 397
  34. theorem OAI.Erdos3.affineInverseAxisLog_le_envelope line 405
  35. theorem OAI.Erdos3.affineDerivativeAxisLog_le_envelope line 415
  36. theorem OAI.Erdos3.affineWeightAxisLog_le_envelope line 425
  37. def OAI.Erdos3.jointAffineSourceInputLog line 452
  38. theorem OAI.Erdos3.jointAffineSourceScales_log_bounds line 457
  39. theorem OAI.Erdos3.jointAffineSourceTolerance_pos line 547
  40. theorem OAI.Erdos3.jointAffineCoefficientTolerance_log_bound line 565
  41. def OAI.Erdos3.jointAffineInverseEnvelope line 604
  42. def OAI.Erdos3.jointAffineDerivativeEnvelope line 605
  43. def OAI.Erdos3.jointAffineWeightEnvelope line 606
  44. def OAI.Erdos3.jointAffineSourceEnvelope line 607
  45. theorem OAI.Erdos3.affineLog_sum_le line 617
  46. theorem OAI.Erdos3.jointAffineSourceInputLog_le_envelope line 628
  47. theorem OAI.Erdos3.jointAffineSourceEnvelope_nonneg line 657
  48. theorem OAI.Erdos3.jointAffineSourceEnvelope_mono line 667
  49. def OAI.Erdos3.partitionedAffineSourceRadius line 688
  50. def OAI.Erdos3.partitionedAffineSourceTolerance line 693
  51. theorem OAI.Erdos3.affineDividedAccuracy_bounds line 708
  52. theorem OAI.Erdos3.partitionedAffineSource_scales_log_bounds line 737
  53. def OAI.Erdos3.affineProfileCoefficientEnvelope line 783
  54. def OAI.Erdos3.affineProfileInputEnvelope line 784
  55. def OAI.Erdos3.affineProfileToleranceEnvelope line 787
  56. theorem OAI.Erdos3.partitionedAffineInputLog_le_envelope line 797
  57. theorem OAI.Erdos3.partitionedAffineToleranceLog_le_envelope line 820