ConfiguredRankData.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

Common, concrete data for the two sides of the IMM rank comparison.

def OAI.Problem335.LowerParameters.rankDimension line 15
Source documentation
The source dimension for the configured bidegree rank measure.
```
def rankDimension (n : ℕ) : ℝ :=
…
```
def OAI.Problem335.LowerParameters.rankMomentScale line 19
Source documentation
The common path-count and occupation-mean factor in the two trace moments.
```
def rankMomentScale (n : ℕ) : ℝ :=
…
```
def OAI.Problem335.LowerParameters.rankData line 25
Source documentation
The actual rank measure, extended by zero outside the range where the balanced schedule is used. The small values do not enter the eventual bounds.
```
def rankData (n : ℕ) (p : MvPolynomial (Fin n × Fin n × Fin n) ℂ) : ℝ :=
…
```
theorem OAI.Problem335.LowerParameters.rankData_eq line 31
theorem OAI.Problem335.LowerParameters.rankData_nonneg line 38
theorem OAI.Problem335.LowerParameters.rankDimension_nonneg line 43
theorem OAI.Problem335.LowerParameters.rankDimension_pos line 47
theorem OAI.Problem335.LowerParameters.rankMomentScale_pos line 55