OAI.TraceReconstruction.superpolynomial_sample_complexity
ProvedThe theorem states that, for every deletion probability q strictly between 0 and 1, every target success level s in (0,1], and every real exponent C>0, the ratio sampleComplexity(n,q,s) / (n^C) tends to infinity (the value ⊤ in extended nonnegative reals) as the word length n tends to infinity. Here sampleComplexity(n,q,s) is the least number m of independent traces for which some estimator exists that, for every binary word x of length n, outputs x with probability at least s. Each trace is obtained from x by an independent mask that deletes each bit with probability q and keeps it with probability 1-q, and the observer sees only the resulting list of retained bits, without positions. The estimator is a randomized rule that may depend on n, q and all m traces, assigning nonnegative probabilities summing to 1 over the candidate words. The infimum is infinity if no number of traces suffices. Thus, for fixed q and s, the number of traces needed grows faster than every fixed polynomial in n.
-- Generated from openai/math @ adc7f1241b42e322a6451854ab7e4b4c146bf78a -- Source: lean/ComparatorChallenges/TraceReconstruction.lean; bytes 3139..3411 -- Kind: theorem; original declaration names and bodies preserved. -- Source groups are independent. Target: Lean 4.33.1; see compilation.json. import Mathlib import Definitions.Def_TraceReconstruction namespace OAI open scoped ENNReal noncomputable section namespace TraceReconstruction open Filter open scoped Topology Classical ENNReal
theorem superpolynomial_sample_complexity
(q : ℝ) (hq : q ∈ Set.Ioo 0 1) (s : ℝ) (hs : s ∈ Set.Ioc 0 1)
(C : ℝ) (hC : 0 < C) :
Tendsto
(fun n : ℕ => sampleComplexity n q s / ENNReal.ofReal ((n : ℝ) ^ C))
atTop (𝓝 ⊤) := by
sorry
end TraceReconstruction
end
end OAI
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.