Conjectures.io

Functional analysis

Green54.green_54

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

References

  • Original formulation: M. Talagrand, *Are All Sets of Positive Measure Essentially Convex?*, in Operator Theory:

No one has attempted this yet.

Formal statement

Lean type

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

What you must prove

import FormalConjectures.GreensOpenProblems.«54»
import TaskSupport

namespace Bounty

theorem target : fcTypeOfName% "Green54.green_54" := by
  sorry

end Bounty

Pinned source: FormalConjectures/GreensOpenProblems/54.lean

Source type SHA-256
sha256:a93e3be294669ae52648b4b3d9a2a417711cce4fd61665358e92d804e113d14d
Task id
fc-379fc029-green54-green-54-6ec57c163e-formalized-v1
Task commitment
sha256:5f2f6f4d6960b6b8ac53df6624428065451a5732d2e0d834f40d10038d984c9a

Something wrong with this formalization?

A statement that does not faithfully capture the original conjecture is the one real risk here, so we would rather hear about it early - before someone spends weeks on it.