feat: add basics of majorization

[dupuisf]

This PR defines majorization. This is needed to develop the theory of unitarily invariant norms on ℂ^n, in particular Schatten norms.

---

• depends on: feat: add lemmas about doubly stochastic matrices #33394

[github-actions]

PR summary 69fc0048aa

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
Mathlib.Analysis.Convex.Majorization.Defs (new file)	349
Mathlib.Analysis.Convex.Majorization.Basic (new file)	1988

---

Declarations diff

+ IsMajorizedBy
+ IsMajorizedBy.equiv_left
+ IsMajorizedBy.equiv_right
+ IsMajorizedBy.isSupermajorizedBy
+ IsMajorizedBy.trans
+ IsSubmajorizedBy
+ IsSubmajorizedBy.equiv_left
+ IsSubmajorizedBy.equiv_right
+ IsSubmajorizedBy.trans
+ IsSupermajorizedBy
+ IsSupermajorizedBy.equiv_left
+ IsSupermajorizedBy.equiv_right
+ IsSupermajorizedBy.forall_nonneg
+ IsSupermajorizedBy.trans
+ card_decSumSet
+ card_incSumSet
+ const_le_of_isSupermajorizedBy_const
+ decSum
+ decSumSet
+ decSum_add_incSum
+ decSum_comp_equiv
+ decSum_const
+ decSum_eq_sum_decSumSet
+ decSum_of_ge_card
+ decSum_of_le_card
+ decSum_zero
+ eq_const_of_isMajorizedBy_const
+ exists_eq_decSum
+ exists_eq_decSum_one
+ exists_eq_incSum
+ exists_eq_incSum_one
+ exists_max'_image
+ exists_min'_image
+ ge_of_mem_decSumSet
+ incSum
+ incSumSet
+ incSum_add_decSum
+ incSum_comp_equiv
+ incSum_const
+ incSum_eq_sum_incSumSet
+ incSum_of_ge_card
+ incSum_of_le_card
+ incSum_one_le
+ incSum_zero
+ isMajorizedBy_def
+ isSubmajorizedBy_def
+ isSubmajorizedBy_iff_forall_pos
+ isSubmajorizedBy_iff_isSupermajorizedBy
+ isSupermajorizedBy_def
+ le_const_of_isSubmajorizedBy_const
+ le_decSum_one
+ le_of_mem_incSumSet
+ mem_doublyStochastic_iff_forall_mulVec_isMajorizedBy
+ mem_doublyStochastic_of_forall_mulVec_isMajorizedBy
+ mulVec_isMajorizedBy_of_mem_doublyStochastic
+ mulVec_isSubmajorizedBy_of_mem_doublyStochastic
+ reindex_mem_doublyStochastic
+ reindex_mem_doublyStochastic_iff
+ sum_decSumSet_le
+ sum_incSumSet_le
+ sum_mulVec_of_mem_doublyStochastic
+ transIsMajorizedByIsMajorizedBy
+ transIsSubmajorizedByIsSubmajorizedBy
+ transIsSupermajorizedByIsSupermajorizedBy
+ transpose_mem_doublyStochastic
+ transpose_mem_doublyStochastic_iff

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

---

No changes to technical debt.

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[mathlib4-dependent-issues-bot]

This PR/issue depends on:

• feat: add lemmas about doubly stochastic matrices #33394
  By Dependent Issues (🤖). Happy coding!