DimensionCorrection.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Problem335.inverse_one_sub_pow_le_two line 9
Source documentation
A uniform Bernoulli bound for the rounding correction in the descending homogeneous-space dimension ratio.
```
theorem inverse_one_sub_pow_le_two (N : ℝ) (I : ℕ)
    (hN : 1 ≤ N) (hI : 2 * (I : ℝ) ≤ N) :
    ((1 - 1 / N) ^ I)⁻¹ ≤ 2 := by
…
```

theorem OAI.Problem335.one_sub_rpow_neg_nat_le_two line 25

Source documentation

Real-exponent version of the preceding natural-power estimate.

theorem one_sub_rpow_neg_nat_le_two (N : ℝ) (I : ℕ)
    (hN : 1 ≤ N) (hI : 2 * (I : ℝ) ≤ N) :
    (1 - 1 / N) ^ (-(I : ℝ)) ≤ 2 := by
…

theorem OAI.Problem335.corrected_ratio_product_le line 37

Source documentation

Rounding loss and the balanced multiplication cost combine into one absolute-discrepancy exponent.

theorem corrected_ratio_product_le (α β N ρ : ℝ) (I J : ℕ)
    (hα : 0 < α) (hβ : α ^ ρ ≤ β)
    (hN : 1 ≤ N) (hI : 2 * (I : ℝ) ≤ N) :
    (α / (1 - 1 / N)) ^ I * β ^ (-(J : ℝ)) ≤
      2 * α ^ ((I : ℝ) - ρ * J) := by
…

theorem OAI.Problem335.intermediate_dimension_ratio_le_balanced line 61

Source documentation

The exact intermediate-dimension bound after the harmless rounding factor has been absorbed. The hypotheses are purely numerical and field-independent.

theorem intermediate_dimension_ratio_le_balanced {v u a b I J : ℕ}
    (hv : 1 ≤ v) (hu : 1 ≤ u) (ha : 0 < a) (hb : 0 < b) (hI : I ≤ a)
    (hbudget : 2 * I ≤ a + v) (ρ : ℝ)
    (hbalance : ((a : ℝ) / ((a : ℝ) + v)) ^ ρ ≤
      (b : ℝ) / ((b : ℝ) + u)) :
    ((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

theorem OAI.Problem335.intermediate_dimension_le_balanced line 89

Source documentation

Unnormalized form of the balanced intermediate-dimension estimate.

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

Mentions: OAI.Problem335.homogeneousDim