Convergence of finite-stage enumerations #
Under monotone stages, the finite stages A s of an enumeration approximate its limit in the sense
of limit approximations: any function restricted to the stages converges pointwise to the same
function restricted to the limit. In particular the set-oracle answers of the stages converge to
those of the limit set (TauCeti.Oracle.Single.Code.converges_setAnswers_stageLimit).
Main results #
TauCeti.Enumeration.converges_indicator_stageLimit: under monotone stages, the indicator functions of the stages converge to that of the limit.
theorem
TauCeti.Enumeration.converges_indicator_stageLimit
{M : Type u_1}
[Zero M]
{A : ℕ → Finset ℕ}
(hA : Monotone A)
(f : ℕ → M)
:
Approximation.Converges (fun (s : ℕ) => (↑(A s)).indicator f) ((stageLimit A).indicator f)
Under monotone stages, the indicator functions of the stages converge to the indicator function
of the limit. This is Mathlib's Monotone.indicator_eventuallyEq_iUnion for the stages.