Ben Green's Open Problem 54

References:

• Ben Green's Open Problem 54
• Original formulation: M. Talagrand, Are All Sets of Positive Measure Essentially Convex?, in Operator Theory: Advances and Applications, 77, 1995 Birkhäuser Verlag Basel/Switzerland.

noncomputable def Green54.gaussianMeasureInf : MeasureTheory.Measure (ℕ → ℝ)

The infinite-dimensional Gaussian measure γ∞ on ℝ^ℕ, defined as the countable product of standard Gaussian measures.

Equations

• Green54.gaussianMeasureInf = MeasureTheory.Measure.infinitePi fun (x : ℕ) => ProbabilityTheory.gaussianReal 0 1

theorem Green54.green_54 : sorry ↔ ∀ (K : Set (ℕ → ℝ)), IsCompact K → Balanced ℝ K → 0.99 ≤ gaussianMeasureInf K → ∃ (C : Set (ℕ → ℝ)), IsCompact C ∧ Convex ℝ C ∧ C ⊆ 10 • K ∧ 1e-2 ≤ gaussianMeasureInf C

Let $K \subset \mathbb{R}^n$ be a balanced compact set (that is, $\lambda K \subseteq K$ whenever $|\lambda| \leq 1$) and suppose that the normalised Gaussian measure $\gamma_n(K) \geq 0.99$. Does $10K$ contain a compact convex set $C$ with $\gamma_n(C) \geq 0.01$?

theorem Green54.green_54_known_case : ¬∀ (K : Set (ℕ → ℝ)), IsCompact K → Balanced ℝ K → 0.99 ≤ gaussianMeasureInf K → ∃ (C : Set (ℕ → ℝ)), IsCompact C ∧ Convex ℝ C ∧ C ⊆ 2 • K ∧ 1e-2 ≤ gaussianMeasureInf C

The same statement is known to be false for 2K instead of 10K.