MissingMathlib

theorem HermiteLEAN.squareBlock_card (ℓ : ℕ) : (squareBlock ℓ).card = 2 * ℓ + 1

Square blocks have the expected odd cardinality.

theorem HermiteLEAN.annulus_distance_lower_bound (j : ℕ) (x : ℝ) : posPart (|↑j - x| - 1) ≤ min |↑j - x| |↑(j + 1) - x|

A convenient interval-distance lower bound for annulus arguments.

theorem HermiteLEAN.polynomial_times_gaussian_le_gaussian {a : ℝ} (ha : 0 < a) (k : ℕ) : ∃ (C : ℝ), 0 < C ∧ ∀ (x : ℝ), 0 ≤ x → (1 + x ^ k) * Real.exp (-a * x ^ 2) ≤ C * Real.exp (-(a / 2) * x ^ 2)

A reusable Gaussian absorption lemma.