OAI/Combinatorics/Progressions/Lattices/JointAffineBooleanSource.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.jointAffineBooleanGoodWeight line 23
  2. def OAI.Erdos3.jointAffineBooleanCutoff line 27
  3. theorem OAI.Erdos3.jointAffineBooleanCutoff_contDiff line 31
  4. theorem OAI.Erdos3.jointAffineBooleanCutoff_range line 38
  5. theorem OAI.Erdos3.jointAffineBooleanGoodWeight_spec line 44
  6. theorem OAI.Erdos3.jointAffineBooleanGoodWeight_measure line 63
  7. theorem OAI.Erdos3.jointAffineBooleanGoodWeight_mass_lower line 92
  8. theorem OAI.Erdos3.exists_joint_affine_boolean_good_mass line 133
  9. theorem OAI.Erdos3.jointAffineBooleanGoodWeight_derivative_budget line 200
  10. theorem OAI.Erdos3.jointAffineBoolean_good_weight_comparison line 249
  11. def OAI.Erdos3.jointAffineBooleanTranslationBudget line 339
  12. theorem OAI.Erdos3.jointAffineBoolean_translation_bound line 346
  13. def OAI.Erdos3.canonicalAffineCubeMinorThreshold line 415
  14. theorem OAI.Erdos3.canonicalAffineCubeMinorThreshold_pos line 419
  15. def OAI.Erdos3.jointAffineBooleanInverseBudget line 428
  16. theorem OAI.Erdos3.jointAffineBooleanInverseBudget_le line 433
  17. def OAI.Erdos3.jointAffineBooleanErrorBudget line 443
  18. theorem OAI.Erdos3.exists_canonical_joint_affine_good_mass line 450
  19. theorem OAI.Erdos3.jointAffineBooleanCutoff_loss line 489
  20. theorem OAI.Erdos3.jointAffineBoolean_regularization_error line 525
  21. theorem OAI.Erdos3.affineCubeMinorThreshold_log_inv_relative line 574
  22. theorem OAI.Erdos3.canonicalAffineCubeMinorThreshold_log_inv_relative line 588
  23. theorem OAI.Erdos3.jointAffineBoolean_source_density_comparison line 612