OAI.RepeatedLocalization.FiniteEntropy.finite_expected_regularization
ProvedThe theorem states that there is a threshold n₀ such that for every dimension n ≥ n₀, every dyadic cell Q of the cube [-1/(2√n),1/(2√n))^n (a pair of a level J and integer grid indices in each of n coordinates), and every probability measure P on ℝⁿ that is absolutely continuous with respect to the normalized Lebesgue measure on Q and has finite relative entropy (KL divergence) with respect to it, a certain adaptive refinement procedure behaves well. The procedure repeatedly looks, within the current conditional law and cell, for first heavy descendant cells, meaning proper dyadic descendants R at relative depth h = R.level − Q.level whose P-mass exceeds the threshold 2^(−n h/2) and which contain no smaller heavy descendant. Each attempt records either such a heavy cell containing the point z or the letter none; it moves to the recorded cell, or on none stops if the residual region outside all first heavy cells has conditional mass at least 1/2. The conclusion is a conjunction. P-almost every z reaches a stopping state (the run terminates), and the terminal log map z ↦ terminalLog is measurable. For every log h of positive P-probability, the terminal cell is a descendant of Q and the conditional law given that log is regular for that cell, meaning it gives the cell mass 1 and every proper descendant R has mass at most 2·2^(−n(R.level−cell.level)/2). The depth (terminal level minus the level of Q) and the number of attempts are P-integrable, and the expected number of attempts is at most 2(1 + expected depth). Finally, the P-integral of the relative entropy of the terminal conditional law with respect to the uniform law on the terminal cell, plus (log 2/4)·n times the expected depth, is at most KL(P ‖ uniform on Q) + 2/e, with the inequality stated in extended nonnegative reals.
-- Generated from openai/math @ adc7f1241b42e322a6451854ab7e4b4c146bf78a -- Source: lean/ComparatorChallenges/GaussianFiniteEntropy.lean; bytes 9052..9129 -- 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_GaussianFiniteEntropy namespace OAI open MeasureTheory ProbabilityTheory Set open scoped BigOperators ENNReal namespace RepeatedLocalization namespace FiniteEntropy
theorem finite_expected_regularization : FiniteEntropyStatement := by sorry end FiniteEntropy end RepeatedLocalization end OAI