OAI/Analysis/PureInfiniteness/FiniteUltrapowerSaturation.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The bounded epsilon test for the finite list of polynomial conditions used by spectral abelianization, including its norm bound.

  1. theorem OAI.NormUltra.bounded_epsilon_test_finite line 17
  2. theorem OAI.NormUltra.norm_mk_le_one_of_defect_tendsto line 36