MaxLeafFormal.CCT

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

Statements of the paper formalised here: Corollary 11.5.

import MaxLeafFormal.MLS
import MaxLeafFormal.CCRate
import MaxLeafFormal.CCGibbs

/-!
# `cor:cc-T`(a): the generating function of a component-count running time

The paper's `def:cc-bound` and part (a) of `cor:cc-T`, with its proof.

`W_ge_Z` is step 1 (no tree needed, `y ≥ 0`), `cc_T_a_of_gibbs` is part (a) with the Gibbs
inequality as a hypothesis, and `cc_T_a` is part (a) as stated, using `CCGibbs.cc_gibbs`.
-/

namespace MaxLeafFormal.CCT

open Finset

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

/-- `eq:cc-bound` for the solution `S` of size `k`, the tree `F` on `S` and constants `c, γ`. -/
def CCBoundOn (g : Finset U → ℕ → ℝ) (S : Finset U) (k : ℕ) (c γ : ℝ) (F : SimpleGraph S) : Prop :=
  ∀ X ⊆ S, g X (k - X.card) ≤
    ((k : ℝ) - X.card) * Real.logb 2 c + X.card - (CCGibbs.eIn F (X.subtype (· ∈ S)) : ℝ) + γ

/-- `def:cc-bound` for one fixed instance: every solution of size at least 1 has a tree. -/
def HasCCBound (sol : Finset U → Prop) (g : Finset U → ℕ → ℝ) (c γ : ℝ) : Prop :=
  1 ≤ c ∧ 0 ≤ γ ∧
    ∀ S : Finset U, sol S → 1 ≤ S.card → ∃ F : SimpleGraph S, F.IsTree ∧ CCBoundOn g S S.card c γ F

/-! ### Real-number helpers -/

/-- `λ_max(M_ζ) ≥ 1` for `ζ ≥ 0`. -/
theorem one_le_spr {ζ : ℝ} (hζ : 0 ≤ ζ) : 1 ≤ CCRate.spr ζ := by
  unfold CCRate.spr
  have h : 1 ≤ Real.sqrt (1 + 4 * ζ ^ 2) := by
    calc (1:ℝ) = Real.sqrt 1 := Real.sqrt_one.symm
      _ ≤ Real.sqrt (1 + 4 * ζ ^ 2) := Real.sqrt_le_sqrt (by nlinarith)
  linarith

/-- `2^{m log₂ c} = c^m` for `c > 0`. -/
theorem rpow_logb_mul_nat {c : ℝ} (hc : 0 < c) (m : ℕ) :
    (2:ℝ) ^ ((m : ℝ) * Real.logb 2 c) = c ^ m := by
  rw [mul_comm, Real.rpow_mul (by norm_num : (0:ℝ) ≤ 2),
    Real.rpow_logb (by norm_num) (by norm_num) hc, Real.rpow_natCast]

/-- The termwise bound of step 1. -/
theorem termwise {c γ y gx : ℝ} (hc : 0 < c) (hy : 0 ≤ y) {k x e : ℕ} (hxk : x ≤ k)
    (hb : gx ≤ ((k : ℝ) - x) * Real.logb 2 c + x - (e : ℝ) + γ) :
    (2:ℝ) ^ (-γ) * (c ^ k)⁻¹ * ((c * y / 2) ^ x * (2:ℝ) ^ e) ≤ y ^ x * (2:ℝ) ^ (-gx) := by
  set E := ((k : ℝ) - x) * Real.logb 2 c + x - (e : ℝ) + γ with hE
  have hmono : (2:ℝ) ^ (-E) ≤ (2:ℝ) ^ (-gx) :=
    Real.rpow_le_rpow_of_exponent_le (by norm_num) (by linarith)
  have hkey : (2:ℝ) ^ (-E) * (c ^ (k - x) * 2 ^ x) = (2:ℝ) ^ (-γ) * 2 ^ e := by
    rw [← rpow_logb_mul_nat hc, ← Real.rpow_natCast (2:ℝ) x, ← Real.rpow_natCast (2:ℝ) e]
    simp only [← Real.rpow_add (by norm_num : (0:ℝ) < 2)]
    congr 1
    rw [hE, Nat.cast_sub hxk]
    ring
  have hD : c ^ (k - x) * (2:ℝ) ^ x ≠ 0 := by positivity
  have h2E : (2:ℝ) ^ (-E) = (2:ℝ) ^ (-γ) * 2 ^ e / (c ^ (k - x) * 2 ^ x) := by
    rw [eq_div_iff hD]; exact hkey
  have hc0 : c ≠ 0 := hc.ne'
  calc (2:ℝ) ^ (-γ) * (c ^ k)⁻¹ * ((c * y / 2) ^ x * (2:ℝ) ^ e)
      = y ^ x * (2:ℝ) ^ (-E) := by
        rw [h2E, ← pow_sub_mul_pow c hxk, div_pow, mul_pow]
        field_simp
    _ ≤ y ^ x * (2:ℝ) ^ (-gx) := mul_le_mul_of_nonneg_left hmono (pow_nonneg hy _)

omit [Fintype U] in

/-- `𝒵_F(ζ)` as a sum over the subsets of `S`. -/
theorem Zpart_eq_sum_powerset (S : Finset U) (F : SimpleGraph S) (ζ : ℝ) :
    CCGibbs.Zpart F ζ =
      ∑ X ∈ S.powerset, ζ ^ X.card * (2:ℝ) ^ CCGibbs.eIn F (X.subtype (· ∈ S)) := by
  unfold CCGibbs.Zpart
  refine Finset.sum_nbij' (fun X' => X'.map (Function.Embedding.subtype (· ∈ S)))
    (fun X => X.subtype (· ∈ S)) ?_ ?_ ?_ ?_ ?_
  · intro X' _
    rw [Finset.mem_powerset]
    intro a ha
    rw [Finset.mem_map] at ha
    obtain ⟨b, _, rfl⟩ := ha
    exact b.2
  · intro X _
    exact Finset.mem_powerset.mpr (Finset.subset_univ _)
  · intro X' _
    ext b
    simp
  · intro X hX
    exact Finset.subtype_map_of_mem (fun x hx => Finset.mem_powerset.mp hX hx)
  · intro X' _
    have h : (X'.map (Function.Embedding.subtype (· ∈ S))).subtype (· ∈ S) = X' := by
      ext b
      simp
    rw [h, Finset.card_map]

/-! ### Step 1 -/

/-- Step 1 (first inequality of `cor:cc-T`(a)). No tree hypothesis; `y ≥ 0` suffices. -/
theorem W_ge_Z (g : Finset U → ℕ → ℝ) (S : Finset U) (k : ℕ) (hSk : S.card = k)
    (c γ : ℝ) (hc : 1 ≤ c) (F : SimpleGraph S) (hbound : CCBoundOn g S k c γ F)
    (y : ℝ) (hy : 0 ≤ y) :
    (2:ℝ) ^ (-γ) * (c ^ k)⁻¹ * CCGibbs.Zpart F (c * y / 2) ≤ MLS.W g S k y := by
  rw [Zpart_eq_sum_powerset, Finset.mul_sum]
  unfold MLS.W
  refine Finset.sum_le_sum fun X hX => ?_
  have hXS : X ⊆ S := Finset.mem_powerset.mp hX
  have hxk : X.card ≤ k := hSk ▸ Finset.card_le_card hXS
  exact termwise (by linarith) hy hxk (hbound X hXS)

/-! ### Step 2 -/

/-- The rescaled Gibbs inequality, graph-free. -/
theorem gibbs_rescale {c l m Z : ℝ} (hc : 0 < c) (hl : 0 < l) {k : ℕ} (hk : 1 ≤ k)
    (h : m * l ^ (k - 1) ≤ Z) : m / l * (l / c) ^ k ≤ (c ^ k)⁻¹ * Z := by
  have heq : m / l * (l / c) ^ k = (c ^ k)⁻¹ * (m * l ^ (k - 1)) := by
    obtain ⟨j, rfl⟩ : ∃ j, k = j + 1 := ⟨k - 1, by omega⟩
    rw [Nat.add_sub_cancel, div_pow, pow_succ]
    field_simp
  rw [heq]
  exact mul_le_mul_of_nonneg_left h (inv_nonneg.mpr (pow_nonneg hc.le _))

/-! ### Part (a) -/

/-- `cor:cc-T`(a), with `lem:cc-gibbs` for this `F` and `ζ = cy/2` as the hypothesis `hG`. -/
theorem cc_T_a_of_gibbs (g : Finset U → ℕ → ℝ) (S : Finset U) (k : ℕ) (hSk : S.card = k)
    (hk : 1 ≤ k) (c γ : ℝ) (hc : 1 ≤ c) (F : SimpleGraph S) (hbound : CCBoundOn g S k c γ F)
    (y : ℝ) (hy : 0 < y)
    (hG : min 1 (c * y / 2) * CCRate.spr (c * y / 2) ^ (k - 1) ≤ CCGibbs.Zpart F (c * y / 2)) :
    (2:ℝ) ^ (-γ) * (c ^ k)⁻¹ * CCGibbs.Zpart F (c * y / 2) ≤ MLS.W g S k y ∧
    (2:ℝ) ^ (-γ) * (min 1 (c * y / 2) / CCRate.spr (c * y / 2)) * (CCRate.spr (c * y / 2) / c) ^ k
      ≤ (2:ℝ) ^ (-γ) * (c ^ k)⁻¹ * CCGibbs.Zpart F (c * y / 2) ∧
    (1 + y) ^ Fintype.card U / MLS.W g S k y
      ≤ (2:ℝ) ^ γ * (CCRate.spr (c * y / 2) / min 1 (c * y / 2)) *
          (2:ℝ) ^ ((Fintype.card U : ℝ) * CCRate.phi c ((k : ℝ) / Fintype.card U) y) := by
  have hc0 : 0 < c := by linarith
  have hζ : 0 < c * y / 2 := by positivity
  have hl1 : 1 ≤ CCRate.spr (c * y / 2) := one_le_spr hζ.le
  have hl : 0 < CCRate.spr (c * y / 2) := by linarith
  have hm : 0 < min 1 (c * y / 2) := lt_min one_pos hζ
  have h2γ : (0:ℝ) < (2:ℝ) ^ (-γ) := Real.rpow_pos_of_pos (by norm_num) _
  have hA := W_ge_Z g S k hSk c γ hc F hbound y hy.le
  have hB : (2:ℝ) ^ (-γ) * (min 1 (c * y / 2) / CCRate.spr (c * y / 2)) *
      (CCRate.spr (c * y / 2) / c) ^ k
      ≤ (2:ℝ) ^ (-γ) * (c ^ k)⁻¹ * CCGibbs.Zpart F (c * y / 2) := by
    have h := gibbs_rescale hc0 hl hk hG
    calc (2:ℝ) ^ (-γ) * (min 1 (c * y / 2) / CCRate.spr (c * y / 2)) *
          (CCRate.spr (c * y / 2) / c) ^ k
        = (2:ℝ) ^ (-γ) * (min 1 (c * y / 2) / CCRate.spr (c * y / 2) *
          (CCRate.spr (c * y / 2) / c) ^ k) := by ring
      _ ≤ (2:ℝ) ^ (-γ) * ((c ^ k)⁻¹ * CCGibbs.Zpart F (c * y / 2)) :=
          mul_le_mul_of_nonneg_left h h2γ.le
      _ = (2:ℝ) ^ (-γ) * (c ^ k)⁻¹ * CCGibbs.Zpart F (c * y / 2) := by ring
  refine ⟨hA, hB, ?_⟩
  -- Step 3.
  have hkn : k ≤ Fintype.card U := hSk ▸ Finset.card_le_univ S
  have hn : (Fintype.card U : ℝ) ≠ 0 := by
    have : 0 < Fintype.card U := by omega
    positivity
  have hR : 0 < (2:ℝ) ^ (-γ) * (min 1 (c * y / 2) / CCRate.spr (c * y / 2)) *
      (CCRate.spr (c * y / 2) / c) ^ k := by positivity
  have hRW := le_trans hB hA
  have h1y : (0:ℝ) < 1 + y := by linarith
  have hlc : 0 < CCRate.spr (c * y / 2) / c := div_pos hl hc0
  have hnk : (Fintype.card U : ℝ) * ((k : ℝ) / Fintype.card U) = k := by field_simp
  have hphi : (2:ℝ) ^ ((Fintype.card U : ℝ) * CCRate.phi c ((k : ℝ) / Fintype.card U) y)
      = (1 + y) ^ Fintype.card U / (CCRate.spr (c * y / 2) / c) ^ k := by
    unfold CCRate.phi
    rw [mul_sub, ← mul_assoc, hnk, Real.rpow_sub (by norm_num : (0:ℝ) < 2),
      rpow_logb_mul_nat h1y, rpow_logb_mul_nat hlc]
  calc (1 + y) ^ Fintype.card U / MLS.W g S k y
      ≤ (1 + y) ^ Fintype.card U / ((2:ℝ) ^ (-γ) * (min 1 (c * y / 2) / CCRate.spr (c * y / 2)) *
          (CCRate.spr (c * y / 2) / c) ^ k) :=
        div_le_div_of_nonneg_left (by positivity) hR hRW
    _ = (2:ℝ) ^ γ * (CCRate.spr (c * y / 2) / min 1 (c * y / 2)) *
          (2:ℝ) ^ ((Fintype.card U : ℝ) * CCRate.phi c ((k : ℝ) / Fintype.card U) y) := by
        rw [hphi, Real.rpow_neg (by norm_num : (0:ℝ) ≤ 2)]
        have h2 : (0:ℝ) < (2:ℝ) ^ γ := Real.rpow_pos_of_pos (by norm_num) _
        field_simp

/-- `cor:cc-T`(a) as stated. It uses `CCGibbs.cc_gibbs`.
`1 ≤ k` is not a binder: it follows from `hF` and `hSk`. -/
theorem cc_T_a (g : Finset U → ℕ → ℝ) (S : Finset U) (k : ℕ) (hSk : S.card = k)
    (c γ : ℝ) (hc : 1 ≤ c) (F : SimpleGraph S) (hF : F.IsTree)
    (hbound : CCBoundOn g S k c γ F) (y : ℝ) (hy : 0 < y) :
    (2:ℝ) ^ (-γ) * (c ^ k)⁻¹ * CCGibbs.Zpart F (c * y / 2) ≤ MLS.W g S k y ∧
    (2:ℝ) ^ (-γ) * (min 1 (c * y / 2) / CCRate.spr (c * y / 2)) * (CCRate.spr (c * y / 2) / c) ^ k
      ≤ (2:ℝ) ^ (-γ) * (c ^ k)⁻¹ * CCGibbs.Zpart F (c * y / 2) ∧
    (1 + y) ^ Fintype.card U / MLS.W g S k y
      ≤ (2:ℝ) ^ γ * (CCRate.spr (c * y / 2) / min 1 (c * y / 2)) *
          (2:ℝ) ^ ((Fintype.card U : ℝ) * CCRate.phi c ((k : ℝ) / Fintype.card U) y) := by
  have hk : 1 ≤ k := by
    obtain ⟨⟨x, hx⟩⟩ := hF.1.nonempty
    rw [← hSk]
    exact Finset.card_pos.mpr ⟨x, hx⟩
  have hζ : 0 < c * y / 2 := by
    have : 0 < c := by linarith
    positivity
  have hG := CCGibbs.cc_gibbs F hF (c * y / 2) hζ
  rw [Fintype.card_coe, hSk] at hG
  exact cc_T_a_of_gibbs g S k hSk hk c γ hc F hbound y hy hG

/-- Optional (stage 2): the form "let `g` have a component-count bound". -/
theorem cc_T_a_of_hasCCBound (sol : Finset U → Prop) (g : Finset U → ℕ → ℝ) (c γ : ℝ)
    (hg : HasCCBound sol g c γ) (S : Finset U) (hS : sol S) (hk : 1 ≤ S.card) :
    ∃ F : SimpleGraph S, F.IsTree ∧ CCBoundOn g S S.card c γ F ∧
      ∀ y : ℝ, 0 < y →
        (2:ℝ) ^ (-γ) * (c ^ S.card)⁻¹ * CCGibbs.Zpart F (c * y / 2) ≤ MLS.W g S S.card y ∧
        (2:ℝ) ^ (-γ) * (min 1 (c * y / 2) / CCRate.spr (c * y / 2)) *
            (CCRate.spr (c * y / 2) / c) ^ S.card
          ≤ (2:ℝ) ^ (-γ) * (c ^ S.card)⁻¹ * CCGibbs.Zpart F (c * y / 2) ∧
        (1 + y) ^ Fintype.card U / MLS.W g S S.card y
          ≤ (2:ℝ) ^ γ * (CCRate.spr (c * y / 2) / min 1 (c * y / 2)) *
              (2:ℝ) ^ ((Fintype.card U : ℝ) *
                CCRate.phi c ((S.card : ℝ) / Fintype.card U) y) := by
  obtain ⟨hc, -, hS'⟩ := hg
  obtain ⟨F, hF, hb⟩ := hS' S hS hk
  exact ⟨F, hF, hb, fun y hy => cc_T_a g S S.card rfl c γ hc F hF hb y hy⟩

end MaxLeafFormal.CCT