MaxLeafFormal.RSCSteiner

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

import MaxLeafFormal.RSCCompose
import MaxLeafFormal.SteinerCDS

/-!
# Algorithm RSC with its Steiner step

No function in this file (or in `SteinerDir`/`SteinerCDS`) returns a connected dominating set or a
spanning tree: `rscAcceptSt_witness` and `rscAcceptSt_witness_min` only state that they exist.
-/

namespace MaxLeafFormal.RSCSteiner

open Finset
open MaxLeafFormal.CDS (IsCDS γc termCount numLeaves)
open MaxLeafFormal.Budget (CdsOutcome cdsMeasure cdsOutput Mcount)

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

/-- Step (c) of alg:rsc-algorithm with `𝒜_St` itself. -/
def rscAcceptSt (G : SimpleGraph V) [DecidableRel G.Adj] (s θ : ℕ) : Set (Finset V × Finset V) :=
  {z | (z.1 ∪ z.2).card ≤ s ∧ termCount G (z.1 ∪ z.2) ≤ θ ∧ SteinerCDS.aSt G (z.1 ∪ z.2) s}

-- `rscAcceptSt` equals `RSCTrials.rscAccept` (uses `SteinerCDS.aSt_iff_extYes`, with `hk` from the first conjunct)

theorem rscAcceptSt_eq (G : SimpleGraph V) [DecidableRel G.Adj] (s θ : ℕ) :
    rscAcceptSt G s θ = RSCTrials.rscAccept G s θ := by
  ext z
  simp only [rscAcceptSt, RSCTrials.rscAccept, Set.mem_ofPred_eq]
  constructor
  · rintro ⟨h1, h2, h3⟩
    exact ⟨h1, h2, (SteinerCDS.aSt_iff_extYes G _ s h1).mp h3⟩
  · rintro ⟨h1, h2, h3⟩
    exact ⟨h1, h2, (SteinerCDS.aSt_iff_extYes G _ s h1).mpr h3⟩

section Data
open Pointwise
open MaxLeafFormal.RSCParams
open MaxLeafFormal.RSCCert (merge init jOf)
open MaxLeafFormal.Antinorm8 (PZ cZ initInf)

-- `RSCCompose.rsc_success_of_data` with the Steiner step; the same binders.

theorem rsc_success_of_data_st (Z : Finset (Fin 8 → ℝ)) (hZ : Z.Nonempty) (hZ0 : ∀ z ∈ Z, 0 ≤ z)
    (C1 : ∀ z ∈ Z, ∀ z' ∈ Z, merge p₂ p₃ z z' ∈ PZ Z)
    (C2 : (∀ ν ≤ ν₀, init p₂ p₃ y ϖ₂ ϖ₃ ν 0 0 ∈ ê ^ (1 + ν) • PZ Z) ∧
          initInf p₂ y ∈ ê ^ (ν₀ + 2) • PZ Z)
    (C4 : ∀ ν, 2 ≤ ν → ν ≤ νE → d₃ ν ≤ 1 →
          (∀ c₃, 1 ≤ c₃ → c₃ ≤ ν - 1 → init p₂ p₃ y ϖ₂ ϖ₃ ν 0 c₃ ∈ ê ^ (1 + ν) • PZ Z) ∧
          (d₂ ν ≤ 1 → ∀ c₂ c₃, 1 ≤ c₂ → c₂ + c₃ ≤ ν - 1 →
             init p₂ p₃ y ϖ₂ ϖ₃ ν c₂ c₃ ∈ ê ^ (1 + ν) • PZ Z))
    (C5 : ∀ ν, 1 ≤ ν → ν ≤ νE → ∀ c₂ c₃, 1 ≤ c₂ + c₃ → c₂ + c₃ ≤ ν →
          ∀ Qs : List (Fin 8 → ℝ), Qs.length = (if c₂ = 0 then jOf d₃ ν else jOf d₂ ν) →
          (∀ Q ∈ Qs, Q ∈ PZ Z ∧ 0 ≤ Q) →
          Qs.foldl (merge p₂ p₃) ((ê ^ (1 + ν))⁻¹ • init p₂ p₃ y ϖ₂ ϖ₃ ν c₂ c₃) ∈ PZ Z)
    (hc : (6060/10000 : ℝ) < cZ p₂ Z hZ)
    (G : SimpleGraph V) [DecidableRel G.Adj] (hG : G.Connected) (κ : ℝ) (hκ : 0 < κ)
    (Θ : ℕ → ℕ)
    (hΘ : ∀ s, 1 ≤ s → s ≤ Fintype.card V →
      RSCTrials.rscOmega * Fintype.card V + Real.logb 2 2 + 1 ≤ Θ s)
    (m : ℕ → ℕ → ℕ → ℕ)
    (hm : ∀ s t θ, 1 ≤ s → s ≤ Fintype.card V → t ≤ s → θ ≤ Θ s →
      Mcount (Fintype.card V) RSCTrials.rscOmega 2 κ (Θ s) θ ≤ m s t θ) :
    (∀ o : CdsOutcome (Fintype.card V) (fun _ _ _ => Finset V × Finset V) Θ m,
        γc G ≤ cdsOutput (Fintype.card V) (fun s _ θ => rscAcceptSt G s θ) o) ∧
    1 - Real.exp (-κ)
      ≤ (cdsMeasure (Fintype.card V)
          (fun _ t _ => RSCTrials.rscTrialMeasure G (7/100) (77/1000) t) Θ m).real
          {o | cdsOutput (Fintype.card V) (fun s _ θ => rscAcceptSt G s θ) o = γc G} := by
  simp only [rscAcceptSt_eq]
  exact RSCCompose.rsc_success_of_data Z hZ hZ0 C1 C2 C4 C5 hc G hG κ hκ Θ hΘ m hm

-- `RSCCompose.rsc_maxLeaf_of_data` with the Steiner step; the same binders.

theorem rsc_maxLeaf_of_data_st (Z : Finset (Fin 8 → ℝ)) (hZ : Z.Nonempty) (hZ0 : ∀ z ∈ Z, 0 ≤ z)
    (C1 : ∀ z ∈ Z, ∀ z' ∈ Z, merge p₂ p₃ z z' ∈ PZ Z)
    (C2 : (∀ ν ≤ ν₀, init p₂ p₃ y ϖ₂ ϖ₃ ν 0 0 ∈ ê ^ (1 + ν) • PZ Z) ∧
          initInf p₂ y ∈ ê ^ (ν₀ + 2) • PZ Z)
    (C4 : ∀ ν, 2 ≤ ν → ν ≤ νE → d₃ ν ≤ 1 →
          (∀ c₃, 1 ≤ c₃ → c₃ ≤ ν - 1 → init p₂ p₃ y ϖ₂ ϖ₃ ν 0 c₃ ∈ ê ^ (1 + ν) • PZ Z) ∧
          (d₂ ν ≤ 1 → ∀ c₂ c₃, 1 ≤ c₂ → c₂ + c₃ ≤ ν - 1 →
             init p₂ p₃ y ϖ₂ ϖ₃ ν c₂ c₃ ∈ ê ^ (1 + ν) • PZ Z))
    (C5 : ∀ ν, 1 ≤ ν → ν ≤ νE → ∀ c₂ c₃, 1 ≤ c₂ + c₃ → c₂ + c₃ ≤ ν →
          ∀ Qs : List (Fin 8 → ℝ), Qs.length = (if c₂ = 0 then jOf d₃ ν else jOf d₂ ν) →
          (∀ Q ∈ Qs, Q ∈ PZ Z ∧ 0 ≤ Q) →
          Qs.foldl (merge p₂ p₃) ((ê ^ (1 + ν))⁻¹ • init p₂ p₃ y ϖ₂ ϖ₃ ν c₂ c₃) ∈ PZ Z)
    (hc : (6060/10000 : ℝ) < cZ p₂ Z hZ)
    (G : SimpleGraph V) [DecidableRel G.Adj] (hG : G.Connected) (κ : ℝ) (hκ : 0 < κ)
    (Θ : ℕ → ℕ)
    (hΘ : ∀ s, 1 ≤ s → s ≤ Fintype.card V →
      RSCTrials.rscOmega * Fintype.card V + Real.logb 2 2 + 1 ≤ Θ s)
    (m : ℕ → ℕ → ℕ → ℕ)
    (hm : ∀ s t θ, 1 ≤ s → s ≤ Fintype.card V → t ≤ s → θ ≤ Θ s →
      Mcount (Fintype.card V) RSCTrials.rscOmega 2 κ (Θ s) θ ≤ m s t θ)
    (hn : 3 ≤ Fintype.card V) :
    1 - Real.exp (-κ)
      ≤ (cdsMeasure (Fintype.card V)
          (fun _ t _ => RSCTrials.rscTrialMeasure G (7/100) (77/1000) t) Θ m).real
          {o | IsGreatest {ℓ | ∃ F : SimpleGraph V, F ≤ G ∧ F.IsTree ∧ MaxLeafFormal.CDS.numLeaves F = ℓ}
                 (Fintype.card V - cdsOutput (Fintype.card V)
                    (fun s _ θ => rscAcceptSt G s θ) o)} := by
  simp only [rscAcceptSt_eq]
  exact RSCCompose.rsc_maxLeaf_of_data Z hZ hZ0 C1 C2 C4 C5 hc G hG κ hκ Θ hΘ m hm hn

end Data

-- An accepted trial extends to a CDS of size ≤ s and a spanning tree with
-- ≥ n − |S| leaves (existence only; no minimality)

theorem rscAcceptSt_witness (G : SimpleGraph V) [DecidableRel G.Adj] (hG : G.Connected)
    (s θ : ℕ) (z : Finset V × Finset V) (hz : z ∈ rscAcceptSt G s θ) :
    ∃ S : Finset V, z.1 ∪ z.2 ⊆ S ∧ IsCDS G S ∧ S.card ≤ s ∧
      ∃ F : SimpleGraph V, F ≤ G ∧ F.IsTree ∧ (∀ v ∉ S, Nat.card (F.neighborSet v) = 1) ∧
        Fintype.card V - S.card ≤ numLeaves F := by
  rw [rscAcceptSt_eq] at hz
  simp only [RSCTrials.rscAccept, MLS.ExtYes, Set.mem_ofPred_eq] at hz
  obtain ⟨hcard, _, Y, hdisj, hY, hcds⟩ := hz
  refine ⟨z.1 ∪ z.2 ∪ Y, subset_union_left, hcds, ?_,
    MaxLeafFormal.CDS.spanningTree_of_CDS G hG _ hcds⟩
  rw [card_union_of_disjoint hdisj]
  omega

-- At s = γc G the CDS is minimum, and for n ≥ 3 the tree has exactly
-- n − γc G leaves, the most of any spanning tree (existence only)

theorem rscAcceptSt_witness_min (G : SimpleGraph V) [DecidableRel G.Adj] (hG : G.Connected)
    (θ : ℕ) (z : Finset V × Finset V) (hz : z ∈ rscAcceptSt G (γc G) θ) :
    ∃ S : Finset V, z.1 ∪ z.2 ⊆ S ∧ IsCDS G S ∧ S.card = γc G ∧
      ∃ F : SimpleGraph V, F ≤ G ∧ F.IsTree ∧ (∀ v ∉ S, Nat.card (F.neighborSet v) = 1) ∧
        (3 ≤ Fintype.card V →
          numLeaves F = Fintype.card V - γc G ∧
          IsGreatest {ℓ | ∃ F' : SimpleGraph V, F' ≤ G ∧ F'.IsTree ∧ numLeaves F' = ℓ}
            (numLeaves F)) := by
  obtain ⟨S, hzS, hS, hSc, F, hFG, hF, hleaf, hnum⟩ := rscAcceptSt_witness G hG (γc G) θ z hz
  have hge : γc G ≤ S.card := Nat.sInf_le ⟨S, hS, rfl⟩
  have hSeq : S.card = γc G := le_antisymm hSc hge
  refine ⟨S, hzS, hS, hSeq, F, hFG, hF, hleaf, fun hn => ?_⟩
  have hmax := MaxLeafFormal.CDS.maxLeaf_eq G hG hn
  have hle : numLeaves F ≤ Fintype.card V - γc G := hmax.2 ⟨F, hFG, hF, rfl⟩
  have heq : numLeaves F = Fintype.card V - γc G := by rw [hSeq] at hnum; omega
  refine ⟨heq, ?_⟩
  rw [heq]
  exact hmax

end MaxLeafFormal.RSCSteiner