/-
Copyright 2026 The Formal Conjectures Authors.
Licensed under the Apache License, Version 2.0 (the "License");
you may not use this file except in compliance with the License.
You may obtain a copy of the License at
https://www.apache.org/licenses/LICENSE-2.0
Unless required by applicable law or agreed to in writing, software
distributed under the License is distributed on an "AS IS" BASIS,
WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
See the License for the specific language governing permissions and
limitations under the License.
-/
module
public import FormalConjecturesUtilBen Green's Open Problem 54
References:
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.
Here $nK = K + \cdots + K$ ($n$ times) is the $n$-fold sumset of $K$, written n • K for n : ℕ
with open scoped Pointwise.
@[expose] public sectionopen MeasureTheory ProbabilityTheoryopen scoped Pointwise ENNRealnamespace Green54The infinite-dimensional Gaussian measure γ∞ on ℝ^ℕ, defined as the countable product of standard Gaussian measures.
noncomputable def gaussianMeasureInf : Measure (ℕ → ℝ) :=
Measure.infinitePi (fun _ : ℕ => gaussianReal 0 1)Let $K \subset \mathbb{R}^{\mathbb{N}}$ be a balanced compact set (that is, $\lambda K \subseteq K$ whenever $|\lambda| \leq 1$) and suppose that the normalised Gaussian measure $\gamma_\infty(K) \geq 0.99$. Does the sumset $10K = K + \cdots + K$ ($10$ times) contain a compact convex set $C$ with $\gamma_\infty(C) \geq 0.01$?
The answer is yes: Hua, Song and Tudose proved that if $\gamma_n(A) > 5/6$ then $3(A + A + A)$ contains a symmetric convex body $C$ with $\gamma_n(C) \geq 1/4$, uniformly in $n$.
@[category research solved, AMS 46 52 60]
theorem green_54 :
answer(True) ↔ ∀ K : Set (ℕ → ℝ), IsCompact K → Balanced ℝ K → (0.99 : ℝ≥0∞) ≤
gaussianMeasureInf K → ∃ C : Set (ℕ → ℝ), IsCompact C ∧ Convex ℝ C ∧ C ⊆ (10 : ℕ) • K ∧
(0.01 : ℝ≥0∞) ≤ gaussianMeasureInf C := ⊢ True ↔
∀ (K : Set (ℕ → ℝ)),
IsCompact K →
Balanced ℝ K →
0.99 ≤ gaussianMeasureInf K → ∃ C, IsCompact C ∧ Convex ℝ C ∧ C ⊆ 10 • K ∧ 1e-2 ≤ gaussianMeasureInf C
All goals completed! 🐙The same statement is known to be false for the sumset $2K = K + K$ instead of $10K$.
@[category research solved, AMS 46 52 60]
theorem green_54_known_case : ¬ (∀ K : Set (ℕ → ℝ), IsCompact K → Balanced ℝ K → (0.99 : ℝ≥0∞) ≤
gaussianMeasureInf K → ∃ C : Set (ℕ → ℝ), IsCompact C ∧ Convex ℝ C ∧ C ⊆ K + K ∧
(0.01 : ℝ≥0∞) ≤ gaussianMeasureInf C) := ⊢ ¬∀ (K : Set (ℕ → ℝ)),
IsCompact K →
Balanced ℝ K →
0.99 ≤ gaussianMeasureInf K → ∃ C, IsCompact C ∧ Convex ℝ C ∧ C ⊆ K + K ∧ 1e-2 ≤ gaussianMeasureInf C
All goals completed! 🐙end Green54