PolynomialPackingAlgebra.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Removing box-volume polynomial factors from separated counts

theorem OAI.PolycyclicRecognition.product_box_factors_eq line 14

Source documentation

The two polynomial box radii contribute one polynomial prefactor.

theorem product_box_factors_eq {B C A x t : ℝ}
    (hB : 0 ≤ B) (hC : 0 ≤ C) (hA : 0 ≤ A) (hx : 0 ≤ x)
    (q c d e : ℕ) :
    ENNReal.ofReal B * ENNReal.ofReal (Real.exp t) *
        ENNReal.ofReal (2 * (C * x ^ q)) ^ d *
        ENNReal.ofReal (2 * (A * x ^ c)) ^ e =
      ENNReal.ofReal ((B * (2 * C) ^ d * (2 * A) ^ e) * x ^ (q * d + c * e) * Real.exp t) := by
…

theorem OAI.PolycyclicRecognition.card_le_of_ennreal_mul_bound line 33

Source documentation

Divide a separated-count inequality by its positive finite cell mass.

theorem card_le_of_ennreal_mul_bound {X : Type*} (s : Finset X)
    {Q : ℝ≥0∞} (hQ : 0 < Q) (hQfin : Q < ⊤) {R : ℝ} (hR : 0 ≤ R)
    (h : (s.card : ℝ≥0∞) * Q ≤ ENNReal.ofReal R) :
    (s.card : ℝ) ≤ R / Q.toReal := by
…

theorem OAI.PolycyclicRecognition.exists_real_card_bound_of_box_factors line 44

Source documentation

The precise two-box bound yields the usual polynomial exponential cardinality estimate with a strictly positive real constant.

theorem exists_real_card_bound_of_box_factors
    {Q : ℝ≥0∞} (hQ : 0 < Q) (hQfin : Q < ⊤)
    {B C A : ℝ} (hB : 0 ≤ B) (hC : 0 ≤ C) (hA : 0 ≤ A)
    (q c d e : ℕ) :
    ∃ D : ℝ, 0 < D ∧ ∀ {X : Type*} (s : Finset X) {x t : ℝ}, 0 ≤ x →
      (s.card : ℝ≥0∞) * Q ≤ ENNReal.ofReal B * ENNReal.ofReal (Real.exp t) *
        ENNReal.ofReal (2 * (C * x ^ q)) ^ d *
        ENNReal.ofReal (2 * (A * x ^ c)) ^ e →
      (s.card : ℝ) ≤ D * x ^ (q * d + c * e) * Real.exp t := by
…