Research proof index

An explicit upper bound for the number of primes below $N$: $|\{p<N:p\text{ is prime}\}|\le \frac{4N}{\log N}+6\sqrt N\left(1+\frac12\log N\right)^3.$ The formal statement also covers the small values of $N$ using Lean's totalized real operations.

NOTE: This could be generalized to 2 * N instead of 2 ^ (ϑ + 1). Also, this can be proved for ↔ instead of →.

Output-only projection corollary of fst_map_run_simulateQ.

(∂U/∂β) = -Var(E) for finite systems.

General identity: S_diff = kB β ⟨E⟩ + kB log Z_math. This connects the differential entropy to the mean energy and the mathematical partition function. Integrability of log (probability …) follows from the pointwise formula.

General entropy non-negativity under a pointwise upper bound probability ≤ 1. This assumption holds automatically in the finite/counting case (since sums bound each term), but can fail in general (continuous) settings; hence we separate it as a hypothesis. Finite case: see CanonicalEnsemble.entropy_nonneg in Finite.