OAI.Problem310.dyadic_affine_avoidance
OpenThe theorem states that, writing dyadicPoint(n) = (1/2)^n, for every real η with 0 < η < 1 there is a set E ⊆ [0,1] of real numbers that is compact, has Lebesgue measure strictly greater than 1 − η, and avoids every nondegenerate affine copy of the dyadic sequence in the following sense: for every real x and every real s ≠ 0 there exists an integer n ≥ 1 such that x + s·(1/2)^n does not belong to E. Thus no translate-and-nonzero-dilate of the whole sequence 1/2, 1/4, 1/8, … (starting at n = 1) lies entirely inside E. The statement is an admitted theorem in the source, not a verified proof.
Preamble
-- Generated from openai/math @ adc7f1241b42e322a6451854ab7e4b4c146bf78a -- Source: lean/ComparatorChallenges/DyadicAvoidance.lean; bytes 133..442 -- 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_DyadicAvoidance namespace OAI noncomputable section namespace Problem310
Formal statement
theorem dyadic_affine_avoidance :
∀ η : ℝ, 0 < η → η < 1 → ∃ E : Set ℝ,
E ⊆ Set.Icc (0 : ℝ) 1 ∧ IsCompact E ∧
MeasureTheory.volume E > ENNReal.ofReal (1 - η) ∧
∀ x s : ℝ, s ≠ 0 → ∃ n : ℕ, 1 ≤ n ∧
x + s * dyadicPoint n ∉ E := by
sorry
end Problem310
end
end OAI
Source
Human review
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.