BinomialRatios.lean`

16 declarations, 0 contain sorry, 0 declared as axioms

Binomial dimension estimates for the intermediate spaces in the differentiation--multiplication rank argument.

def OAI.Problem335.homogeneousDim line 12
Source documentation
Dimension of homogeneous degree t polynomials in r variables, for a positive number of variables.
```
def homogeneousDim (r t : ℕ) : ℕ := (r + t - 1).choose t
```
theorem OAI.Problem335.homogeneousDim_pos line 14
theorem OAI.Problem335.homogeneousDim_zero line 19
theorem OAI.Problem335.homogeneousDim_succ_mul line 22
theorem OAI.Problem335.homogeneousDim_succ_cast line 29
theorem OAI.Problem335.homogeneousDim_cast_eq_succ line 35

theorem OAI.Problem335.homogeneousDim_down_step line 43

Source documentation

Moving down one degree costs at most the largest ratio on the interval.

theorem homogeneousDim_down_step {r a t : ℕ} (hr : 1 ≤ r)
    (ht : t + 1 ≤ a) :
    (homogeneousDim r t : ℝ) ≤
      (homogeneousDim r (t + 1) : ℝ) *
        ((a : ℝ) / ((a : ℝ) + r - 1)) := by
…

Mentions: OAI.Problem335.homogeneousDim

theorem OAI.Problem335.homogeneousDim_up_step line 60

Source documentation

Moving up one degree costs at most the initial coarse ratio.

theorem homogeneousDim_up_step {r b t : ℕ} (hr : 1 ≤ r)
    (hb : 0 < b) (ht : b ≤ t) :
    (homogeneousDim r (t + 1) : ℝ) ≤
      (homogeneousDim r t : ℝ) * (((b : ℝ) + r) / b) := by
…

Mentions: OAI.Problem335.homogeneousDim

theorem OAI.Problem335.homogeneousDim_down_bound line 75

Source documentation

Iterating the descending degree ratio.

theorem homogeneousDim_down_bound {r a : ℕ} (hr : 1 ≤ r) (I : ℕ) :
    I ≤ a → (homogeneousDim r (a - I) : ℝ) ≤
      (homogeneousDim r a : ℝ) * ((a : ℝ) / ((a : ℝ) + r - 1)) ^ I := by
…

Mentions: OAI.Problem335.homogeneousDim

theorem OAI.Problem335.homogeneousDim_up_bound line 103

Source documentation

Iterating the ascending degree ratio.

theorem homogeneousDim_up_bound {r b : ℕ} (hr : 1 ≤ r) (hb : 0 < b) (J : ℕ) :
    (homogeneousDim r (b + J) : ℝ) ≤
      (homogeneousDim r b : ℝ) * (((b : ℝ) + r) / b) ^ J := by
…

Mentions: OAI.Problem335.homogeneousDim

theorem OAI.Problem335.homogeneousDim_down_ratio line 120
theorem OAI.Problem335.homogeneousDim_up_ratio line 128

theorem OAI.Problem335.intermediate_dimension_ratio_le line 138

Source documentation

The product of the two degree-space ratios bounds the relative size of the intermediate space in the mixed operator factorization.

theorem intermediate_dimension_ratio_le {v u a b I J : ℕ}
    (hv : 1 ≤ v) (hu : 1 ≤ u) (hb : 0 < b) (hI : I ≤ a) :
    ((homogeneousDim v (a - I) : ℝ) * homogeneousDim u (b + J)) /
        ((homogeneousDim v a : ℝ) * homogeneousDim u b) ≤
      ((a : ℝ) / ((a : ℝ) + v - 1)) ^ I *
        (((b : ℝ) + u) / b) ^ J := by
…

Mentions: OAI.Problem335.homogeneousDim

theorem OAI.Problem335.ratio_power_slope_bound line 155
Source documentation
The slope condition balances the cost of multiplication against the cost of differentiation.
```
theorem ratio_power_slope_bound {α β ρ : ℝ} (hα : 0 < α)
    (hβ : α ^ ρ ≤ β) (I J : ℕ) :
    α ^ I / β ^ J ≤ α ^ ((I : ℝ) - ρ * J) := by
…
```

theorem OAI.Problem335.corrected_ratio_power_bound line 169

Source documentation

A bounded rounding correction can be pulled out before using the slope condition.

theorem corrected_ratio_power_bound {α β ρ η : ℝ} (hα : 0 < α)
    (hβ : α ^ ρ ≤ β) {I J : ℕ} (hη : η ^ I ≤ 2) :
    (α * η) ^ I * (β⁻¹) ^ J ≤ 2 * α ^ ((I : ℝ) - ρ * J) := by
…

theorem OAI.Problem335.intermediate_dimension_slope_bound line 182

Source documentation

The intermediate homogeneous-space bound in the balanced slope form. The only analytic hypothesis left is the small rounding correction.

theorem intermediate_dimension_slope_bound {v u a b I J : ℕ} {ρ : ℝ}
    (hv : 1 ≤ v) (hu : 1 ≤ u) (ha : 0 < a) (hb : 0 < b) (hI : I ≤ a)
    (hβ : ((a : ℝ) / ((a : ℝ) + v)) ^ ρ ≤ (b : ℝ) / ((b : ℝ) + u))
    (hcorr : ((1 - 1 / ((a : ℝ) + v))⁻¹) ^ I ≤ 2) :
    ((homogeneousDim v (a - I) : ℝ) * homogeneousDim u (b + J)) /
        ((homogeneousDim v a : ℝ) * homogeneousDim u b) ≤
      2 * ((a : ℝ) / ((a : ℝ) + v)) ^ ((I : ℝ) - ρ * J) := by
…

Mentions: OAI.Problem335.homogeneousDim