ExponentialVolumeRatio.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Exact exponential cardinality bounds from a box volume ratio

theorem OAI.PolycyclicRecognition.card_le_of_exponential_box_volume line 15

Source documentation

The fixed determinant and coordinate-cube factors cancel exactly. This includes zero-dimensional ideals.

theorem card_le_of_exponential_box_volume {n d : ℕ} {D R p q : ℝ}
    (hD : 0 < D) (hR : 0 ≤ R)
    (h : (n : ℝ≥0∞) *
        (ENNReal.ofReal D * ENNReal.ofReal (Real.exp q) * ENNReal.ofReal 2 ^ d) ≤
      ENNReal.ofReal D * ENNReal.ofReal (Real.exp p) * ENNReal.ofReal (2 * R) ^ d) :
    (n : ℝ) ≤ R ^ d * Real.exp (p - q) := by
…