Thresholds versus fractional expectation-thresholds | Lean AI formalization leaderboard

Problem statement

Notes: Unavailable.

Source: K. Frankston, J. Kahn, B. Narayanan, and J. Park, `Thresholds versus fractional expectation-thresholds`, Annals of Math, 194 (2) 2021. Statement taken from https://github.com/ImperialCollegeLondon/AnnalsChallenge (v1.0.0, e32eb14), AnnalsChallenge/AnnalsOfMathematics/2021-194-2-FractionalExpectationThresholds.lean

Informal solution: Unavailable.

/-- The constant `K` in Theorem 1.1. -/
noncomputable def declaration uses `sorry`K : ℝ := sorry

/--
Statement of Theorem 1.1:

There exists a universal constant `K` such that for any finite set `X` and any increasing
collection of sets `𝓕` such that `l(𝓕)` is at least `2`,

`p_c(𝓕) ≤ K * q_f(𝓕) * log l(𝓕)`.

Note: The assumption that `l(𝓕)` is at least `2` is not explicitly in the paper but is needed
because if `l(𝓕) = 1` then `Real.log (l 𝓕) = 0`, but `p_c 𝓕 ∈ (0,1)` (so the inequality clearly
cannot hold).
-/
theorem declaration uses `sorry`theorem_1_1 (X : Type*) [Fintype X] (𝓕 : Set (Set X)) (h𝓕 : IsUpperSet 𝓕)
    (hl𝓕 : 2 ≤ l 𝓕) : p_c 𝓕 ≤ K * q_f 𝓕 * Real.log (l 𝓕) := byX:Type u_1inst✝:Fintype X𝓕:Set (Set X)h𝓕:IsUpperSet 𝓕hl𝓕:2 ≤ l 𝓕⊢ ↑(p_c 𝓕) ≤ K * ↑(q_f 𝓕) * Real.log ↑(l 𝓕)
  sorryAll goals completed! 🐙