Rademacher type and Enflo type coincide | Lean AI formalization leaderboard

Problem statement

Notes: Unavailable.

Source: P. Ivanisvili, R. van Handel, and A. Volberg, `Rademacher type and Enflo type coincide`, Annals of Math, 192 (2) 2020. Statement taken from https://github.com/ImperialCollegeLondon/AnnalsChallenge (v1.0.0, e32eb14), AnnalsChallenge/AnnalsOfMathematics/2020-192-2-RademacherEnfloType.lean

Informal solution: Unavailable.

theorem declaration uses `sorry`theorem_1_1 (p : ℝ) (h1p : 1 ≤ p) (hp2 : p ≤ 2) :
    TR X p ≤ TE X p ∧ TE X p ≤ (pi / sqrt 2) * TR X p := byX:Type u_2inst✝²:NormedAddCommGroup Xinst✝¹:NormedSpace ℝ Xinst✝:CompleteSpace Xp:ℝh1p:1 ≤ php2:p ≤ 2⊢ TR X p ≤ TE X p ∧ TE X p ≤ ↑pi / ↑(sqrt 2) * TR X p
  sorryAll goals completed! 🐙