IntermediateDimension.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

def OAI.Problem335.positiveBidegreeSet line 12
Source documentation
Factors applied first in the intermediate-space argument.
```
def positiveBidegreeSet {ι : Type*} (s : Finset ι) (e i : ι → ℕ) (lam : ℝ) : Finset ι := by
…
```
def OAI.Problem335.positiveBidegreeV line 17
Source documentation
Total differentiation degree of the first group of factors.
```
def positiveBidegreeV {ι : Type*} (s : Finset ι) (e i : ι → ℕ) (lam : ℝ) : ℕ :=
…
```
def OAI.Problem335.positiveBidegreeU line 21
Source documentation
Total multiplication degree of the first group of factors.
```
def positiveBidegreeU {ι : Type*} (s : Finset ι) (e i : ι → ℕ) (lam : ℝ) : ℕ :=
…
```
theorem OAI.Problem335.positiveBidegreeV_le line 24
theorem OAI.Problem335.positiveBidegreeU_le line 30

theorem OAI.Problem335.positiveBidegree_rpow line 41

Source documentation

Natural bidegree assignments give exactly the discrepancy-weight product.

theorem positiveBidegree_rpow {ι : Type*} (s : Finset ι) (e i : ι → ℕ)
    (ρ lam α : ℝ) (hα : 0 < α) (hie : ∀ j ∈ s, i j ≤ e j)
    (hlam : (1 + ρ) * lam = ρ)
    (hbalance : lam * (∑ j ∈ s, e j : ℕ) = (∑ j ∈ s, i j : ℕ)) :
    α ^ ((positiveBidegreeV s e i lam : ℝ) - ρ * positiveBidegreeU s e i lam) =
      ∏ j ∈ s, (α ^ ((1 + ρ) / 2)) ^ |(i j : ℝ) - lam * e j| := by
…

Mentions: OAI.Problem335.positiveBidegreeV, OAI.Problem335.positiveBidegreeU

theorem OAI.Problem335.intermediate_dimension_le_weight_product line 66

Source documentation

The intermediate space associated to an admissible natural bidegree assignment is bounded by its product of discrepancy weights.

theorem intermediate_dimension_le_weight_product {ι : Type*} (s : Finset ι)
    (e i : ι → ℕ) (k n v u a b : ℕ) (ρ lam : ℝ)
    (hie : ∀ j ∈ s, i j ≤ e j)
    (he : ∑ j ∈ s, e j = n) (hi : ∑ j ∈ s, i j = k)
    (hproportion : lam * n = k) (hlam : (1 + ρ) * lam = ρ)
    (hv : 1 ≤ v) (hu : 1 ≤ u) (ha : 0 < a) (hb : 0 < b)
    (hka : k ≤ a) (hbudget : 2 * k ≤ a + v)
    (hbalance : ((a : ℝ) / ((a : ℝ) + v)) ^ ρ ≤
      (b : ℝ) / ((b : ℝ) + u)) :
    (homogeneousDim v (a - positiveBidegreeV s e i lam) : ℝ) *
        homogeneousDim u (b + positiveBidegreeU s e i lam) ≤
      2 * ((homogeneousDim v a : ℝ) * homogeneousDim u b) *
…

Mentions: OAI.Problem335.homogeneousDim, OAI.Problem335.positiveBidegreeV, OAI.Problem335.positiveBidegreeU

theorem OAI.Problem335.sum_intermediate_dimensions_le_weight_product line 96

Source documentation

Summing intermediate dimensions over the admissible bidegrees gives the numerical product bound used after rank subadditivity.

theorem sum_intermediate_dimensions_le_weight_product {ι : Type*}
    [Fintype ι] [DecidableEq ι] (e : ι → ℕ) (k n v u a b : ℕ) (ρ lam : ℝ)
    (he : ∑ j, e j = n) (hproportion : lam * n = k)
    (hlam : (1 + ρ) * lam = ρ)
    (hv : 1 ≤ v) (hu : 1 ≤ u) (ha : 0 < a) (hb : 0 < b)
    (hka : k ≤ a) (hbudget : 2 * k ≤ a + v)
    (hbalance : ((a : ℝ) / ((a : ℝ) + v)) ^ ρ ≤
      (b : ℝ) / ((b : ℝ) + u)) :
    (∑ i ∈ (Fintype.piFinset (fun j => Finset.range (e j + 1))).filter
        (fun i => ∑ j, i j = k),
      (homogeneousDim v (a - positiveBidegreeV Finset.univ e i lam) : ℝ) *
        homogeneousDim u (b + positiveBidegreeU Finset.univ e i lam)) ≤
…

Mentions: OAI.Problem335.homogeneousDim, OAI.Problem335.positiveBidegreeV, OAI.Problem335.positiveBidegreeU