MaxLeafFormal.RSCCompose

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

Statements of the paper formalised here: Proposition 8.6, Theorem 8.1.

import MaxLeafFormal.RSCGraph
import MaxLeafFormal.RSCTrials

/-!
# Composition of `prop:rsc-bound` and the success bound of `thm:rsc`

* (A) `Wcl_eq`: the two transcriptions `RSCGraph.Wcl` and `RSCTrials.Wcl` of `W^cl_S(y)`
  (`def:rsc-gf`) are equal, with no hypotheses.
* (B) `rsc_success_of_data`: the success part of `thm:rsc`, conditional on conditions (C1), (C2),
  (C4), (C5) of `lem:rsc-cert` for the parameters of `prop:rsc-cert` and `c_Z > 0.6060`.
* `rsc_rho_lt`: `1.6990 < ϱ < 1.6991`; `rsc_maxLeaf_of_data`: the Max Leaf clause of `thm:rsc`
  for `n ≥ 3`.
-/

namespace MaxLeafFormal.RSCCompose

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

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

section Bridge
variable (G : SimpleGraph V) [DecidableRel G.Adj]

theorem pk_eq_of_two_le (p₂ p₃ : ℝ) (k : ℕ) (hk : 2 ≤ k) :
    RSCTree.pk p₂ p₃ k = RSCTrials.pk p₂ p₃ k := by
  unfold RSCTree.pk RSCTrials.pk
  rcases Nat.lt_or_ge 2 k with h | h
  · rw [ite_eq_right (by omega), ite_eq_right (by omega)]
  · rw [ite_eq_left h, ite_eq_left (by omega)]

theorem nbrCount_eq (X' : Finset V) (v : V) :
    RSCGraph.nbrCount G X' v = (G.neighborFinset v ∩ X').card := by
  unfold RSCGraph.nbrCount
  congr 1
  ext w
  simp [SimpleGraph.mem_neighborFinset, and_comm]

theorem cand_eq (X' : Finset V) : RSCGraph.cand G X' = RSCTrials.cand G X' := by
  ext v
  simp [RSCGraph.cand, RSCTrials.cand, nbrCount_eq]

theorem closureProb_eq_prodMeas (p₂ p₃ : ℝ) (X' U : Finset V) :
    RSCTrials.closureProb G p₂ p₃ X' U =
      if U ⊆ RSCGraph.cand G X' then
        RSCTree.prodMeas (fun v => RSCTree.pk p₂ p₃ (RSCGraph.nbrCount G X' v))
          (RSCGraph.cand G X') U
      else 0 := by
  have hk : ∀ v ∈ RSCTrials.cand G X',
      RSCTrials.inclProb G p₂ p₃ X' v = RSCTree.pk p₂ p₃ (RSCGraph.nbrCount G X' v) := by
    intro v hv
    have h2 : 2 ≤ (G.neighborFinset v ∩ X').card := by
      simp only [RSCTrials.cand, Finset.mem_filter, Finset.mem_univ, true_and] at hv
      exact hv.2
    rw [RSCTrials.inclProb, nbrCount_eq, pk_eq_of_two_le p₂ p₃ _ h2]
  unfold RSCTrials.closureProb RSCTree.prodMeas
  rw [cand_eq]
  split_ifs with hU
  · congr 1
    · exact Finset.prod_congr rfl fun v hv => hk v (hU hv)
    · exact Finset.prod_congr rfl fun v hv => by rw [hk v (Finset.mem_sdiff.1 hv).1]
  · rfl

-- Bridge (A); no hypotheses on p₂, p₃, y or S

theorem Wcl_eq (S : Finset V) (p₂ p₃ y : ℝ) :
    RSCGraph.Wcl G S p₂ p₃ y = RSCTrials.Wcl G p₂ p₃ S y := by
  unfold RSCGraph.Wcl RSCTrials.Wcl
  refine Finset.sum_congr rfl fun X' _ => ?_
  congr 1
  rw [← Finset.sum_subset (Finset.subset_univ (RSCGraph.cand G X').powerset)]
  · refine Finset.sum_congr rfl fun U hU => ?_
    have hU' : U ⊆ RSCGraph.cand G X' := Finset.mem_powerset.1 hU
    rw [closureProb_eq_prodMeas, ite_eq_left hU']
    split_ifs with hS
    · rw [Real.rpow_neg (by norm_num), Real.rpow_natCast, one_div, inv_pow, mul_one]
    · simp
  · intro U _ hU
    have hU' : ¬ U ⊆ RSCGraph.cand G X' := fun h => hU (Finset.mem_powerset.2 h)
    rw [closureProb_eq_prodMeas, ite_eq_right hU', zero_mul]

end Bridge

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

-- prop:rsc-bound in the exact form of `hbound` of `rsc_success_of_bound`.
-- The binders Z … hc are copied verbatim from `RSCGraph.rsc_bound_of_data'`.

theorem rsc_bound_trials (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) :
    ∀ S : Finset V, IsCDS G S → S.card = γc G →
      (0.6060 : ℝ) * (145729958 / 189014575 : ℝ) ^ Fintype.card V
        ≤ RSCTrials.Wcl G (7/100) (77/1000) S (31/100) := by
  intro S hS hmin
  have h := RSCGraph.rsc_bound_of_data' Z hZ hZ0 C1 C2 C4 C5 hc G hG S hS hmin
  rw [Wcl_eq] at h
  have e1 : (0.6060 : ℝ) = 6060/10000 := by norm_num
  rw [e1]
  simpa [p₂, p₃, y, ê] using h

-- Composition (B). Conclusion copied verbatim from `RSCTrials.rsc_success_of_bound`.

theorem rsc_success_of_data (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 _ θ => RSCTrials.rscAccept 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 _ θ => RSCTrials.rscAccept G s θ) o = γc G} :=
  RSCTrials.rsc_success_of_bound G hG κ hκ Θ hΘ m hm
    (rsc_bound_trials Z hZ hZ0 C1 C2 C4 C5 hc G hG)

-- 1.6990 < ϱ < 1.6991

theorem rsc_rho_lt : (16990/10000 : ℝ) < (1 + 31/100) / (145729958 / 189014575) ∧
    (1 + 31/100 : ℝ) / (145729958 / 189014575) < 16991/10000 := by
  constructor <;> norm_num

-- The Max Leaf clause of thm:rsc

theorem rsc_maxLeaf_of_data (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 _ θ => RSCTrials.rscAccept G s θ) o)} := by
  have hp : (0:ℝ) ≤ 7/100 ∧ (7/100:ℝ) ≤ 77/1000 ∧ (77/1000:ℝ) ≤ 1 := by norm_num
  have hPi : ∀ (i : Fin (Fintype.card V)) (t : Fin ((i : ℕ) + 1 + 1)),
      MeasureTheory.IsProbabilityMeasure (RSCTrials.rscTrialMeasure G (7/100) (77/1000) (t : ℕ)) :=
    fun i t => RSCTrials.isProbabilityMeasure_rscTrialMeasure G _ _ hp _ (by omega)
  have hB : ∀ i : Fin (Fintype.card V), MeasureTheory.IsProbabilityMeasure
      (MaxLeafFormal.Budget.budgetMeasure
        (fun (t : Fin ((i : ℕ) + 1 + 1)) (_ : ℕ) =>
          RSCTrials.rscTrialMeasure G (7/100) (77/1000) (t : ℕ))
        (Θ ((i : ℕ) + 1)) (fun t θ => m ((i : ℕ) + 1) t θ)) := fun i => by
    unfold MaxLeafFormal.Budget.budgetMeasure; infer_instance
  have hprob : MeasureTheory.IsProbabilityMeasure (cdsMeasure (Fintype.card V)
      (fun _ t _ => RSCTrials.rscTrialMeasure G (7/100) (77/1000) t) Θ m) := by
    unfold cdsMeasure; infer_instance
  obtain ⟨-, h⟩ := rsc_success_of_data Z hZ hZ0 C1 C2 C4 C5 hc G hG κ hκ Θ hΘ m hm
  refine h.trans (MeasureTheory.measureReal_mono ?_)
  intro o ho
  simp only [Set.mem_ofPred_eq] at ho ⊢
  rw [ho]
  exact MaxLeafFormal.CDS.maxLeaf_eq G hG hn

end Data
end MaxLeafFormal.RSCCompose
Back to top