UltrapowerCopyBounds.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Quantitative finite amplification over a commuting positive family. Each copy has the same return moments; different copies have small mixed moments.

theorem OAI.WeakPureInfiniteness.ultrapower_copy_compression_bounds line 22