MaxLeafFormal.MLS

Source file MaxLeafFormal/MLS.lean of the Lean project (how it is built).

Statements of the paper formalised here: Theorem 3.5, Lemma 3.9, Theorem 4.1, Remark 4.4, Corollary 4.3.

import Mathlib

/-!
# The probabilistic and counting core of Theorem 3.5 (exponential-moment Monotone Local Search)
-/

namespace MaxLeafFormal.MLS

open Finset

variable {U : Type*} [Fintype U] [DecidableEq U]

/-- The specification of the extension algorithm: some `Y` disjoint from `X` with
`|Y| ≤ k'` completes `X` to a solution. -/
def ExtYes (sol : Finset U → Prop) (X : Finset U) (k' : ℕ) : Prop :=
  ∃ Y : Finset U, Disjoint X Y ∧ Y.card ≤ k' ∧ sol (X ∪ Y)

/-- The exponential moment `μ_t(S)`. -/
noncomputable def mu (g : Finset U → ℕ → ℝ) (S : Finset U) (k t : ℕ) : ℝ :=
  ∑ X ∈ S.powersetCard t, (2:ℝ) ^ (-(g X (k - t)))

/-- The generating function `W_S(y)`. -/
noncomputable def W (g : Finset U → ℕ → ℝ) (S : Finset U) (k : ℕ) (y : ℝ) : ℝ :=
  ∑ X ∈ S.powerset, y ^ X.card * (2:ℝ) ^ (-(g X (k - X.card)))

/-- Condition (⋆) for the solution `S`. -/
def Star (g : Finset U → ℕ → ℝ) (S : Finset U) (k : ℕ) (ω Γ : ℝ) : Prop :=
  ∃ t ≤ k, (2:ℝ) ^ (-(ω * Fintype.card U)) / Γ
              ≤ mu g S k t / (Fintype.card U).choose t

/-! ### 1. Threshold selection (`lem:fw-threshold-prob`) -/

theorem threshold_selection {ι : Type*} (s : Finset ι) (h : ι → ℝ)
    (h0 : ∀ i ∈ s, 0 ≤ h i) (Mplus Θ : ℕ) (hM : s.card ≤ Mplus)
    (hΘ : (Mplus : ℝ) * 2 ^ (-(Θ : ℝ)) ≤ (∑ i ∈ s, (2:ℝ) ^ (-h i)) / 2) :
    ∃ θ : ℕ, θ ≤ Θ ∧
      (∑ i ∈ s, (2:ℝ) ^ (-h i)) / (4 * (Θ + 1))
        ≤ ((s.filter (fun i => h i ≤ θ)).card : ℝ) * 2 ^ (-(θ : ℝ)) := by
  classical
  set μ := ∑ i ∈ s, (2:ℝ) ^ (-h i) with hμ
  by_contra hcon
  push Not at hcon
  -- the indices above the cap contribute at most `μ/2`
  set s' := s.filter (fun i => h i ≤ Θ) with hs'
  have hhigh : ∑ i ∈ s.filter (fun i => ¬ h i ≤ Θ), (2:ℝ) ^ (-h i) ≤ μ / 2 := by
    calc ∑ i ∈ s.filter (fun i => ¬ h i ≤ Θ), (2:ℝ) ^ (-h i)
        ≤ ∑ i ∈ s.filter (fun i => ¬ h i ≤ Θ), (2:ℝ) ^ (-(Θ : ℝ)) := by
          apply sum_le_sum
          intro i hi
          rw [mem_filter] at hi
          exact Real.rpow_le_rpow_of_exponent_le (by norm_num) (by linarith [hi.2])
      _ = ((s.filter (fun i => ¬ h i ≤ Θ)).card : ℝ) * 2 ^ (-(Θ : ℝ)) := by
          rw [sum_const, nsmul_eq_mul]
      _ ≤ (Mplus : ℝ) * 2 ^ (-(Θ : ℝ)) := by
          gcongr
          exact_mod_cast (card_filter_le _ _).trans hM
      _ ≤ μ / 2 := hΘ
  have hsplit := sum_filter_add_sum_filter_not s (fun i => h i ≤ (Θ : ℝ)) (fun i => (2:ℝ) ^ (-h i))
  have hlow : μ / 2 ≤ ∑ i ∈ s', (2:ℝ) ^ (-h i) := by linarith
  -- each low index is bounded through its rounded-up value
  have hround : ∑ i ∈ s', (2:ℝ) ^ (-h i) ≤ ∑ i ∈ s', 2 * (2:ℝ) ^ (-((⌈h i⌉₊ : ℕ) : ℝ)) := by
    apply sum_le_sum
    intro i hi
    rw [mem_filter] at hi
    have hc := Nat.ceil_lt_add_one (h0 i hi.1)
    rw [show (2:ℝ) * 2 ^ (-((⌈h i⌉₊ : ℕ) : ℝ)) = 2 ^ (1 + -((⌈h i⌉₊ : ℕ) : ℝ)) by
      rw [Real.rpow_add (by norm_num), Real.rpow_one]]
    exact Real.rpow_le_rpow_of_exponent_le (by norm_num) (by linarith)
  have hmaps : ∀ i ∈ s', ⌈h i⌉₊ ∈ range (Θ + 1) := by
    intro i hi
    rw [mem_filter] at hi
    rw [mem_range, Nat.lt_succ_iff]
    exact Nat.ceil_le.2 hi.2
  have hfib := sum_fiberwise_of_maps_to hmaps (fun i => 2 * (2:ℝ) ^ (-((⌈h i⌉₊ : ℕ) : ℝ)))
  have hgroup : ∑ i ∈ s', 2 * (2:ℝ) ^ (-((⌈h i⌉₊ : ℕ) : ℝ))
      ≤ ∑ θ ∈ range (Θ + 1), 2 * (((s.filter (fun i => h i ≤ θ)).card : ℝ) * 2 ^ (-(θ : ℝ))) := by
    rw [← hfib]
    apply sum_le_sum
    intro θ _
    rw [sum_congr rfl (fun i hi => by rw [(mem_filter.1 hi).2])]
    rw [sum_const, nsmul_eq_mul]
    have : ((s'.filter (fun i => ⌈h i⌉₊ = θ)).card : ℝ) ≤ (s.filter (fun i => h i ≤ θ)).card := by
      apply Nat.cast_le.2
      apply card_le_card
      intro i hi
      simp only [hs', mem_filter] at hi ⊢
      refine ⟨hi.1.1, ?_⟩
      rw [← hi.2]
      exact Nat.le_ceil _
    have h2 : (0:ℝ) ≤ 2 ^ (-(θ : ℝ)) := by positivity
    nlinarith
  have hstrict : ∑ θ ∈ range (Θ + 1), 2 * (((s.filter (fun i => h i ≤ θ)).card : ℝ) * 2 ^ (-(θ : ℝ)))
      < ∑ θ ∈ range (Θ + 1), 2 * (μ / (4 * (Θ + 1))) := by
    apply sum_lt_sum_of_nonempty nonempty_range_add_one
    intro θ hθ
    have := hcon θ (Nat.lt_succ_iff.1 (mem_range.1 hθ))
    linarith
  rw [sum_const, card_range, nsmul_eq_mul] at hstrict
  have hΘpos : (0:ℝ) < Θ + 1 := by positivity
  have : ((Θ + 1 : ℕ) : ℝ) * (2 * (μ / (4 * (Θ + 1)))) = μ / 2 := by
    push_cast
    field_simp
    ring
  linarith

theorem threshold_upper {ι : Type*} (s : Finset ι) (h : ι → ℝ) (θ : ℤ) :
    ((s.filter (fun i => h i ≤ θ)).card : ℝ) * 2 ^ (-(θ : ℝ))
      ≤ ∑ i ∈ s, (2:ℝ) ^ (-h i) := by
  classical
  calc ((s.filter (fun i => h i ≤ θ)).card : ℝ) * 2 ^ (-(θ : ℝ))
      = ∑ i ∈ s.filter (fun i => h i ≤ θ), (2:ℝ) ^ (-(θ : ℝ)) := by
        rw [sum_const, nsmul_eq_mul]
    _ ≤ ∑ i ∈ s.filter (fun i => h i ≤ θ), (2:ℝ) ^ (-h i) := by
        apply sum_le_sum
        intro i hi
        rw [mem_filter] at hi
        exact Real.rpow_le_rpow_of_exponent_le (by norm_num) (by linarith [hi.2])
    _ ≤ ∑ i ∈ s, (2:ℝ) ^ (-h i) :=
        sum_le_sum_of_subset_of_nonneg (filter_subset _ _) (fun _ _ _ => by positivity)


/-! ### Algorithm MLS-θ -/

/-- The cap `Θ` of `eq:fw-params`. -/
noncomputable def cap (n : ℕ) (ω Γ : ℝ) : ℕ := ⌈ω * n + Real.logb 2 Γ⌉₊ + 1

/-- The trial counts `m_{t,θ}` of `eq:fw-params` (independent of `t`). -/
noncomputable def trials (n : ℕ) (ω Γ κ : ℝ) (θ : ℕ) : ℕ :=
  ⌈4 * κ * Γ * (cap n ω Γ + 1) * (2:ℝ) ^ (ω * n - θ)⌉₊

/-- Trial slots: sample size `t ≤ k`, threshold `θ ≤ Θ`, repetition `j`. -/
abbrev Slot (n k : ℕ) (ω Γ κ : ℝ) : Type :=
  Σ p : Fin (k + 1) × Fin (cap n ω Γ + 1), Fin (trials n ω Γ κ p.2)

/-- MLS-θ accepts the outcome `o`. -/
def Accepts (sol : Finset U → Prop) (g : Finset U → ℕ → ℝ) (k : ℕ) (ω Γ κ : ℝ)
    (o : Slot (Fintype.card U) k ω Γ κ → Finset U) : Prop :=
  ∃ j, g (o j) (k - j.1.1) ≤ (j.1.2 : ℕ) ∧ ExtYes sol (o j) (k - j.1.1)

/-- Product of uniform measures on `t`-subsets, one factor per slot. -/
noncomputable def trialMeasure (k : ℕ) (ω Γ κ : ℝ) :
    MeasureTheory.Measure (Slot (Fintype.card U) k ω Γ κ → Finset U) :=
  MeasureTheory.Measure.pi fun j =>
    ProbabilityTheory.uniformOn ((powersetCard (j.1.1 : ℕ) (univ : Finset U) : Finset (Finset U)) :
      Set (Finset U))

/-! ### 2. Soundness (`thm:fw-main` (ii)) -/

theorem mls_sound (sol : Finset U → Prop) (g : Finset U → ℕ → ℝ) (k : ℕ)
    (ω Γ κ : ℝ) (o : Slot (Fintype.card U) k ω Γ κ → Finset U)
    (ho : ∀ j, (o j).card = j.1.1) (h : Accepts sol g k ω Γ κ o) :
    ∃ S, sol S ∧ S.card ≤ k := by
  obtain ⟨j, -, Y, hdisj, hY, hsol⟩ := h
  refine ⟨o j ∪ Y, hsol, ?_⟩
  rw [card_union_of_disjoint hdisj, ho j]
  have := j.1.1.isLt
  omega

/-! ### 4. Time budget (arithmetic content of `thm:fw-main` (i)) -/

theorem cap_pow_le (n : ℕ) (ω Γ : ℝ) (hω : 0 ≤ ω) (hΓ : 1 ≤ Γ) :
    (2:ℝ) ^ (cap n ω Γ) ≤ 4 * Γ * 2 ^ (ω * n) := by
  have hx : 0 ≤ ω * n + Real.logb 2 Γ :=
    add_nonneg (by positivity) (Real.logb_nonneg (by norm_num) hΓ)
  have hc := Nat.ceil_lt_add_one hx
  have hΓ0 : 0 < Γ := by linarith
  calc (2:ℝ) ^ (cap n ω Γ) = (2:ℝ) ^ ((cap n ω Γ : ℕ) : ℝ) := (Real.rpow_natCast _ _).symm
    _ ≤ (2:ℝ) ^ (ω * n + Real.logb 2 Γ + 2) := by
        apply Real.rpow_le_rpow_of_exponent_le (by norm_num)
        unfold cap
        push_cast
        linarith
    _ = 4 * Γ * 2 ^ (ω * n) := by
        rw [Real.rpow_add (by norm_num), Real.rpow_add (by norm_num),
          Real.rpow_logb (by norm_num) (by norm_num) hΓ0]
        norm_num
        ring

theorem mls_budget (n k : ℕ) (ω Γ κ : ℝ) (hω : 0 ≤ ω) (hΓ : 1 ≤ Γ) (hκ : 0 < κ) :
    (2:ℝ) ^ (cap n ω Γ) ≤ 4 * Γ * 2 ^ (ω * n) ∧
    ∑ t ∈ range (k + 1), ∑ θ ∈ range (cap n ω Γ + 1),
        (trials n ω Γ κ θ : ℝ) * 2 ^ (θ + 1)
      ≤ (k + 1) * (cap n ω Γ + 1) *
          (8 * κ * Γ * (cap n ω Γ + 1) * 2 ^ (ω * n) + 2 ^ (cap n ω Γ + 1)) := by
  refine ⟨cap_pow_le n ω Γ hω hΓ, ?_⟩
  set Θ := cap n ω Γ
  have hpair : ∀ θ ∈ range (Θ + 1), (trials n ω Γ κ θ : ℝ) * 2 ^ (θ + 1)
      ≤ 8 * κ * Γ * (Θ + 1) * 2 ^ (ω * n) + 2 ^ (Θ + 1) := by
    intro θ hθ
    have hθ' : θ ≤ Θ := Nat.lt_succ_iff.1 (mem_range.1 hθ)
    have harg : 0 ≤ 4 * κ * Γ * (Θ + 1) * (2:ℝ) ^ (ω * n - θ) := by
      have : (0:ℝ) ≤ Γ := by linarith
      positivity
    have hc := Nat.ceil_lt_add_one harg
    have h2 : (2:ℝ) ^ (ω * n - θ) * 2 ^ (θ + 1) = 2 * 2 ^ (ω * n) := by
      rw [← Real.rpow_natCast, ← Real.rpow_add (by norm_num)]
      rw [show ω * n - (θ : ℝ) + ((θ + 1 : ℕ) : ℝ) = 1 + ω * n by push_cast; ring,
        Real.rpow_add (by norm_num), Real.rpow_one]
    have hpow : (2:ℝ) ^ (θ + 1) ≤ 2 ^ (Θ + 1) := pow_le_pow_right₀ (by norm_num) (by omega)
    have hp0 : (0:ℝ) ≤ 2 ^ (θ + 1) := by positivity
    calc (trials n ω Γ κ θ : ℝ) * 2 ^ (θ + 1)
        ≤ (4 * κ * Γ * (Θ + 1) * (2:ℝ) ^ (ω * n - θ) + 1) * 2 ^ (θ + 1) := by
          unfold trials
          gcongr
      _ = 8 * κ * Γ * (Θ + 1) * 2 ^ (ω * n) + 2 ^ (θ + 1) := by
          rw [add_mul, mul_assoc (4 * κ * Γ * (Θ + 1)), h2]
          ring
      _ ≤ 8 * κ * Γ * (Θ + 1) * 2 ^ (ω * n) + 2 ^ (Θ + 1) := by linarith
  calc ∑ t ∈ range (k + 1), ∑ θ ∈ range (Θ + 1), (trials n ω Γ κ θ : ℝ) * 2 ^ (θ + 1)
      ≤ ∑ t ∈ range (k + 1), ∑ θ ∈ range (Θ + 1),
          (8 * κ * Γ * (Θ + 1) * 2 ^ (ω * n) + 2 ^ (Θ + 1)) :=
        sum_le_sum fun _ _ => sum_le_sum hpair
    _ = (k + 1) * (Θ + 1) * (8 * κ * Γ * (Θ + 1) * 2 ^ (ω * n) + 2 ^ (Θ + 1)) := by
        simp only [sum_const, card_range, nsmul_eq_mul]
        push_cast
        ring

/-! ### 5. Generating-function condition -/

theorem W_eq_sum_mu (g : Finset U → ℕ → ℝ) (S : Finset U) (k : ℕ) (hSk : S.card = k) (y : ℝ) :
    W g S k y = ∑ t ∈ range (k + 1), y ^ t * mu g S k t := by
  unfold W mu
  have hmaps : ∀ X ∈ S.powerset, X.card ∈ range (k + 1) := fun X hX =>
    mem_range.2 (Nat.lt_succ_of_le (hSk ▸ card_le_card (mem_powerset.1 hX)))
  rw [← sum_fiberwise_of_maps_to hmaps]
  refine sum_congr rfl fun t _ => ?_
  rw [mul_sum, ← powersetCard_eq_filter]
  refine sum_congr rfl fun X hX => ?_
  rw [(mem_powersetCard.1 hX).2]

theorem star_of_W (g : Finset U → ℕ → ℝ) (S : Finset U) (k : ℕ) (hSk : S.card = k)
    (ω Γ y : ℝ) (hΓ : 0 < Γ) (hy : 0 ≤ y)
    (hW : (1 + y) ^ Fintype.card U * (2:ℝ) ^ (-(ω * Fintype.card U)) / Γ ≤ W g S k y) :
    Star g S k ω Γ := by
  set n := Fintype.card U
  set c := (2:ℝ) ^ (-(ω * n)) / Γ with hc
  have hc0 : 0 < c := by positivity
  by_contra hcon
  simp only [Star, not_exists, not_and, not_le] at hcon
  have hkn : k ≤ n := hSk ▸ card_le_univ S
  have hlt : ∀ t ∈ range (k + 1), mu g S k t < c * n.choose t := by
    intro t ht
    have h1 := hcon t (Nat.lt_succ_iff.1 (mem_range.1 ht))
    have hpos : (0:ℝ) < n.choose t :=
      Nat.cast_pos.2 (Nat.choose_pos ((Nat.lt_succ_iff.1 (mem_range.1 ht)).trans hkn))
    rwa [div_lt_iff₀ hpos] at h1
  have hsum : W g S k y < ∑ t ∈ range (k + 1), y ^ t * (c * n.choose t) := by
    rw [W_eq_sum_mu g S k hSk, ← sum_erase_add _ _ (mem_range.2 (Nat.succ_pos k)),
      ← sum_erase_add _ _ (mem_range.2 (Nat.succ_pos k))]
    apply add_lt_add_of_le_of_lt
    · exact sum_le_sum fun t ht =>
        mul_le_mul_of_nonneg_left (hlt t (mem_of_mem_erase ht)).le (pow_nonneg hy t)
    · simpa using hlt 0 (mem_range.2 (Nat.succ_pos k))
  have hbin : ∑ t ∈ range (k + 1), y ^ t * (c * n.choose t) ≤ c * (1 + y) ^ n := by
    rw [add_comm 1 y, add_pow, mul_sum]
    calc ∑ t ∈ range (k + 1), y ^ t * (c * n.choose t)
        ≤ ∑ t ∈ range (n + 1), y ^ t * (c * n.choose t) :=
          sum_le_sum_of_subset_of_nonneg (fun x hx => by simp only [mem_range] at hx ⊢; omega)
            (fun _ _ _ => by positivity)
      _ = ∑ t ∈ range (n + 1), c * (y ^ t * 1 ^ (n - t) * n.choose t) :=
          sum_congr rfl fun _ _ => by ring
  have : (1 + y) ^ n * (2:ℝ) ^ (-(ω * n)) / Γ = c * (1 + y) ^ n := by rw [hc]; ring
  linarith

/-! ### 6. Mean-cost route (Jensen step of `thm:co-mean`) -/

theorem mu_ge_of_mean (g : Finset U → ℕ → ℝ) (S : Finset U) (k t : ℕ)
    (hSk : S.card = k) (ht : t ≤ k) (lam : ℝ)
    (hmean : (∑ X ∈ S.powersetCard t, g X (k - t)) / k.choose t ≤ lam) :
    (k.choose t : ℝ) * 2 ^ (-lam) ≤ mu g S k t := by
  set N : ℝ := (k.choose t : ℝ)
  have hN : 0 < N := Nat.cast_pos.2 (Nat.choose_pos ht)
  set m := (∑ X ∈ S.powersetCard t, g X (k - t)) / N with hm
  have hl2 : 0 < Real.log 2 := Real.log_pos (by norm_num)
  -- tangent line of `x ↦ 2^(-x)` at `m`
  have htan : ∀ a : ℝ, (2:ℝ) ^ (-m) * (1 - (a - m) * Real.log 2) ≤ (2:ℝ) ^ (-a) := by
    intro a
    have h := Real.add_one_le_exp (-(a - m) * Real.log 2)
    rw [Real.rpow_def_of_pos (by norm_num), Real.rpow_def_of_pos (by norm_num)]
    calc Real.exp (Real.log 2 * -m) * (1 - (a - m) * Real.log 2)
        ≤ Real.exp (Real.log 2 * -m) * Real.exp (-(a - m) * Real.log 2) := by
          gcongr; linarith
      _ = Real.exp (Real.log 2 * -a) := by rw [← Real.exp_add]; ring_nf
  have hcard : ((S.powersetCard t).card : ℝ) = N := by rw [card_powersetCard, hSk]
  have hsum : ∑ X ∈ S.powersetCard t, (2:ℝ) ^ (-m) * (1 - (g X (k - t) - m) * Real.log 2)
      = N * 2 ^ (-m) := by
    rw [← mul_sum, sum_sub_distrib, sum_const, ← sum_mul, sum_sub_distrib, sum_const,
      nsmul_eq_mul, nsmul_eq_mul, hcard]
    have : ∑ X ∈ S.powersetCard t, g X (k - t) = N * m := by rw [hm]; field_simp
    rw [this]; ring
  calc N * 2 ^ (-lam) ≤ N * 2 ^ (-m) := by
        gcongr
        norm_num
    _ = _ := hsum.symm
    _ ≤ mu g S k t := sum_le_sum fun X _ => htan _


/-! ### 3. Success probability (`thm:fw-main` (iii)) -/

/-- Mathlib's σ-algebra on `Finset U` (generated by the membership tests) is discrete
when `U` is finite. -/
instance : MeasurableSingletonClass (Finset U) := by
  refine ⟨fun s0 => ?_⟩
  have : ({s0} : Set (Finset U)) = ⋂ a : U, (fun s : Finset U => a ∈ s) ⁻¹' {a ∈ s0} := by
    ext s
    simp only [Set.mem_singleton_iff, Set.mem_iInter, Set.mem_preimage, eq_iff_iff]
    constructor
    · rintro rfl a; exact Iff.rfl
    · intro h; ext a; exact h a
  rw [this]
  exact MeasurableSet.iInter fun a =>
    (measurable_finset_iff.1 measurable_id a) (measurableSet_singleton _)

theorem trialMeasure_factor_prob (k : ℕ) (hk : k ≤ Fintype.card U) (ω Γ κ : ℝ)
    (j : Slot (Fintype.card U) k ω Γ κ) :
    MeasureTheory.IsProbabilityMeasure (ProbabilityTheory.uniformOn
      ((powersetCard (j.1.1 : ℕ) (univ : Finset U) : Finset (Finset U)) : Set (Finset U))) := by
  apply ProbabilityTheory.isProbabilityMeasure_uniformOn (Finset.finite_toSet _)
  rw [Finset.coe_nonempty, powersetCard_nonempty, card_univ]
  have := j.1.1.isLt
  omega

theorem mls_success (sol : Finset U → Prop) (g : Finset U → ℕ → ℝ)
    (hg : ∀ X k', 0 ≤ g X k') (k : ℕ) (hk : k ≤ Fintype.card U)
    (ω Γ κ : ℝ) (hω : 0 ≤ ω) (hΓ : 1 ≤ Γ) (hκ : 0 < κ)
    (S : Finset U) (hS : sol S) (hSk : S.card = k) (hstar : Star g S k ω Γ) :
    1 - Real.exp (-κ)
      ≤ (trialMeasure k ω Γ κ {o | Accepts sol g k ω Γ κ o}).toReal := by
  classical
  open MeasureTheory ProbabilityTheory in
  set n := Fintype.card U with hn
  set Θ := cap n ω Γ with hΘdef
  obtain ⟨t, htk, hstar⟩ := hstar
  have htn : t ≤ n := htk.trans hk
  have hΓ0 : 0 < Γ := by linarith
  set N : ℝ := (n.choose t : ℝ) with hN
  have hNpos : 0 < N := Nat.cast_pos.2 (Nat.choose_pos htn)
  set M := mu g S k t with hM
  have hMN : N * (2:ℝ) ^ (-(ω * n)) / Γ ≤ M := by
    rw [le_div_iff₀ hNpos] at hstar
    calc N * (2:ℝ) ^ (-(ω * n)) / Γ = 2 ^ (-(ω * n)) / Γ * N := by ring
      _ ≤ M := hstar
  -- the cap is high enough: `2^{-Θ} ≤ 2^{-ωn} / (2Γ)`
  have hcapexp : (2:ℝ) ^ (-((Θ : ℕ) : ℝ)) ≤ (2:ℝ) ^ (-(ω * n)) / Γ / 2 := by
    have hx := Nat.le_ceil (ω * n + Real.logb 2 Γ)
    calc (2:ℝ) ^ (-((Θ : ℕ) : ℝ)) ≤ (2:ℝ) ^ (-(ω * n + Real.logb 2 Γ + 1)) := by
          apply Real.rpow_le_rpow_of_exponent_le (by norm_num)
          rw [hΘdef]; unfold cap; push_cast; linarith
      _ = (2:ℝ) ^ (-(ω * n)) / Γ / 2 := by
          rw [show -(ω * n + Real.logb 2 Γ + 1) = -(ω * n) + -Real.logb 2 Γ + -1 by ring,
            Real.rpow_add (by norm_num), Real.rpow_add (by norm_num),
            Real.rpow_neg (by norm_num : (0:ℝ) ≤ 2) (Real.logb 2 Γ),
            Real.rpow_logb (by norm_num) (by norm_num) hΓ0, Real.rpow_neg_one]
          ring
  -- threshold selection
  obtain ⟨θ, hθΘ, hθ⟩ := threshold_selection (S.powersetCard t) (fun X => g X (k - t))
    (fun X _ => hg X _) (n.choose t) Θ
    (by rw [card_powersetCard, hSk]; exact Nat.choose_le_choose t hk)
    (by
      change N * _ ≤ M / 2
      calc N * (2:ℝ) ^ (-((Θ : ℕ) : ℝ)) ≤ N * ((2:ℝ) ^ (-(ω * n)) / Γ / 2) := by gcongr
        _ = N * (2:ℝ) ^ (-(ω * n)) / Γ / 2 := by ring
        _ ≤ M / 2 := by linarith)
  set G := (S.powersetCard t).filter (fun X => g X (k - t) ≤ θ) with hGdef
  change M / (4 * (Θ + 1)) ≤ (G.card : ℝ) * 2 ^ (-(θ : ℝ)) at hθ
  set q : ℝ := (G.card : ℝ)
  set p : ℝ := q / N with hp
  set m := trials n ω Γ κ θ with hm
  -- `p * m ≥ κ`
  have hpm : κ ≤ p * m := by
    have hmge : 4 * κ * Γ * (Θ + 1) * (2:ℝ) ^ (ω * n - θ) ≤ m := Nat.le_ceil _
    have h2θ : (2:ℝ) ^ (θ : ℝ) * 2 ^ (-(θ : ℝ)) = 1 := by
      rw [← Real.rpow_add (by norm_num)]; simp
    have hq : (2:ℝ) ^ (θ : ℝ) * M / (4 * (Θ + 1)) ≤ q := by
      have := mul_le_mul_of_nonneg_left hθ (by positivity : (0:ℝ) ≤ 2 ^ (θ : ℝ))
      calc (2:ℝ) ^ (θ : ℝ) * M / (4 * (Θ + 1)) = 2 ^ (θ : ℝ) * (M / (4 * (Θ + 1))) := by ring
        _ ≤ 2 ^ (θ : ℝ) * (q * 2 ^ (-(θ : ℝ))) := this
        _ = q := by rw [mul_comm q, ← mul_assoc, h2θ, one_mul]
    have hsplit : (2:ℝ) ^ (ω * n - θ) = 2 ^ (ω * n) * 2 ^ (-(θ : ℝ)) := by
      rw [sub_eq_add_neg, Real.rpow_add (by norm_num)]
    have hinv : (2:ℝ) ^ (ω * n) * 2 ^ (-(ω * n)) = 1 := by
      rw [← Real.rpow_add (by norm_num)]; simp
    have hΘ1 : (0:ℝ) < Θ + 1 := by positivity
    -- `p ≥ 2^θ M /(4(Θ+1) N) ≥ 2^θ 2^{-ωn} / (4 Γ (Θ+1))`
    have hp_ge : (2:ℝ) ^ (θ : ℝ) * 2 ^ (-(ω * n)) / (4 * Γ * (Θ + 1)) ≤ p := by
      rw [hp, le_div_iff₀ hNpos]
      calc (2:ℝ) ^ (θ : ℝ) * 2 ^ (-(ω * n)) / (4 * Γ * (Θ + 1)) * N
          = (2:ℝ) ^ (θ : ℝ) * (N * (2:ℝ) ^ (-(ω * n)) / Γ) / (4 * (Θ + 1)) := by
            field_simp
        _ ≤ (2:ℝ) ^ (θ : ℝ) * M / (4 * (Θ + 1)) := by gcongr
        _ ≤ q := hq
    have hp0 : 0 ≤ (2:ℝ) ^ (θ : ℝ) * 2 ^ (-(ω * n)) / (4 * Γ * (Θ + 1)) := by positivity
    calc κ = (2:ℝ) ^ (θ : ℝ) * 2 ^ (-(ω * n)) / (4 * Γ * (Θ + 1))
              * (4 * κ * Γ * (Θ + 1) * (2:ℝ) ^ (ω * n - θ)) := by
          rw [hsplit]
          field_simp
          rw [show (2:ℝ) ^ (θ : ℝ) * 2 ^ (-(ω * n)) * 2 ^ (ω * n) * 2 ^ (-(θ : ℝ))
              = (2 ^ (ω * n) * 2 ^ (-(ω * n))) * (2 ^ (θ : ℝ) * 2 ^ (-(θ : ℝ))) by ring,
            hinv, h2θ]
          ring
      _ ≤ p * m := mul_le_mul hp_ge hmge (by positivity) (hp0.trans hp_ge)
  -- the probability model
  have hfac := trialMeasure_factor_prob (U := U) k hk ω Γ κ
  set μ := trialMeasure (U := U) k ω Γ κ with hμ
  have : IsProbabilityMeasure μ := by
    rw [hμ]; unfold trialMeasure
    have := hfac
    infer_instance
  set A := {o | Accepts sol g k ω Γ κ o}
  set P : Fin (k + 1) × Fin (Θ + 1) := (⟨t, Nat.lt_succ_of_le htk⟩, ⟨θ, Nat.lt_succ_of_le hθΘ⟩)
  set T : Finset (Finset U) := powersetCard t (univ : Finset U)
  set B : Set (Slot n k ω Γ κ → Finset U) :=
    Set.pi Set.univ (fun j => if j.1 = P then ((G : Set (Finset U)))ᶜ else Set.univ)
  have hAB : Aᶜ ⊆ B := by
    intro o ho j _
    dsimp only
    by_cases hj : j.1 = P
    · rw [ite_eq_left_iff.mpr (fun h => absurd hj h)]
      intro hoj
      apply ho
      have hj1 : (j.1.1 : ℕ) = t := by rw [hj]
      have hj2 : (j.1.2 : ℕ) = θ := by rw [hj]
      rw [Finset.mem_coe, hGdef, mem_filter, mem_powersetCard] at hoj
      refine ⟨j, ?_, S \ o j, disjoint_sdiff, ?_, ?_⟩
      · rw [hj1, hj2]; exact hoj.2
      · rw [card_sdiff_of_subset hoj.1.1, hSk, hoj.1.2, hj1]
      · rwa [union_sdiff_of_subset hoj.1.1]
    · rw [if_neg hj]; exact Set.mem_univ _
  -- the factor of a block slot
  have hGT : G ⊆ T := fun X hX => by
    rw [hGdef, mem_filter, mem_powersetCard] at hX
    exact mem_powersetCard.2 ⟨subset_univ _, hX.1.2⟩
  have hfacG : ∀ j : Slot n k ω Γ κ, j.1 = P →
      (uniformOn ((powersetCard (j.1.1 : ℕ) (univ : Finset U) : Finset (Finset U)) :
        Set (Finset U)) (G : Set (Finset U))ᶜ).toReal = 1 - p := by
    intro j hj
    have hj1 : (j.1.1 : ℕ) = t := by rw [hj]
    haveI := hfac j
    rw [prob_compl_eq_one_sub (Finset.measurableSet _), ENNReal.toReal_sub_of_le prob_le_one
      ENNReal.one_ne_top, ENNReal.toReal_one, hj1, uniformOn_apply_finset,
      inter_eq_right.2 hGT, ENNReal.toReal_div, ENNReal.toReal_natCast, ENNReal.toReal_natCast,
      card_powersetCard, card_univ]
  have hB : (μ B).toReal = (1 - p) ^ m := by
    rw [hμ]; unfold trialMeasure
    rw [Measure.pi_pi, ENNReal.toReal_prod]
    rw [Fintype.prod_sigma]
    rw [Fintype.prod_eq_single P]
    · rw [Finset.prod_congr rfl (fun i _ => by rw [if_pos rfl, hfacG ⟨P, i⟩ rfl]),
        prod_const, card_univ, Fintype.card_fin]
    · intro P' hP'
      refine Finset.prod_eq_one fun i _ => ?_
      rw [if_neg hP']
      haveI := hfac ⟨P', i⟩
      rw [measure_univ, ENNReal.toReal_one]
  -- conclude
  have hp1 : p ≤ 1 := by
    rw [hp, div_le_one hNpos, hN]
    have : G.card ≤ T.card := card_le_card hGT
    rw [card_powersetCard, card_univ] at this
    change (G.card : ℝ) ≤ _
    exact_mod_cast this
  have hexp : (1 - p) ^ m ≤ Real.exp (-κ) := by
    calc (1 - p) ^ m ≤ (Real.exp (-p)) ^ m := by
          apply pow_le_pow_left₀ (by linarith)
          linarith [Real.add_one_le_exp (-p)]
      _ = Real.exp (-(p * m)) := by rw [← Real.exp_nat_mul]; ring_nf
      _ ≤ Real.exp (-κ) := Real.exp_le_exp.2 (by linarith)
  have hAc : (μ Aᶜ).toReal ≤ Real.exp (-κ) := by
    calc (μ Aᶜ).toReal ≤ (μ B).toReal :=
          ENNReal.toReal_mono (measure_ne_top _ _) (measure_mono hAB)
      _ ≤ _ := hB ▸ hexp
  have hsum : (μ A).toReal + (μ Aᶜ).toReal = 1 := by
    have := measureReal_add_measureReal_compl (μ := μ) (MeasurableSet.of_discrete (s := A))
    simpa [Measure.real] using this
  linarith

theorem mls_success_of_mean (sol : Finset U → Prop) (g : Finset U → ℕ → ℝ)
    (hg : ∀ X k', 0 ≤ g X k') (k t : ℕ) (ht : t ≤ k) (hn : 1 ≤ Fintype.card U)
    (lam κ : ℝ) (hlam : 0 ≤ lam) (hκ : 0 < κ)
    (S : Finset U) (hS : sol S) (hSk : S.card = k)
    (hmean : (∑ X ∈ S.powersetCard t, g X (k - t)) / k.choose t ≤ lam) :
    let ω := (Real.logb 2 ((Fintype.card U).choose t / k.choose t) + lam)
               / Fintype.card U
    1 - Real.exp (-κ)
      ≤ (trialMeasure k ω 1 κ {o | Accepts sol g k ω 1 κ o}).toReal := by
  intro ω
  set n := Fintype.card U
  have hkn : k ≤ n := hSk ▸ card_le_univ S
  have hn0 : (0:ℝ) < n := by exact_mod_cast hn
  have hNk : (0:ℝ) < k.choose t := Nat.cast_pos.2 (Nat.choose_pos ht)
  have hNn : (0:ℝ) < n.choose t := Nat.cast_pos.2 (Nat.choose_pos (ht.trans hkn))
  have hratio : (1:ℝ) ≤ (n.choose t : ℝ) / k.choose t := by
    rw [one_le_div hNk]; exact_mod_cast Nat.choose_le_choose t hkn
  have hωn : ω * n = Real.logb 2 ((n.choose t : ℝ) / k.choose t) + lam := by
    change (_ / (n : ℝ)) * n = _
    field_simp
    rfl
  have hω : 0 ≤ ω := by
    change 0 ≤ _ / (n : ℝ)
    exact div_nonneg (add_nonneg (Real.logb_nonneg (by norm_num) hratio) hlam) hn0.le
  apply mls_success sol g hg k hkn ω 1 κ hω le_rfl hκ S hS hSk
  refine ⟨t, ht, ?_⟩
  have hmu := mu_ge_of_mean g S k t hSk ht lam hmean
  rw [div_one, hωn, le_div_iff₀ hNn, neg_add, Real.rpow_add (by norm_num), Real.rpow_neg
    (by norm_num) (Real.logb _ _), Real.rpow_logb (by norm_num) (by norm_num)
    (by positivity), inv_div]
  calc (k.choose t : ℝ) / n.choose t * 2 ^ (-lam) * n.choose t = k.choose t * 2 ^ (-lam) := by
        field_simp
    _ ≤ mu g S k t := hmu


/-! ## One sample size (`rem:co-fsigma`) and linear mean savings (`cor:co-linear`) -/

open Real in
/-- Binary entropy in base 2. -/
noncomputable def H2 (x : ℝ) : ℝ := Real.binEntropy x / Real.log 2

noncomputable def fσ (σ β ρ τ : ℝ) : ℝ := H2 τ - σ * H2 (τ / σ) + β - ρ * τ

noncomputable def Fstar (σ β ρ : ℝ) : ℝ :=
  if σ ≤ 2 ^ (-ρ) then β
  else β - σ * ρ + H2 σ + (1 - σ) * Real.logb 2 (1 - 2 ^ (-ρ))

noncomputable def τstar (σ ρ : ℝ) : ℝ :=
  if σ ≤ 2 ^ (-ρ) then 0 else (σ - 2 ^ (-ρ)) / (1 - 2 ^ (-ρ))

section OneSize

open Real

/-- Closed form of `fσ` (the expansion of the entropies in `rem:co-fsigma`), in natural logarithms. -/
noncomputable def fClosed (σ β ρ τ : ℝ) : ℝ :=
  (negMulLog (1 - τ) - negMulLog (σ - τ) + negMulLog σ) / log 2 + β - ρ * τ

theorem fσ_eq_closed {σ : ℝ} (hσ : σ ≠ 0) (β ρ : ℝ) : fσ σ β ρ = fClosed σ β ρ := by
  funext τ
  unfold fσ fClosed H2
  rw [binEntropy_eq_negMulLog_add_negMulLog_one_sub,
    binEntropy_eq_negMulLog_add_negMulLog_one_sub]
  have h1 := negMulLog_mul σ (τ / σ)
  have h2 := negMulLog_mul σ (1 - τ / σ)
  rw [mul_div_cancel₀ _ hσ] at h1
  rw [show σ * (1 - τ / σ) = σ - τ by field_simp] at h2
  have : σ * (negMulLog (τ / σ) + negMulLog (1 - τ / σ))
      = negMulLog τ + negMulLog (σ - τ) - negMulLog σ := by
    linear_combination -h1 - h2
  rw [← mul_div_assoc, this]
  ring

/-- The derivative of the closed form. -/
noncomputable def dClosed (σ ρ τ : ℝ) : ℝ := (log (1 - τ) - log (σ - τ)) / log 2 - ρ

theorem hasDerivAt_fClosed {σ τ : ℝ} (β ρ : ℝ) (h1 : τ < 1) (h2 : τ < σ) :
    HasDerivAt (fClosed σ β ρ) (dClosed σ ρ τ) τ := by
  have ha : HasDerivAt (fun x => negMulLog (1 - x)) ((-log (1 - τ) - 1) * (-1)) τ :=
    (hasDerivAt_negMulLog (by linarith)).comp τ ((hasDerivAt_id τ).const_sub 1)
  have hb : HasDerivAt (fun x => negMulLog (σ - x)) ((-log (σ - τ) - 1) * (-1)) τ :=
    (hasDerivAt_negMulLog (by linarith)).comp τ ((hasDerivAt_id τ).const_sub σ)
  have := ((((ha.sub hb).add_const (negMulLog σ)).div_const (log 2)).add_const β).sub
    ((hasDerivAt_id τ).const_mul ρ)
  unfold fClosed dClosed
  convert this using 1
  · funext x; simp only [Pi.sub_apply, Pi.add_apply, id]
  · ring

theorem continuous_fClosed (σ β ρ : ℝ) : Continuous (fClosed σ β ρ) := by
  unfold fClosed
  fun_prop

/-- Sign of the derivative: compare `σ - τ` with `p(1 - τ)`, `p = 2^{-ρ}`. -/
theorem dClosed_eq {σ τ : ℝ} (ρ : ℝ) (h1 : τ < 1) :
    dClosed σ ρ τ = (log ((2:ℝ) ^ (-ρ) * (1 - τ)) - log (σ - τ)) / log 2 := by
  have hl : 0 < log 2 := log_pos (by norm_num)
  unfold dClosed
  rw [log_mul (by positivity) (by linarith), log_rpow (by norm_num)]
  field_simp
  ring

theorem dClosed_pos {σ τ : ℝ} (ρ : ℝ) (h1 : τ < 1) (h2 : τ < σ)
    (h : σ - τ < (2:ℝ) ^ (-ρ) * (1 - τ)) : 0 < dClosed σ ρ τ := by
  rw [dClosed_eq ρ h1]
  apply div_pos _ (log_pos (by norm_num))
  rw [sub_pos]
  exact log_lt_log (by linarith) h

theorem dClosed_neg {σ τ : ℝ} (ρ : ℝ) (h1 : τ < 1) (h0 : 0 ≤ τ) (h2 : τ < σ)
    (h : (2:ℝ) ^ (-ρ) * (1 - τ) < σ - τ) : dClosed σ ρ τ < 0 := by
  rw [dClosed_eq ρ h1]
  apply div_neg_of_neg_of_pos _ (log_pos (by norm_num))
  rw [sub_neg]
  exact log_lt_log (by have : (0:ℝ) < 2 ^ (-ρ) := by positivity
                       nlinarith) h

theorem fClosed_zero (σ β ρ : ℝ) : fClosed σ β ρ 0 = β := by
  unfold fClosed
  simp

/-- The core of `rem:co-fsigma`: `τ*` lies in `[0, σ]`, attains `F*`, and every other point
of `[0, σ]` has a strictly larger value. -/
theorem onesize_core (σ β ρ : ℝ) (hσ : σ ∈ Set.Ioo 0 1) (hρ : 0 ≤ ρ) :
    τstar σ ρ ∈ Set.Icc 0 σ ∧ fClosed σ β ρ (τstar σ ρ) = Fstar σ β ρ ∧
      ∀ τ ∈ Set.Icc 0 σ, τ ≠ τstar σ ρ → Fstar σ β ρ < fClosed σ β ρ τ := by
  obtain ⟨hσ0, hσ1⟩ := hσ
  set p : ℝ := (2:ℝ) ^ (-ρ) with hp
  have hp0 : 0 < p := by positivity
  have hp1 : p ≤ 1 := by
    rw [hp]; exact rpow_le_one_of_one_le_of_nonpos (by norm_num) (by linarith)
  have hcont := (continuous_fClosed σ β ρ).continuousOn (s := Set.Icc 0 σ)
  have hderiv : ∀ τ ∈ Set.Ioo 0 σ, deriv (fClosed σ β ρ) τ = dClosed σ ρ τ := fun τ hτ =>
    (hasDerivAt_fClosed β ρ (by linarith [hτ.2]) hτ.2).deriv
  by_cases hcase : σ ≤ p
  · -- the minimum is at `0`
    have hτs : τstar σ ρ = 0 := by unfold τstar; rw [if_pos hcase]
    have hF : Fstar σ β ρ = β := by unfold Fstar; rw [if_pos hcase]
    rw [hτs, hF]
    have hmono : StrictMonoOn (fClosed σ β ρ) (Set.Icc 0 σ) := by
      apply strictMonoOn_of_deriv_pos (convex_Icc 0 σ) hcont
      intro τ hτ
      rw [interior_Icc] at hτ
      rw [hderiv τ hτ]
      apply dClosed_pos ρ (by linarith [hτ.2]) hτ.2
      rcases eq_or_lt_of_le hp1 with h | h
      · rw [← hp, h]; linarith [hτ.1]
      · nlinarith [hτ.1]
    refine ⟨⟨le_rfl, hσ0.le⟩, fClosed_zero σ β ρ, fun τ hτ hne => ?_⟩
    have := hmono ⟨le_rfl, hσ0.le⟩ hτ (lt_of_le_of_ne hτ.1 (Ne.symm hne))
    rwa [fClosed_zero] at this
  · -- the minimum is at the interior point `τ* = (σ - p)/(1 - p)`
    push Not at hcase
    have hp1' : p < 1 := hcase.trans hσ1
    set ts := (σ - p) / (1 - p) with hts
    have hτs : τstar σ ρ = ts := by unfold τstar; rw [if_neg (not_le.2 hcase)]
    have hF : Fstar σ β ρ = β - σ * ρ + H2 σ + (1 - σ) * logb 2 (1 - p) := by
      unfold Fstar; rw [if_neg (not_le.2 hcase)]
    have h1p : 0 < 1 - p := by linarith
    have hts0 : 0 < ts := div_pos (by linarith) h1p
    have htsσ : ts < σ := by rw [hts, div_lt_iff₀ h1p]; nlinarith
    -- sign of `dClosed` relative to `ts`
    have hkey : ∀ τ : ℝ, σ - τ - p * (1 - τ) = (1 - p) * (ts - τ) := by
      intro τ; rw [hts]; field_simp; ring
    have hmono : StrictMonoOn (fClosed σ β ρ) (Set.Icc ts σ) := by
      apply strictMonoOn_of_deriv_pos (convex_Icc ts σ) (hcont.mono (Set.Icc_subset_Icc_left hts0.le))
      intro τ hτ
      rw [interior_Icc] at hτ
      rw [hderiv τ ⟨hts0.trans hτ.1, hτ.2⟩]
      apply dClosed_pos ρ (by linarith [hτ.2]) hτ.2
      have := hkey τ
      nlinarith [hτ.1]
    have hanti : StrictAntiOn (fClosed σ β ρ) (Set.Icc 0 ts) := by
      apply strictAntiOn_of_deriv_neg (convex_Icc 0 ts) (hcont.mono (Set.Icc_subset_Icc_right htsσ.le))
      intro τ hτ
      rw [interior_Icc] at hτ
      rw [hderiv τ ⟨hτ.1, hτ.2.trans htsσ⟩]
      apply dClosed_neg ρ (by linarith [hτ.2]) hτ.1.le (hτ.2.trans htsσ)
      have := hkey τ
      nlinarith [hτ.2]
    -- the value at `ts`
    have hval : fClosed σ β ρ ts = β - σ * ρ + H2 σ + (1 - σ) * logb 2 (1 - p) := by
      set a := (1 - σ) / (1 - p) with ha
      have ha0 : 0 < a := div_pos (by linarith) h1p
      have e1 : 1 - ts = a := by rw [hts, ha]; field_simp; ring
      have e2 : σ - ts = p * a := by rw [hts, ha]; field_simp; ring
      have e3 : ts = σ - p * a := by linarith
      have hlogp : log p = -ρ * log 2 := by rw [hp, log_rpow (by norm_num)]
      have hloga : log a = log (1 - σ) - log (1 - p) := log_div (by linarith) h1p.ne'
      have hl : 0 < log 2 := log_pos (by norm_num)
      unfold fClosed H2 logb
      rw [e1, e2, binEntropy_eq_negMulLog_add_negMulLog_one_sub]
      unfold negMulLog
      rw [log_mul hp0.ne' ha0.ne', hlogp, hloga, e3]
      field_simp
      have : (1 - p) * a = 1 - σ := by rw [ha]; field_simp
      linear_combination (-(log (1 - σ)) + log (1 - p)) * this
    rw [hτs, hF]
    refine ⟨⟨hts0.le, htsσ.le⟩, hval, fun τ hτ hne => ?_⟩
    rw [← hval]
    rcases lt_or_gt_of_ne hne with h | h
    · exact hanti ⟨hτ.1, h.le⟩ ⟨hts0.le, le_rfl⟩ h
    · exact hmono ⟨le_rfl, htsσ.le⟩ ⟨h.le, hτ.2⟩ h

end OneSize

/-! ### 7. `rem:co-fsigma`, and part (2) of `cor:co-linear` -/

theorem one_sample_size (σ β ρ : ℝ) (hσ : σ ∈ Set.Ioo 0 1) (hβ : 0 ≤ β) (hρ : 0 ≤ ρ) :
    StrictConvexOn ℝ (Set.Icc 0 σ) (fσ σ β ρ) ∧
    τstar σ ρ ∈ Set.Icc 0 σ ∧
    (∀ τ ∈ Set.Icc 0 σ, fσ σ β ρ τ = Fstar σ β ρ ↔ τ = τstar σ ρ) ∧
    (∀ τ ∈ Set.Icc 0 σ, Fstar σ β ρ ≤ fσ σ β ρ τ) ∧
    (Fstar σ β ρ < β ↔ Real.logb 2 (1 / σ) < ρ) := by
  obtain ⟨hmem, hval, hmin⟩ := onesize_core σ β ρ hσ hρ
  obtain ⟨hσ0, hσ1⟩ := hσ
  rw [fσ_eq_closed hσ0.ne' β ρ]
  refine ⟨?_, hmem, ?_, ?_, ?_⟩
  · -- strict convexity: the derivative is strictly increasing on `(0, σ)`
    apply StrictMonoOn.strictConvexOn_of_deriv (convex_Icc 0 σ)
      (continuous_fClosed σ β ρ).continuousOn
    rw [interior_Icc]
    intro a ha b hb hab
    rw [(hasDerivAt_fClosed β ρ (by linarith [ha.2]) ha.2).deriv,
      (hasDerivAt_fClosed β ρ (by linarith [hb.2]) hb.2).deriv]
    unfold dClosed
    have hl : 0 < Real.log 2 := Real.log_pos (by norm_num)
    rw [sub_lt_sub_iff_right, div_lt_div_iff_of_pos_right hl,
      ← Real.log_div (by linarith [ha.2]) (by linarith [ha.2]),
      ← Real.log_div (by linarith [hb.2]) (by linarith [hb.2])]
    apply Real.log_lt_log (div_pos (by linarith [ha.2]) (by linarith [ha.2]))
    rw [div_lt_div_iff₀ (by linarith [ha.2]) (by linarith [hb.2])]
    nlinarith [ha.1, hb.2]
  · intro τ hτ
    constructor
    · intro h
      by_contra hne
      exact (hmin τ hτ hne).ne' h
    · rintro rfl; exact hval
  · intro τ hτ
    by_cases hne : τ = τstar σ ρ
    · rw [hne, hval]
    · exact (hmin τ hτ hne).le
  · have hiff : Real.logb 2 (1 / σ) < ρ ↔ (2:ℝ) ^ (-ρ) < σ := by
      rw [one_div, Real.logb_inv, neg_lt, Real.lt_logb_iff_rpow_lt (by norm_num) hσ0]
    rw [hiff]
    constructor
    · intro h
      by_contra hle
      push Not at hle
      have : Fstar σ β ρ = β := by unfold Fstar; rw [if_pos hle]
      linarith
    · intro h
      have h0 : (0:ℝ) ≠ τstar σ ρ := by
        unfold τstar
        rw [if_neg (not_le.2 h)]
        have : 2 ^ (-ρ) < (1:ℝ) := h.trans hσ1
        exact (div_pos (by linarith) (by linarith)).ne
      have := hmin 0 ⟨le_rfl, hσ0.le⟩ h0
      rwa [fClosed_zero] at this


/-! ### 8. `cor:co-linear` (1), the inequality -/

theorem linear_savings_W (g : Finset U → ℕ → ℝ) (S : Finset U) (k : ℕ) (hSk : S.card = k)
    (σ β ρ C : ℝ) (hσ : σ = k / Fintype.card U) (hσ01 : σ ∈ Set.Ioo 0 1)
    (hβ : 0 ≤ β) (hρ : 0 ≤ ρ) (hC : 0 ≤ C)
    (hlin : ∀ t ≤ k, (∑ X ∈ S.powersetCard t, g X (k - t)) / k.choose t
                        ≤ β * Fintype.card U - ρ * t + C) :
    let y := if σ ≤ 2 ^ (-ρ) then 0 else (σ * 2 ^ ρ - 1) / (2 ^ ρ * (1 - σ))
    (1 + y) ^ Fintype.card U / W g S k y ≤ 2 ^ (C + Fintype.card U * Fstar σ β ρ) := by
  intro y
  set n := Fintype.card U with hn
  obtain ⟨hσ0, hσ1⟩ := hσ01
  have hn0 : (0:ℝ) < n := by
    rcases Nat.eq_zero_or_pos n with h | h
    · rw [hσ, h, Nat.cast_zero, div_zero] at hσ0; exact absurd hσ0 (lt_irrefl 0)
    · exact_mod_cast h
  have hkσ : (k : ℝ) = σ * n := by rw [hσ]; field_simp
  set u : ℝ := (2:ℝ) ^ ρ with hu
  have hu0 : 0 < u := by positivity
  have hpu : (2:ℝ) ^ (-ρ) = u⁻¹ := by rw [hu, Real.rpow_neg (by norm_num)]
  have hy0 : 0 ≤ y := by
    change 0 ≤ if σ ≤ 2 ^ (-ρ) then 0 else (σ * 2 ^ ρ - 1) / (2 ^ ρ * (1 - σ))
    split_ifs with h
    · exact le_rfl
    · push Not at h
      rw [hpu, inv_lt_iff_one_lt_mul₀' hu0] at h
      rw [← hu]
      apply div_nonneg (by linarith) (mul_nonneg hu0.le (by linarith))
  -- lower bound on `W` from Jensen and the binomial theorem
  set c : ℝ := (2:ℝ) ^ (-(β * n + C)) with hc
  have hWlow : c * (1 + u * y) ^ k ≤ W g S k y := by
    rw [W_eq_sum_mu g S k hSk, add_comm 1 (u * y), add_pow, mul_sum]
    apply sum_le_sum
    intro t ht
    have htk : t ≤ k := Nat.lt_succ_iff.1 (mem_range.1 ht)
    have hmu := mu_ge_of_mean g S k t hSk htk _ (hlin t htk)
    have h2 : (2:ℝ) ^ (-(β * n - ρ * t + C)) = c * u ^ t := by
      rw [hc, hu, ← Real.rpow_mul_natCast (by norm_num),
        ← Real.rpow_add (by norm_num)]
      ring_nf
    rw [h2] at hmu
    calc c * ((u * y) ^ t * 1 ^ (k - t) * k.choose t)
        = y ^ t * (k.choose t * (c * u ^ t)) := by ring
      _ ≤ y ^ t * mu g S k t := mul_le_mul_of_nonneg_left hmu (pow_nonneg hy0 t)
  have hc0 : 0 < c := by positivity
  have hB0 : 0 < (1 + u * y) ^ k := by positivity
  have hW0 : 0 < W g S k y := lt_of_lt_of_le (mul_pos hc0 hB0) hWlow
  -- reduce to the exponent `E(y)`
  have hred : (1 + y) ^ n / (1 + u * y) ^ k ≤ (2:ℝ) ^ (n * (Fstar σ β ρ - β)) →
      (1 + y) ^ n / W g S k y ≤ 2 ^ (C + n * Fstar σ β ρ) := by
    intro hE
    calc (1 + y) ^ n / W g S k y ≤ (1 + y) ^ n / (c * (1 + u * y) ^ k) :=
          div_le_div_of_nonneg_left (by positivity) (mul_pos hc0 hB0) hWlow
      _ = c⁻¹ * ((1 + y) ^ n / (1 + u * y) ^ k) := by field_simp
      _ ≤ c⁻¹ * (2:ℝ) ^ (n * (Fstar σ β ρ - β)) := by gcongr
      _ = 2 ^ (C + n * Fstar σ β ρ) := by
          rw [hc, ← Real.rpow_neg (by norm_num), ← Real.rpow_add (by norm_num)]
          ring_nf
  apply hred
  by_cases hcase : σ ≤ 2 ^ (-ρ)
  · have hy : y = 0 := if_pos hcase
    have hF : Fstar σ β ρ = β := if_pos hcase
    rw [hy, hF]
    simp
  · have hy : y = (σ * u - 1) / (u * (1 - σ)) := if_neg hcase
    have hF : Fstar σ β ρ = β - σ * ρ + H2 σ + (1 - σ) * Real.logb 2 (1 - 2 ^ (-ρ)) :=
      if_neg hcase
    push Not at hcase
    rw [hpu] at hcase hF
    have hσu : 1 < σ * u := by rwa [inv_lt_iff_one_lt_mul₀' hu0, mul_comm] at hcase
    have hu1 : 1 < u := by nlinarith
    have h1σ : 0 < 1 - σ := by linarith
    have hA : 1 + y = (u - 1) / (u * (1 - σ)) := by rw [hy]; field_simp; ring
    have hB : 1 + u * y = σ * (u - 1) / (1 - σ) := by rw [hy]; field_simp; ring
    have hA0 : 0 < (u - 1) / (u * (1 - σ)) := div_pos (by linarith) (by positivity)
    have hB0' : 0 < σ * (u - 1) / (1 - σ) := div_pos (by nlinarith) h1σ
    rw [hA, hB]
    apply le_of_eq
    have hpos : 0 < ((u - 1) / (u * (1 - σ))) ^ n / (σ * (u - 1) / (1 - σ)) ^ k :=
      div_pos (pow_pos hA0 n) (pow_pos hB0' k)
    rw [← Real.rpow_logb (b := 2) (by norm_num) (by norm_num) hpos]
    congr 1
    have hl : 0 < Real.log 2 := Real.log_pos (by norm_num)
    have hlogu : Real.log u = ρ * Real.log 2 := by rw [hu, Real.log_rpow (by norm_num)]
    have hu1' : u - 1 = u * (1 - u⁻¹) := by field_simp
    have hlogu1 : Real.log (u - 1) = Real.log u + Real.log (1 - u⁻¹) := by
      rw [hu1', Real.log_mul hu0.ne' (by
        have : u⁻¹ < 1 := inv_lt_one_of_one_lt₀ hu1
        linarith)]
    rw [hF]
    unfold Real.logb H2
    rw [Real.log_div (pow_pos hA0 n).ne' (pow_pos hB0' k).ne', Real.log_pow, Real.log_pow,
      Real.log_div (by linarith) (by positivity), Real.log_mul hu0.ne' h1σ.ne',
      Real.log_div (by nlinarith) h1σ.ne', Real.log_mul hσ0.ne' (by linarith), hkσ,
      Real.binEntropy_eq_negMulLog_add_negMulLog_one_sub, Real.negMulLog, Real.negMulLog,
      hlogu1, hlogu]
    field_simp
    ring

end MaxLeafFormal.MLS