MaxLeafFormal.RateAssembly

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

Statements of the paper formalised here: Corollary 6.2, Proposition 7.8, Theorem 6.4.

import MaxLeafFormal.RSRate
import MaxLeafFormal.RSThetaRate
import MaxLeafFormal.CDS

/-!
# Assemblies of the rates with `MLS` and `CDS`

`cor:rs-moments`, `prop:rst-rate` and the completeness inequality in the proof of `thm:rs`, for
the running-time exponent `g(X) = |Tm(J_X)|`. They combine the rates `RSThetaRate.rst_rates` and
(`RSRate.rs_rate_c`, `RSRate.rs_constants`) with the checked declarations `MLS.star_of_W`,
`MLS.linear_savings_W`, `CDS.mean_terminals` and `CDS.rstheta_moment_bound_{0,1}`.
-/

namespace MaxLeafFormal.RateAssembly

open CDS Finset

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

/-- The running-time exponent `g(X) = |Tm(J_X)|`, independent of the budget. -/
noncomputable def gT (G : SimpleGraph V) [DecidableRel G.Adj] : Finset V → ℕ → ℝ :=
  fun X _ => (termCount G X : ℝ)

/-! ### Helpers -/

omit [Fintype V] [DecidableEq V] in

/-- A connected dominating set is nonempty. -/
theorem card_pos_of_isCDS {G : SimpleGraph V} {S : Finset V} (hS : IsCDS G S) : 0 < S.card := by
  obtain ⟨⟨v, hv⟩⟩ := hS.1.nonempty
  exact Finset.card_pos.2 ⟨v, by exact_mod_cast hv⟩

omit [Fintype V] [DecidableEq V] in

/-- A connected dominating set has one component. -/
theorem comp_of_isCDS {G : SimpleGraph V} {S : Finset V} (hS : IsCDS G S) : comp G S = 1 := by
  unfold comp
  have : Subsingleton (G.induce (S : Set V)).ConnectedComponent :=
    hS.1.preconnected.subsingleton_connectedComponent
  have : Nonempty (G.induce (S : Set V)).ConnectedComponent := by
    obtain ⟨v⟩ := hS.1.nonempty
    exact ⟨(G.induce (S : Set V)).connectedComponentMk v⟩
  exact Nat.card_eq_one_iff_unique.2 ⟨inferInstance, inferInstance⟩

/-- `|Tm(J_S)| = 1` for a connected dominating set `S`. -/
theorem termCount_of_isCDS (G : SimpleGraph V) [DecidableRel G.Adj] {S : Finset V}
    (hS : IsCDS G S) : termCount G S = 1 := by
  have hN : closedNbhd G S = univ := by
    apply eq_univ_of_forall
    intro v
    rw [mem_closedNbhd]
    rcases hS.2 v with h | ⟨u, hu, huv⟩
    · exact Or.inl h
    · exact Or.inr ⟨u, hu, huv.symm⟩
  unfold termCount
  rw [hN, card_univ, comp_of_isCDS hS]
  simp

/-- `|Tm(J_∅)| = n`. -/
theorem termCount_empty (G : SimpleGraph V) [DecidableRel G.Adj] :
    termCount G ∅ = Fintype.card V := by
  have hN : closedNbhd G ∅ = ∅ := by simp [closedNbhd]
  have hc : comp G ∅ = 0 := by
    unfold comp
    apply Nat.card_eq_zero.2
    left
    refine ⟨fun c => ?_⟩
    induction c using SimpleGraph.ConnectedComponent.ind with
    | h v => exact absurd v.2 (by simp)
  unfold termCount
  rw [hN, hc]
  simp

omit [DecidableEq V] in

/-- (⋆) is monotone in `ω`. -/
theorem star_mono {g : Finset V → ℕ → ℝ} {S : Finset V} {k : ℕ} {ω ω' Γ : ℝ}
    (hΓ : 0 < Γ) (h : MLS.Star g S k ω Γ) (hωω' : ω ≤ ω') : MLS.Star g S k ω' Γ := by
  obtain ⟨t, ht, h⟩ := h
  refine ⟨t, ht, le_trans ?_ h⟩
  apply div_le_div_of_nonneg_right _ hΓ.le
  apply Real.rpow_le_rpow_of_exponent_le (by norm_num)
  have : (0:ℝ) ≤ Fintype.card V := Nat.cast_nonneg _
  nlinarith

/-- `W_S(y)` for `gT` is the sum bounded in `CDS.rstheta_moment_bound_{0,1}`. -/
theorem W_gT (G : SimpleGraph V) [DecidableRel G.Adj] (S : Finset V) (k : ℕ) (y : ℝ) :
    MLS.W (gT G) S k y = ∑ X ∈ S.powerset, y ^ X.card * (1/2 : ℝ) ^ termCount G X := by
  unfold MLS.W gT
  refine sum_congr rfl fun X _ => ?_
  rw [Real.rpow_neg (by norm_num), Real.rpow_natCast, one_div, inv_pow]

theorem W_gT_pos (G : SimpleGraph V) [DecidableRel G.Adj] (S : Finset V) (k : ℕ) {y : ℝ}
    (hy : 0 ≤ y) : 0 < MLS.W (gT G) S k y := by
  rw [W_gT]
  calc (0:ℝ) < y ^ (∅ : Finset V).card * (1/2 : ℝ) ^ termCount G ∅ := by simp
    _ ≤ _ := single_le_sum (f := fun X : Finset V => y ^ X.card * (1/2 : ℝ) ^ termCount G X)
        (fun X _ => by positivity) (empty_mem_powerset S)

/-- A certificate bound `c e₁^s e₂^{n-s} ≤ W_S(y)` with `c ≥ 1/2` gives (⋆) with `Γ = 2` at every
`ω` above `ω_cert(σ)`. -/
theorem star_of_cert (G : SimpleGraph V) [DecidableRel G.Adj] (S : Finset V)
    (c e₁ e₂ y ω : ℝ) (hc : 1/2 ≤ c) (he₁ : 0 < e₁) (he₂ : 0 < e₂) (hy : 0 ≤ y)
    (hn : 0 < Fintype.card V) (hsn : S.card ≤ Fintype.card V)
    (hmom : c * e₁ ^ S.card * e₂ ^ (Fintype.card V - S.card)
      ≤ ∑ X ∈ S.powerset, y ^ X.card * (1/2 : ℝ) ^ termCount G X)
    (hω : RSThetaRate.omegaCert y e₁ e₂ (S.card / Fintype.card V) ≤ ω) :
    MLS.Star (gT G) S S.card ω 2 := by
  set n := Fintype.card V with hn'
  set s := S.card with hs
  apply MLS.star_of_W (gT G) S s rfl ω 2 y (by norm_num) hy
  rw [W_gT]
  refine le_trans ?_ hmom
  have hn0 : (0:ℝ) < n := by exact_mod_cast hn
  have h1y : 0 < 1 + y := by linarith
  have hA : 0 < (1 + y) ^ n * (2:ℝ) ^ (-(ω * n)) := by positivity
  have hB : 0 < e₁ ^ s * e₂ ^ (n - s) := by positivity
  -- the core inequality, in base-2 logarithms
  have hcore : (1 + y) ^ n * (2:ℝ) ^ (-(ω * n)) ≤ e₁ ^ s * e₂ ^ (n - s) := by
    rw [← Real.logb_le_logb (b := 2) (by norm_num) hA hB, Real.logb_mul (by positivity) (by positivity),
      Real.logb_mul (by positivity) (by positivity), Real.logb_pow, Real.logb_pow, Real.logb_pow,
      Real.logb_rpow (by norm_num) (by norm_num), Nat.cast_sub hsn]
    unfold RSThetaRate.omegaCert at hω
    have hσn : ((s : ℝ) / n) * n = s := by field_simp
    have key : (Real.logb 2 (1 + y) - (s / n : ℝ) * Real.logb 2 e₁
        - (1 - (s / n : ℝ)) * Real.logb 2 e₂) * n
        = n * Real.logb 2 (1 + y) - s * Real.logb 2 e₁ - (n - s) * Real.logb 2 e₂ := by
      field_simp
    have := mul_le_mul_of_nonneg_right hω hn0.le
    rw [key] at this
    linarith
  calc (1 + y) ^ n * (2:ℝ) ^ (-(ω * n)) / 2 ≤ c * ((1 + y) ^ n * (2:ℝ) ^ (-(ω * n))) := by
        rw [div_le_iff₀ (by norm_num)]; nlinarith
    _ ≤ c * (e₁ ^ s * e₂ ^ (n - s)) := mul_le_mul_of_nonneg_left hcore (by linarith)
    _ = c * e₁ ^ s * e₂ ^ (n - s) := by ring

/-! ### `cor:rs-moments` -/

/-- cor:rs-moments. -/
theorem rs_moments (G : SimpleGraph V) [DecidableRel G.Adj] (hG : G.Connected)
    (S : Finset V) (hS : IsCDS G S) :
    MLS.Star (gT G) S S.card (RSRate.rsF (S.card / Fintype.card V)) 2 := by
  set n := Fintype.card V with hn'
  set s := S.card with hs
  have hs0 : 0 < s := card_pos_of_isCDS hS
  have hsn : s ≤ n := card_le_univ S
  rcases hsn.lt_or_eq with hlt | heq
  · -- `0 < σ < 1`: `cor:co-linear` with `β = 1`, `ρ = 1/σ`, `C = 1`
    have hn2 : 2 ≤ n := by omega
    have hn0 : (0:ℝ) < n := by exact_mod_cast (show 0 < n by omega)
    have hs0' : (0:ℝ) < s := by exact_mod_cast hs0
    set σ : ℝ := (s : ℝ) / n with hσ
    have hσ0 : 0 < σ := div_pos hs0' hn0
    have hσ1 : σ < 1 := by rw [hσ, div_lt_one hn0]; exact_mod_cast hlt
    have hlin : ∀ t ≤ s, (∑ X ∈ S.powersetCard t, gT G X (s - t)) / s.choose t
        ≤ 1 * (n : ℝ) - σ⁻¹ * t + 1 := by
      intro t hts
      have hinv : σ⁻¹ * t = t * n / s := by rw [hσ]; field_simp
      rw [hinv]
      rcases Nat.eq_zero_or_pos t with rfl | ht1
      · simp [gT, termCount_empty]
        rw [← hn']
        linarith
      · have hm := (mean_terminals G hG hn2 S hS t ht1 hts).2
        have hts' : (t : ℝ) ≤ s := by exact_mod_cast hts
        have h2 : (t : ℝ) * (n - 2) / s = t * n / s - 2 * t / s := by field_simp
        have h3 : 2 * (t : ℝ) / s ≤ 2 := by
          rw [div_le_iff₀ hs0']; linarith
        unfold gT
        rw [h2] at hm
        linarith
    have hL := MLS.linear_savings_W (gT G) S s rfl σ 1 σ⁻¹ 1 hσ ⟨hσ0, hσ1⟩ (by norm_num)
      (inv_nonneg.2 hσ0.le) (by norm_num) hlin
    set y : ℝ := if σ ≤ 2 ^ (-σ⁻¹) then 0 else (σ * 2 ^ σ⁻¹ - 1) / (2 ^ σ⁻¹ * (1 - σ)) with hy
    have hL' : (1 + y) ^ n / MLS.W (gT G) S s y ≤ 2 ^ (1 + n * MLS.Fstar σ 1 σ⁻¹) := hL
    have hy0 : 0 ≤ y := by
      rw [hy]
      split_ifs with h
      · exact le_rfl
      · push Not at h
        have hu0 : (0:ℝ) < 2 ^ σ⁻¹ := by positivity
        rw [Real.rpow_neg (by norm_num), inv_lt_iff_one_lt_mul₀' hu0] at h
        exact div_nonneg (by linarith) (mul_nonneg hu0.le (by linarith))
    rw [← RSRate.rsF_eq_Fstar ⟨hσ0, hσ1⟩] at hL'
    have hW := W_gT_pos G S s hy0
    apply MLS.star_of_W (gT G) S s rfl _ 2 y (by norm_num) hy0
    rw [div_le_iff₀ hW] at hL'
    have hsplit : (2:ℝ) ^ (1 + n * RSRate.rsF σ)
        = 2 * (2:ℝ) ^ (RSRate.rsF σ * n) := by
      rw [Real.rpow_add (by norm_num), Real.rpow_one, mul_comm (n:ℝ)]
    have hinv : (2:ℝ) ^ (-(RSRate.rsF σ * n)) * (2:ℝ) ^ (RSRate.rsF σ * n) = 1 := by
      rw [← Real.rpow_add (by norm_num)]; simp
    have hp : 0 < (2:ℝ) ^ (-(RSRate.rsF σ * n)) := by positivity
    rw [hsplit] at hL'
    calc (1 + y) ^ n * (2:ℝ) ^ (-(RSRate.rsF σ * n)) / 2
        ≤ (2 * (2:ℝ) ^ (RSRate.rsF σ * n) * MLS.W (gT G) S s y)
            * (2:ℝ) ^ (-(RSRate.rsF σ * n)) / 2 := by gcongr
      _ = MLS.W (gT G) S s y * ((2:ℝ) ^ (-(RSRate.rsF σ * n)) * (2:ℝ) ^ (RSRate.rsF σ * n)) := by
          ring
      _ = MLS.W (gT G) S s y := by rw [hinv, mul_one]
  · -- `s = n`: `S = V`, `t = n`, `μ_n(S) = 2^{-|Tm(J_V)|} = 1/2` and `F*(1) = 0`
    have hn0 : (0:ℝ) < n := by exact_mod_cast (show 0 < n by omega)
    have hσ : ((s : ℝ) / n) = 1 := by rw [heq]; exact div_self hn0.ne'
    rw [hσ, RSRate.rsF_one]
    refine ⟨s, le_rfl, ?_⟩
    unfold MLS.mu gT
    rw [hs, powersetCard_self, sum_singleton, termCount_of_isCDS G hS, ← hs, heq, Nat.choose_self]
    norm_num

/-! ### `prop:rst-rate` -/

/-- prop:rst-rate. -/
theorem rst_rate (G : SimpleGraph V) [DecidableRel G.Adj] (hG : G.Connected)
    (S : Finset V) (hS : IsCDS G S) :
    MLS.Star (gT G) S S.card (7827016/10^7) 2 := by
  have hs0 := card_pos_of_isCDS hS
  have hsn : S.card ≤ Fintype.card V := card_le_univ S
  have hn : 0 < Fintype.card V := lt_of_lt_of_le hs0 hsn
  have hn0 : (0:ℝ) < Fintype.card V := by exact_mod_cast hn
  have hs0' : (0:ℝ) < S.card := by exact_mod_cast hs0
  set σ : ℝ := (S.card : ℝ) / Fintype.card V with hσ
  have hσ0 : 0 < σ := div_pos hs0' hn0
  have hσ1 : σ ≤ 1 := by rw [hσ, div_le_one hn0]; exact_mod_cast hsn
  obtain ⟨-, hR2, hR3⟩ := RSRate.rs_rate_c
  obtain ⟨hw0, hw1, -, -, -, -, -⟩ := RSThetaRate.rst_rates
  have hm := rs_moments G hG S hS
  by_cases hlo : σ ≤ 31/100
  · exact star_mono (by norm_num) hm ((hR2 σ ⟨hσ0, hlo⟩).trans (by norm_num))
  by_cases hhi : 54/100 ≤ σ
  · exact star_mono (by norm_num) hm ((hR3 σ ⟨hhi, hσ1⟩).trans (by norm_num))
  push Not at hlo hhi
  have hq : ∀ a b : ℕ, ((RSThetaCert.q a b : ℚ) : ℝ) = (a : ℝ) / b := fun a b => by
    unfold RSThetaCert.q; push_cast; rfl
  by_cases hmid : σ ≤ 4172629/10^7
  · have hω := (hw0 σ ⟨hlo.le, hmid⟩).le.trans (show (78270152/10^8 : ℝ) ≤ 7827016/10^7 by norm_num)
    unfold RSThetaRate.ω₀ at hω
    simp only [RSThetaCert.y0, RSThetaCert.e1_0, RSThetaCert.e2_0, hq, Nat.cast_ofNat] at hω
    exact star_of_cert G S (6212/10000) _ _ (69/200) _ (by norm_num) (by norm_num) (by norm_num)
      (by norm_num) hn hsn (rstheta_moment_bound_0 G hG S hS) hω
  · push Not at hmid
    have hω := (hw1 σ ⟨hmid.le, hhi.le⟩).le.trans (show (78270152/10^8 : ℝ) ≤ 7827016/10^7 by norm_num)
    unfold RSThetaRate.ω₁ at hω
    simp only [RSThetaCert.y1, RSThetaCert.e1_1, RSThetaCert.e2_1, hq, Nat.cast_ofNat] at hω
    exact star_of_cert G S (6293/10000) _ _ (17/50) _ (by norm_num) (by norm_num) (by norm_num)
      (by norm_num) hn hsn (rstheta_moment_bound_1 G hG S hS) hω

/-! ### The completeness inequality of `thm:rs` -/

/-- The completeness inequality in the proof of thm:rs. -/
theorem rs_star (G : SimpleGraph V) [DecidableRel G.Adj] (hG : G.Connected)
    (S : Finset V) (hS : IsCDS G S) :
    MLS.Star (gT G) S S.card (80309062/10^8) 2 := by
  have hs0 := card_pos_of_isCDS hS
  have hsn : S.card ≤ Fintype.card V := card_le_univ S
  have hn0 : (0:ℝ) < Fintype.card V := by exact_mod_cast lt_of_lt_of_le hs0 hsn
  have hs0' : (0:ℝ) < S.card := by exact_mod_cast hs0
  have hσ0 : 0 < (S.card : ℝ) / Fintype.card V := div_pos hs0' hn0
  have hσ1 : (S.card : ℝ) / Fintype.card V ≤ 1 := by
    rw [div_le_one hn0]; exact_mod_cast hsn
  obtain ⟨hR1, -, -⟩ := RSRate.rs_rate_c
  obtain ⟨hC, -, -⟩ := RSRate.rs_constants
  exact star_mono (by norm_num) (rs_moments G hG S hS) ((hR1 _ ⟨hσ0, hσ1⟩).trans hC.le)

end MaxLeafFormal.RateAssembly