Fractal uncertainty in higher dimensions | Lean AI formalization leaderboard

Problem statement

Notes: Unavailable.

Source: A. Cohen, `Fractal uncertainty in higher dimensions`, Annals of Math, 202 (1) 2025. Statement taken from https://github.com/ImperialCollegeLondon/AnnalsChallenge (v1.0.0, e32eb14), AnnalsChallenge/AnnalsOfMathematics/2025-202-1-FractalUncertainty.lean

Informal solution: Unavailable.

theorem declaration uses `sorry`theorem_1_1 (ν : ℝ) (hν₀ : 0 < ν) :
    ∃ (β C : ℝ), β > 0 ∧ C > 0 ∧ ∀ (h : ℝ) (X Y : Set ℝᵈ)
      (hX : MeasurableSet X) (hY : MeasurableSet Y), h ∈ Set.Ioo 0 (1 / 100) →
        X ⊆ FractalUncertainty.cube (-1) 1 → FractalUncertainty.PorousOnBalls ν h 1 X → Y ⊆ FractalUncertainty.cube (-h⁻¹) h⁻¹ →
          FractalUncertainty.PorousOnLines ν 1 h⁻¹ Y → ∀ (f : Lp ℂ 2), (𝓕 f : Lp ℂ 2) =ᵐ[volume.restrict Yᶜ] 0 →
            (eLpNorm (X.indicator f) 2).toReal ≤ C * h ^ β * ‖f‖ := byd:ℕν:ℝhν₀:0 < ν⊢ ∃ β C,
  β > 0 ∧
    C > 0 ∧
      ∀ (h : ℝ) (X Y : Set ℝᵈ),
        MeasurableSet X →
          MeasurableSet Y →
            h ∈ Set.Ioo 0 (1 / 100) →
              X ⊆ cube (-1) 1 →
                PorousOnBalls ν h 1 X →
                  Y ⊆ cube (-h⁻¹) h⁻¹ →
                    PorousOnLines ν 1 h⁻¹ Y →
                      ∀ (f : ↥(Lp ℂ 2 volume)),
                        ↑↑(𝓕 f) =ᵐ[volume.restrict Yᶜ] 0 → (eLpNorm (X.indicator ↑↑f) 2 volume).toReal ≤ C * h ^ β * ‖f‖
  sorryAll goals completed! 🐙