OAI.RepeatedLocalization.repeated_localization
ProvedThe theorem states that the defined proposition MainStatement holds. Setting: the unknown parameter z lies in the cube [-1/(2√n), 1/(2√n))ⁿ in ℝⁿ with the uniform (normalized Lebesgue) prior, and is embedded on the unit sphere via the chart (z, √(1-Σ zₐ²)) in ℝⁿ⁺¹. A data block consists of ⌊n/16⌋ rows in ℝⁿ⁺¹ with i.i.d. standard Gaussian entries, and the exact label of row r is the inner product of that row with the chart point. An adaptive experiment of t rounds uses, at round i, a rule (depending on the previous i choices) that maps the Gaussian block and its labels to a probability vector on N choices, measurably in the data. This gives a joint law of z and the choice history w ∈ {0,…,N-1}ᵗ. A disclosure assigns, at each round i, a dyadic cell to every pair (z, w up to round i); a cell is a level J and an index in {0,…,2^J-1}ⁿ, denoting a subcube of side 1/(√n·2^J) of the initial cube. It is valid if it is measurable, takes finitely many values at each round, always contains z and lies inside the initial cube for z in the cube, and its cells are nested decreasing in i. The claim: there exist c>0 and n₀ such that for every C₀>0 there is C>0 such that, for all n ≥ n₀, N ≥ 1, t and all rule families satisfying (2/⌊n/8⌋ + exp(-c⌊n/16⌋))·log N ≤ C₀(n+1), there is a valid disclosure for which both the mutual information between z and the pair (history, sequence of disclosed cells) is at most C(n+1)t, and the expected level of the final disclosed cell (zero if t=0) under the experiment law is at most C t.
-- Generated from openai/math @ adc7f1241b42e322a6451854ab7e4b4c146bf78a -- Source: lean/ComparatorChallenges/GaussianInformation.lean; bytes 4642..4701 -- 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_GaussianInformation namespace OAI open MeasureTheory ProbabilityTheory Set open scoped BigOperators ENNReal namespace RepeatedLocalization
theorem repeated_localization : MainStatement := by sorry end RepeatedLocalization end OAI
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.