MaxLeafFormal.PDGraph

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

Statements of the paper formalised here: Lemma D.11.18, Lemma D.11.19, Theorem 12.10, Proposition 12.11.

import MaxLeafFormal.PDRate
import MaxLeafFormal.MLSNec
import MaxLeafFormal.CDS

/-!
# Paired Domination: the graph argument and tightness

`lem:fa-pd-point`, the second claim of `lem:fa-pd-rate` and `prop:fa-pd-tight`.
-/
namespace MaxLeafFormal.PDGraph
open Finset SimpleGraph MaxLeafFormal.MLS MaxLeafFormal.PDRate

namespace Aux

theorem sqrt3_sq : Real.sqrt 3 ^ 2 = 3 := Real.sq_sqrt (by norm_num)

theorem sqrt3_gt_one : 1 < Real.sqrt 3 := by
  nlinarith [Real.sqrt_nonneg 3, sqrt3_sq]

theorem ystar_pos : 0 < ystar := by
  unfold ystar
  linarith [sqrt3_gt_one]

theorem N_factor (y : ℝ) :
    4 * y ^ 2 + y / 2 - 13 / 32 = 4 * (y - ystar) * (y - (-1 - 3 * Real.sqrt 3) / 16) := by
  unfold ystar
  linear_combination (9 / 64 : ℝ) * sqrt3_sq

end Aux

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

/-- `und(X) = V \ N[X]`. -/
def und (G : SimpleGraph V) [DecidableRel G.Adj] (X : Finset V) : Finset V :=
  univ \ CDS.closedNbhd G X

/-- The running-time exponent `g(X) = |und(X)|`; it ignores the size argument. -/
def pdG (G : SimpleGraph V) [DecidableRel G.Adj] : Finset V → ℕ → ℝ :=
  fun X _ => ((und G X).card : ℝ)

/-- `W_S(y)` for the exponent `|und(X)|`. -/
noncomputable def pdW (G : SimpleGraph V) [DecidableRel G.Adj] (S : Finset V) (y : ℝ) : ℝ :=
  W (pdG G) S S.card y

def IsDominating (G : SimpleGraph V) (S : Finset V) : Prop :=
  ∀ v, v ∈ S ∨ ∃ u ∈ S, G.Adj v u

/-- A paired dominating set: dominating, and `G[S]` has a perfect matching. -/
def IsPairedDom (G : SimpleGraph V) (S : Finset V) : Prop :=
  IsDominating G S ∧ ∃ M : G.Subgraph, M.verts = (S : Set V) ∧ M.IsMatching

/-- An oriented perfect matching of `G[S]`, as a finite set of ordered pairs. -/
def IsPairing (G : SimpleGraph V) (S : Finset V) (P : Finset (V × V)) : Prop :=
  (∀ q ∈ P, q.1 ∈ S ∧ q.2 ∈ S ∧ G.Adj q.1 q.2) ∧
  ∀ w ∈ S, ∃! q : V × V, q ∈ P ∧ (q.1 = w ∨ q.2 = w)

/-- Anchors: every vertex outside `S` gets a neighbour in `S`. -/
def IsAnchor (G : SimpleGraph V) (S : Finset V) (anc : V → V) : Prop :=
  ∀ v, v ∉ S → anc v ∈ S ∧ G.Adj v (anc v)

/-- `d_u`, the number of vertices anchored at `u`. -/
def ancDeg (S : Finset V) (anc : V → V) (u : V) : ℕ :=
  (univ.filter (fun v => v ∉ S ∧ anc v = u)).card

/-- The right-hand side of the first inequality of `lem:fa-pd-point`. -/
def pdRhs (S : Finset V) (P : Finset (V × V)) (anc : V → V) (X : Finset V) : ℕ :=
  (univ.filter (fun v => v ∉ S ∧ anc v ∉ X)).card +
    2 * (P.filter (fun q => q.1 ∉ X ∧ q.2 ∉ X)).card

/-- `Ω_{uv}(y) = y² + y(2^{-d_u} + 2^{-d_v}) + 2^{-n_{uv}}`, `n_{uv} = 2 + d_u + d_v`. -/
noncomputable def Ωpair (y : ℝ) (du dv : ℕ) : ℝ :=
  y ^ 2 + y * ((2:ℝ) ^ (-(du : ℝ)) + (2:ℝ) ^ (-(dv : ℝ))) + (2:ℝ) ^ (-((2 + du + dv : ℕ) : ℝ))

theorem pdW_eq (G : SimpleGraph V) [DecidableRel G.Adj] (S : Finset V) (y : ℝ) :
    pdW G S y = ∑ X ∈ S.powerset, y ^ X.card * (2:ℝ) ^ (-((und G X).card : ℝ)) := by
  rfl

namespace Aux

theorem two_rpow_neg_nat (m : ℕ) : (2:ℝ) ^ (-(m:ℝ)) = (1 / 2 : ℝ) ^ m := by
  rw [Real.rpow_neg (by norm_num), Real.rpow_natCast, one_div, inv_pow]

/-- Subsets of a disjoint union are pairs of subsets. -/
theorem sum_powerset_union {W β : Type*} [DecidableEq W] [AddCommMonoid β] (A C : Finset W)
    (hAC : Disjoint A C) (f : Finset W → Finset W → β) :
    ∑ X ∈ (A ∪ C).powerset, f (X ∩ A) (X ∩ C) = ∑ Z ∈ A.powerset, ∑ Y ∈ C.powerset, f Z Y := by
  rw [← sum_product' (f := f)]
  refine sum_nbij' (fun X => (X ∩ A, X ∩ C)) (fun p => p.1 ∪ p.2) ?_ ?_ ?_ ?_ ?_
  · intro X _
    simp only [mem_coe, mem_product, mem_powerset]
    exact ⟨inter_subset_right, inter_subset_right⟩
  · intro p hp
    simp only [mem_coe, mem_product, mem_powerset] at hp ⊢
    exact union_subset_union hp.1 hp.2
  · intro X hX
    simp only [mem_coe, mem_powerset] at hX
    simp only
    rw [← inter_union_distrib_left, inter_eq_left.2 hX]
  · intro p hp
    simp only [mem_coe, mem_product, mem_powerset] at hp
    obtain ⟨h1, h2⟩ := hp
    refine Prod.ext ?_ ?_
    · ext x
      simp only [mem_inter, mem_union]
      constructor
      · rintro ⟨hx | hx, hxA⟩
        · exact hx
        · exact absurd (h2 hx) (disjoint_left.1 hAC hxA)
      · intro hx; exact ⟨Or.inl hx, h1 hx⟩
    · ext x
      simp only [mem_inter, mem_union]
      constructor
      · rintro ⟨hx | hx, hxC⟩
        · exact absurd hxC (disjoint_left.1 hAC (h1 hx))
        · exact hx
      · intro hx; exact ⟨Or.inr hx, h2 hx⟩
  · intro X _
    rfl

/-- Sums over subsets of a disjoint union of blocks factor over the blocks. -/
theorem sum_powerset_blocks {W ι β : Type*} [DecidableEq W] [DecidableEq ι] [CommSemiring β]
    (s : Finset ι) (B : ι → Finset W) (hdisj : ∀ i ∈ s, ∀ j ∈ s, i ≠ j → Disjoint (B i) (B j))
    (F : ι → Finset W → β) :
    ∑ X ∈ (s.biUnion B).powerset, ∏ i ∈ s, F i (X ∩ B i)
      = ∏ i ∈ s, ∑ Z ∈ (B i).powerset, F i Z := by
  induction s using Finset.induction_on with
  | empty => simp
  | @insert a s ha ih =>
    have hdisj' : ∀ i ∈ s, ∀ j ∈ s, i ≠ j → Disjoint (B i) (B j) := fun i hi j hj =>
      hdisj i (mem_insert_of_mem hi) j (mem_insert_of_mem hj)
    have hAC : Disjoint (B a) (s.biUnion B) := by
      rw [disjoint_biUnion_right]
      intro i hi
      exact hdisj a (mem_insert_self a s) i (mem_insert_of_mem hi) (fun h => ha (h ▸ hi))
    calc ∑ X ∈ ((insert a s).biUnion B).powerset, ∏ i ∈ insert a s, F i (X ∩ B i)
        = ∑ X ∈ (B a ∪ s.biUnion B).powerset,
            F a (X ∩ B a) * ∏ i ∈ s, F i ((X ∩ s.biUnion B) ∩ B i) := by
          rw [biUnion_insert]
          refine sum_congr rfl fun X _ => ?_
          rw [prod_insert ha]
          congr 1
          refine prod_congr rfl fun i hi => ?_
          rw [inter_assoc, inter_eq_right.2 (subset_biUnion_of_mem B hi)]
      _ = ∑ Z ∈ (B a).powerset, ∑ Y ∈ (s.biUnion B).powerset,
            F a Z * ∏ i ∈ s, F i (Y ∩ B i) :=
          sum_powerset_union (B a) (s.biUnion B) hAC
            (fun Z Y => F a Z * ∏ i ∈ s, F i (Y ∩ B i))
      _ = ∏ i ∈ insert a s, ∑ Z ∈ (B i).powerset, F i Z := by
          rw [prod_insert ha, ← ih hdisj', sum_mul_sum]

end Aux

/-- The unique pair of a pairing that contains a vertex is determined by that vertex. -/
theorem IsPairing.eq_of_mem {G : SimpleGraph V} {S : Finset V} {P : Finset (V × V)}
    (hP : IsPairing G S P) {q q' : V × V} (hq : q ∈ P) (hq' : q' ∈ P) {w : V}
    (hw : q.1 = w ∨ q.2 = w) (hw' : q'.1 = w ∨ q'.2 = w) : q = q' := by
  have hwS : w ∈ S := by
    rcases hw with h | h
    · exact h ▸ (hP.1 q hq).1
    · exact h ▸ (hP.1 q hq).2.1
  exact (hP.2 w hwS).unique ⟨hq, hw⟩ ⟨hq', hw'⟩

theorem IsPairing.fst_ne_snd {G : SimpleGraph V} {S : Finset V} {P : Finset (V × V)}
    (hP : IsPairing G S P) {q : V × V} (hq : q ∈ P) : q.1 ≠ q.2 :=
  G.ne_of_adj (hP.1 q hq).2.2

/-- The pairs of a pairing partition `S`: sums over `S` split into sums over pairs. -/
theorem IsPairing.sum_ends {G : SimpleGraph V} {S : Finset V} {P : Finset (V × V)}
    (hP : IsPairing G S P) {β : Type*} [AddCommMonoid β] (f : V → β) :
    ∑ q ∈ P, (f q.1 + f q.2) = ∑ w ∈ S, f w := by
  have hS : S = P.biUnion (fun q => ({q.1, q.2} : Finset V)) := by
    ext w
    simp only [mem_biUnion, mem_insert, mem_singleton]
    constructor
    · intro hw
      obtain ⟨q, ⟨hq, hqw⟩, -⟩ := hP.2 w hw
      exact ⟨q, hq, by rcases hqw with h | h <;> [left; right] <;> exact h.symm⟩
    · rintro ⟨q, hq, h | h⟩
      · exact h ▸ (hP.1 q hq).1
      · exact h ▸ (hP.1 q hq).2.1
  rw [hS, sum_biUnion]
  · refine sum_congr rfl fun q hq => ?_
    rw [sum_pair (hP.fst_ne_snd hq)]
  · intro q hq q' hq' hne
    simp only [Function.onFun]
    rw [Finset.disjoint_left]
    intro w hw hw'
    simp only [mem_insert, mem_singleton] at hw hw'
    exact hne (hP.eq_of_mem hq hq' (by rcases hw with h | h <;> [left; right] <;> exact h.symm)
      (by rcases hw' with h | h <;> [left; right] <;> exact h.symm))

/-- Every perfect matching `M` of `G[S]` (Mathlib form) is listed by a pairing `P`
with exactly the same edges. -/
theorem pairing_of_matching (G : SimpleGraph V) (S : Finset V) (M : G.Subgraph)
    (hMv : M.verts = (S : Set V)) (hM : M.IsMatching) :
    ∃ P : Finset (V × V), IsPairing G S P ∧ ∀ a b, M.Adj a b ↔ ((a, b) ∈ P ∨ (b, a) ∈ P) := by
  classical
  let e := Fintype.equivFin V
  let P : Finset (V × V) := (univ ×ˢ univ).filter (fun q => M.Adj q.1 q.2 ∧ e q.1 < e q.2)
  have hmemP : ∀ a b, (a, b) ∈ P ↔ M.Adj a b ∧ e a < e b := by
    intro a b; simp [P]
  have hvS : ∀ v, v ∈ M.verts ↔ v ∈ S := by
    intro v; rw [hMv]; rfl
  refine ⟨P, ⟨?_, ?_⟩, ?_⟩
  · rintro ⟨a, b⟩ hq
    rw [hmemP] at hq
    exact ⟨(hvS a).1 (M.edge_vert hq.1), (hvS b).1 (M.edge_vert hq.1.symm), M.adj_sub hq.1⟩
  · intro w hw
    obtain ⟨w', hww', huniq⟩ := hM ((hvS w).2 hw)
    have hne : w ≠ w' := G.ne_of_adj (M.adj_sub hww')
    have hene : e w ≠ e w' := fun h => hne (e.injective h)
    rcases lt_or_gt_of_ne hene with hlt | hlt
    · refine ⟨(w, w'), ⟨(hmemP w w').2 ⟨hww', hlt⟩, Or.inl rfl⟩, ?_⟩
      rintro ⟨a, b⟩ ⟨hq, h | h⟩
      · simp only at h; subst h
        rw [hmemP] at hq
        rw [huniq b hq.1]
      · simp only at h; subst h
        rw [hmemP] at hq
        have := huniq a hq.1.symm
        subst this
        exact absurd (hq.2.trans hlt) (lt_irrefl _)
    · refine ⟨(w', w), ⟨(hmemP w' w).2 ⟨hww'.symm, hlt⟩, Or.inr rfl⟩, ?_⟩
      rintro ⟨a, b⟩ ⟨hq, h | h⟩
      · simp only at h; subst h
        rw [hmemP] at hq
        have := huniq b hq.1
        subst this
        exact absurd (hq.2.trans hlt) (lt_irrefl _)
      · simp only at h; subst h
        rw [hmemP] at hq
        rw [huniq a hq.1.symm]
  · intro a b
    rw [hmemP, hmemP]
    constructor
    · intro h
      have hne : e a ≠ e b := fun h' => G.ne_of_adj (M.adj_sub h) (e.injective h')
      rcases lt_or_gt_of_ne hne with hlt | hlt
      · exact Or.inl ⟨h, hlt⟩
      · exact Or.inr ⟨h.symm, hlt⟩
    · rintro (h | h)
      · exact h.1
      · exact h.1.symm

/-- Every pairing `P` lists the edges of a perfect matching `M` of `G[S]` (Mathlib form). -/
theorem matching_of_pairing (G : SimpleGraph V) (S : Finset V) (P : Finset (V × V))
    (hP : IsPairing G S P) :
    ∃ M : G.Subgraph, M.verts = (S : Set V) ∧ M.IsMatching ∧
      ∀ a b, M.Adj a b ↔ ((a, b) ∈ P ∨ (b, a) ∈ P) := by
  let M : G.Subgraph :=
    { verts := (S : Set V)
      Adj := fun a b => (a, b) ∈ P ∨ (b, a) ∈ P
      adj_sub := by
        rintro a b (h | h)
        · exact (hP.1 _ h).2.2
        · exact (hP.1 _ h).2.2.symm
      edge_vert := by
        rintro a b (h | h)
        · exact (hP.1 _ h).1
        · exact (hP.1 _ h).2.1
      symm := ⟨fun a b h => h.symm⟩ }
  refine ⟨M, rfl, ?_, fun a b => Iff.rfl⟩
  intro v hv
  have hvS : v ∈ S := hv
  obtain ⟨⟨a, b⟩, ⟨hq, hqv⟩, -⟩ := hP.2 v hvS
  have hab : a ≠ b := hP.fst_ne_snd hq
  rcases hqv with h | h
  · simp only at h; subst h
    refine ⟨b, Or.inl hq, ?_⟩
    rintro w (hw | hw)
    · exact congrArg Prod.snd (hP.eq_of_mem hw hq (Or.inl rfl) (Or.inl rfl))
    · have := hP.eq_of_mem hw hq (Or.inr rfl) (Or.inl rfl)
      simp only [Prod.mk.injEq] at this
      exact absurd this.2 hab
  · simp only at h; subst h
    refine ⟨a, Or.inr hq, ?_⟩
    rintro w (hw | hw)
    · have := hP.eq_of_mem hw hq (Or.inl rfl) (Or.inr rfl)
      simp only [Prod.mk.injEq] at this
      exact absurd this.1.symm hab
    · exact congrArg Prod.fst (hP.eq_of_mem hw hq (Or.inr rfl) (Or.inr rfl))

theorem exists_anchor (G : SimpleGraph V) (S : Finset V) (hS : IsDominating G S) :
    ∃ anc : V → V, IsAnchor G S anc := by
  classical
  refine ⟨fun v => if h : v ∈ S then v else Classical.choose ((hS v).resolve_left h), ?_⟩
  intro v hv
  simp only [dif_neg hv]
  exact Classical.choose_spec ((hS v).resolve_left hv)

/-- `∑_{u ∈ S} (number of outside vertices anchored at u satisfying p)`. -/
theorem ancDeg.sum_eq {G : SimpleGraph V} {S : Finset V} {anc : V → V} (ha : IsAnchor G S anc)
    (T : Finset V) (hT : T ⊆ S) :
    ∑ u ∈ T, ancDeg S anc u = (univ.filter (fun v => v ∉ S ∧ anc v ∈ T)).card := by
  rw [card_eq_sum_card_fiberwise (f := anc) (t := T)]
  · refine sum_congr rfl fun u hu => ?_
    unfold ancDeg
    congr 1
    ext v
    simp only [mem_filter, mem_univ, true_and]
    constructor
    · rintro ⟨hv, rfl⟩; exact ⟨⟨hv, hu⟩, rfl⟩
    · rintro ⟨⟨hv, -⟩, rfl⟩; exact ⟨hv, rfl⟩
  · intro v hv
    simp at hv
    exact hv.2

/-- `∑_{uv ∈ M} n_{uv} = n`. -/
theorem card_eq_sum_pairs (G : SimpleGraph V) (S : Finset V) (P : Finset (V × V))
    (hP : IsPairing G S P) (anc : V → V) (ha : IsAnchor G S anc) :
    Fintype.card V = ∑ q ∈ P, (2 + ancDeg S anc q.1 + ancDeg S anc q.2) := by
  have h1 : ∑ q ∈ P, (2 + ancDeg S anc q.1 + ancDeg S anc q.2)
      = ∑ q ∈ P, ((1 + ancDeg S anc q.1) + (1 + ancDeg S anc q.2)) :=
    sum_congr rfl fun q _ => by ring
  rw [h1, hP.sum_ends (fun w => 1 + ancDeg S anc w), sum_add_distrib, ancDeg.sum_eq ha S
    subset_rfl, sum_const, smul_eq_mul, mul_one]
  have h2 : (univ.filter (fun v => v ∉ S ∧ anc v ∈ S)) = univ.filter (fun v => v ∉ S) := by
    ext v
    simp only [mem_filter, mem_univ, true_and]
    exact ⟨fun h => h.1, fun h => ⟨h, (ha v h).1⟩⟩
  rw [h2, ← card_univ, ← card_filter_add_card_filter_not (s := univ) (fun v => v ∈ S)]
  congr 1
  rw [filter_mem_eq_inter, univ_inter]

namespace Aux

theorem card_inter_pair {W : Type*} [DecidableEq W] (X : Finset W) {a b : W} (hab : a ≠ b) :
    (X ∩ {a, b}).card = (if a ∈ X then 1 else 0) + (if b ∈ X then 1 else 0) := by
  rw [inter_comm, ← filter_mem_eq_inter, card_filter, sum_pair hab]

/-- The exact factorization of `lem:fa-pd-point`. -/
theorem point_factor (G : SimpleGraph V) (S : Finset V)
    (P : Finset (V × V)) (hP : IsPairing G S P) (anc : V → V) (ha : IsAnchor G S anc) (y : ℝ) :
    ∑ X ∈ S.powerset, y ^ X.card * (2:ℝ) ^ (-(pdRhs S P anc X : ℝ))
      = ∏ q ∈ P, Ωpair y (ancDeg S anc q.1) (ancDeg S anc q.2) := by
  set d := ancDeg S anc with hd
  let e : V × V → Finset V := fun q => {q.1, q.2}
  let r : V × V → Finset V → ℕ := fun q Z =>
    (if q.1 ∉ Z then d q.1 else 0) + (if q.2 ∉ Z then d q.2 else 0) +
      (if q.1 ∉ Z ∧ q.2 ∉ Z then 2 else 0)
  let F : V × V → Finset V → ℝ := fun q Z => y ^ Z.card * (1 / 2 : ℝ) ^ r q Z
  have hS : S = P.biUnion e := by
    ext w
    simp only [e, mem_biUnion, mem_insert, mem_singleton]
    constructor
    · intro hw
      obtain ⟨q, ⟨hq, hqw⟩, -⟩ := hP.2 w hw
      exact ⟨q, hq, by rcases hqw with h | h <;> [left; right] <;> exact h.symm⟩
    · rintro ⟨q, hq, h | h⟩
      · exact h ▸ (hP.1 q hq).1
      · exact h ▸ (hP.1 q hq).2.1
  have hdisj : ∀ i ∈ P, ∀ j ∈ P, i ≠ j → Disjoint (e i) (e j) := by
    intro q hq q' hq' hne
    rw [Finset.disjoint_left]
    intro w hw hw'
    simp only [e, mem_insert, mem_singleton] at hw hw'
    exact hne (hP.eq_of_mem hq hq' (by rcases hw with h | h <;> [left; right] <;> exact h.symm)
      (by rcases hw' with h | h <;> [left; right] <;> exact h.symm))
  -- each term is a product over the pairs
  have hterm : ∀ X ∈ S.powerset, y ^ X.card * (2:ℝ) ^ (-(pdRhs S P anc X : ℝ))
      = ∏ q ∈ P, F q (X ∩ e q) := by
    intro X hX
    rw [mem_powerset] at hX
    have hcard : ∑ q ∈ P, (X ∩ e q).card = X.card := by
      have h1 : ∑ q ∈ P, (X ∩ e q).card
          = ∑ q ∈ P, ((if q.1 ∈ X then 1 else 0) + (if q.2 ∈ X then 1 else 0)) :=
        sum_congr rfl fun q hq => card_inter_pair X (hP.fst_ne_snd hq)
      have hs : ∑ q ∈ P, ((if q.1 ∈ X then 1 else 0) + (if q.2 ∈ X then 1 else 0))
          = ∑ w ∈ S, (if w ∈ X then 1 else 0) := hP.sum_ends (fun w => if w ∈ X then 1 else 0)
      rw [h1, hs, ← card_filter]
      congr 1
      ext w
      simp only [mem_filter]
      exact ⟨fun h => h.2, fun h => ⟨hX h, h⟩⟩
    have hr : ∑ q ∈ P, r q (X ∩ e q) = pdRhs S P anc X := by
      have hr1 : ∀ q ∈ P, r q (X ∩ e q) = ((if q.1 ∉ X then d q.1 else 0) +
          (if q.2 ∉ X then d q.2 else 0)) + (if q.1 ∉ X ∧ q.2 ∉ X then 2 else 0) := by
        intro q _
        simp only [r, e, mem_inter, mem_insert, mem_singleton, true_or, or_true, and_true]
      have hs : ∑ q ∈ P, ((if q.1 ∉ X then d q.1 else 0) + (if q.2 ∉ X then d q.2 else 0))
          = ∑ w ∈ S, (if w ∉ X then d w else 0) := hP.sum_ends (fun w => if w ∉ X then d w else 0)
      rw [sum_congr rfl hr1, sum_add_distrib, hs, ← sum_filter, ← sum_filter, sum_const,
        smul_eq_mul, hd, ancDeg.sum_eq ha _ (filter_subset _ _)]
      unfold pdRhs
      have hf : (univ.filter (fun v => v ∉ S ∧ anc v ∈ S.filter (fun w => w ∉ X)))
          = univ.filter (fun v => v ∉ S ∧ anc v ∉ X) := by
        ext v
        simp only [mem_filter, mem_univ, true_and]
        constructor
        · rintro ⟨hv, -, h⟩; exact ⟨hv, h⟩
        · rintro ⟨hv, h⟩; exact ⟨hv, (ha v hv).1, h⟩
      rw [hf]
      ring
    simp only [F]
    rw [prod_mul_distrib, prod_pow_eq_pow_sum, prod_pow_eq_pow_sum, hcard, hr,
      two_rpow_neg_nat]
  -- each factor is `Ωpair`
  have hfactor : ∀ q ∈ P, ∑ Z ∈ (e q).powerset, F q Z = Ωpair y (d q.1) (d q.2) := by
    intro q hq
    have hne : q.1 ≠ q.2 := hP.fst_ne_snd hq
    have hnot : q.1 ∉ ({q.2} : Finset V) := by simpa using hne
    simp only [e]
    have h0 : (∅ : Finset V) ≠ {q.2} := (singleton_nonempty _).ne_empty.symm
    have hps : ({q.2} : Finset V).powerset = {∅, {q.2}} := by
      ext Z; simp [Finset.subset_singleton_iff]
    rw [sum_powerset_insert hnot, hps, sum_pair h0, sum_pair h0]
    unfold Ωpair
    rw [two_rpow_neg_nat, two_rpow_neg_nat, two_rpow_neg_nat]
    simp [F, r, hne, hne.symm, card_pair hne]
    ring
  rw [sum_congr rfl hterm, hS, sum_powerset_blocks P e hdisj F]
  exact prod_congr rfl hfactor

end Aux

/-- `lem:fa-pd-point`. -/
theorem pd_point (G : SimpleGraph V) [DecidableRel G.Adj] (S : Finset V)
    (P : Finset (V × V)) (hP : IsPairing G S P) (anc : V → V) (ha : IsAnchor G S anc) :
    (∀ X ⊆ S, (und G X).card ≤ pdRhs S P anc X) ∧
    ∀ y : ℝ, 0 ≤ y →
      ∏ q ∈ P, Ωpair y (ancDeg S anc q.1) (ancDeg S anc q.2) ≤ pdW G S y := by
  have h1 : ∀ X ⊆ S, (und G X).card ≤ pdRhs S P anc X := by
    intro X _
    set A := univ.filter (fun v => v ∉ S ∧ anc v ∉ X)
    set Pf := P.filter (fun q => q.1 ∉ X ∧ q.2 ∉ X)
    have hsub : und G X ⊆ A ∪ Pf.biUnion (fun q => ({q.1, q.2} : Finset V)) := by
      intro v hv
      simp only [und, mem_sdiff, mem_univ, true_and, CDS.mem_closedNbhd, not_or, not_exists,
        not_and] at hv
      by_cases hvS : v ∈ S
      · obtain ⟨q, ⟨hq, hqv⟩, -⟩ := hP.2 v hvS
        have hadj := (hP.1 q hq).2.2
        have hboth : q.1 ∉ X ∧ q.2 ∉ X := by
          rcases hqv with h | h
          · rw [h] at hadj ⊢
            exact ⟨hv.1, fun h2 => hv.2 _ h2 hadj.symm⟩
          · rw [h] at hadj ⊢
            exact ⟨fun h2 => hv.2 _ h2 hadj, hv.1⟩
        refine mem_union_right _ (mem_biUnion.2 ⟨q, mem_filter.2 ⟨hq, hboth⟩, ?_⟩)
        rcases hqv with h | h
        · rw [← h]; exact mem_insert_self _ _
        · rw [← h]; exact mem_insert_of_mem (mem_singleton_self _)
      · refine mem_union_left _ (mem_filter.2 ⟨mem_univ _, hvS, fun h => ?_⟩)
        exact hv.2 _ h (ha v hvS).2.symm
    have hB : (Pf.biUnion (fun q => ({q.1, q.2} : Finset V))).card ≤ 2 * Pf.card := by
      calc (Pf.biUnion (fun q => ({q.1, q.2} : Finset V))).card
          ≤ ∑ q ∈ Pf, ({q.1, q.2} : Finset V).card := card_biUnion_le
        _ ≤ ∑ _q ∈ Pf, 2 := sum_le_sum fun q _ => (card_insert_le _ _).trans (by simp)
        _ = 2 * Pf.card := by rw [sum_const, smul_eq_mul, mul_comm]
    unfold pdRhs
    calc (und G X).card ≤ (A ∪ Pf.biUnion (fun q => ({q.1, q.2} : Finset V))).card :=
          card_le_card hsub
      _ ≤ A.card + (Pf.biUnion (fun q => ({q.1, q.2} : Finset V))).card := card_union_le _ _
      _ ≤ A.card + 2 * Pf.card := by omega
  refine ⟨h1, fun y hy => ?_⟩
  rw [← Aux.point_factor G S P hP anc ha y, pdW_eq]
  refine sum_le_sum fun X hX => ?_
  apply mul_le_mul_of_nonneg_left _ (pow_nonneg hy _)
  apply Real.rpow_le_rpow_of_exponent_le (by norm_num)
  have := h1 X (mem_powerset.1 hX)
  have : ((und G X).card : ℝ) ≤ (pdRhs S P anc X : ℝ) := by exact_mod_cast this
  linarith

/-- Optional: the factorization in the proof of `lem:fa-pd-point`, an identity for every real `y`. -/
theorem pd_point_factor (G : SimpleGraph V) (S : Finset V)
    (P : Finset (V × V)) (hP : IsPairing G S P) (anc : V → V) (ha : IsAnchor G S anc) (y : ℝ) :
    ∑ X ∈ S.powerset, y ^ X.card * (2:ℝ) ^ (-(pdRhs S P anc X : ℝ))
      = ∏ q ∈ P, Ωpair y (ancDeg S anc q.1) (ancDeg S anc q.2) :=
  Aux.point_factor G S P hP anc ha y

/-- The AM–GM consequence before `lem:fa-pd-rate`, for `y ≥ 0` (false for some `y < 0`):
`Ω_{uv}(y) ≥ y² + 4·2^{-n_{uv}/2}·y + 2^{-n_{uv}}`, the argument of the logarithm in `h_{n_{uv}}`. -/
theorem Ωpair_amgm (y : ℝ) (hy : 0 ≤ y) (du dv : ℕ) :
    y ^ 2 + 4 * (2:ℝ) ^ (-((2 + du + dv : ℕ) : ℝ) / 2) * y + (2:ℝ) ^ (-((2 + du + dv : ℕ) : ℝ))
      ≤ Ωpair y du dv := by
  have hsq : ∀ d : ℕ, (2:ℝ) ^ (-(d:ℝ)) = ((2:ℝ) ^ (-(d:ℝ) / 2)) ^ 2 := by
    intro d
    rw [← Real.rpow_natCast, ← Real.rpow_mul (by norm_num)]
    congr 1; push_cast; ring
  have hsplit : (2:ℝ) ^ (-((2 + du + dv : ℕ) : ℝ) / 2)
      = (2:ℝ) ^ (-1:ℝ) * ((2:ℝ) ^ (-(du:ℝ) / 2) * (2:ℝ) ^ (-(dv:ℝ) / 2)) := by
    rw [← Real.rpow_add (by norm_num), ← Real.rpow_add (by norm_num)]
    congr 1; push_cast; ring
  have hhalf : (2:ℝ) ^ (-1:ℝ) = 1 / 2 := by rw [Real.rpow_neg_one]; norm_num
  unfold Ωpair
  rw [hsplit, hhalf, hsq du, hsq dv]
  nlinarith [mul_nonneg hy (sq_nonneg ((2:ℝ) ^ (-(du:ℝ) / 2) - (2:ℝ) ^ (-(dv:ℝ) / 2)))]

/-- Optional: a graph with a paired dominating set has no isolated vertex. -/
theorem noIsolated_of_pairedDom (G : SimpleGraph V) (S : Finset V) (hS : IsPairedDom G S) :
    ∀ v, ∃ u, G.Adj v u := by
  intro v
  obtain ⟨hdom, M, hMv, hM⟩ := hS
  rcases hdom v with hv | ⟨u, -, hu⟩
  · have hv' : v ∈ M.verts := by rw [hMv]; exact hv
    obtain ⟨w, hw, -⟩ := hM hv'
    exact ⟨w, M.adj_sub hw⟩
  · exact ⟨u, hu⟩

/-- Optional: a graph without isolated vertices has a paired dominating set
(the setting of `thm:fa-pd`). -/
theorem exists_pairedDom (G : SimpleGraph V) (hG : ∀ v, ∃ u, G.Adj v u) :
    ∃ S : Finset V, IsPairedDom G S := by
  classical
  let ends : Finset (V × V) → Finset V := fun P => P.biUnion (fun q => ({q.1, q.2} : Finset V))
  have hends : ∀ P w, w ∈ ends P ↔ ∃ q ∈ P, q.1 = w ∨ q.2 = w := by
    intro P w
    simp only [ends, mem_biUnion, mem_insert, mem_singleton]
    constructor
    · rintro ⟨q, hq, h | h⟩
      · exact ⟨q, hq, Or.inl h.symm⟩
      · exact ⟨q, hq, Or.inr h.symm⟩
    · rintro ⟨q, hq, h | h⟩
      · exact ⟨q, hq, Or.inl h.symm⟩
      · exact ⟨q, hq, Or.inr h.symm⟩
  let C := (univ : Finset (Finset (V × V))).filter (fun P => IsPairing G (ends P) P)
  have hC0 : (∅ : Finset (V × V)) ∈ C := by
    simp only [C, mem_filter, mem_univ, true_and]
    refine ⟨fun q hq => by simp at hq, fun w hw => ?_⟩
    obtain ⟨q, hq, -⟩ := (hends ∅ w).1 hw
    simp at hq
  obtain ⟨P, hPC, hPmax⟩ := C.exists_max_image card ⟨∅, hC0⟩
  have hP : IsPairing G (ends P) P := (mem_filter.1 hPC).2
  refine ⟨ends P, ?_, ?_⟩
  · intro v
    by_cases hv : v ∈ ends P
    · exact Or.inl hv
    · right
      obtain ⟨u, hvu⟩ := hG v
      by_cases hu : u ∈ ends P
      · exact ⟨u, hu, hvu⟩
      · exfalso
        have hnotin : (v, u) ∉ P := fun h => hv ((hends P v).2 ⟨_, h, Or.inl rfl⟩)
        have hP' : IsPairing G (ends (insert (v, u) P)) (insert (v, u) P) := by
          refine ⟨?_, ?_⟩
          · intro q hq
            refine ⟨(hends _ q.1).2 ⟨q, hq, Or.inl rfl⟩, (hends _ q.2).2 ⟨q, hq, Or.inr rfl⟩, ?_⟩
            rcases mem_insert.1 hq with h | h
            · rw [h]; exact hvu
            · exact (hP.1 q h).2.2
          · intro w hw
            obtain ⟨q0, hq0, hq0w⟩ := (hends _ w).1 hw
            refine ⟨q0, ⟨hq0, hq0w⟩, ?_⟩
            rintro q ⟨hq, hqw⟩
            rcases mem_insert.1 hq0 with h0 | h0
            · rcases mem_insert.1 hq with h | h
              · rw [h, h0]
              · exfalso
                rw [h0] at hq0w
                rcases hq0w with h1 | h1
                · rw [← h1] at hqw
                  exact hv ((hends P v).2 ⟨q, h, hqw⟩)
                · rw [← h1] at hqw
                  exact hu ((hends P u).2 ⟨q, h, hqw⟩)
            · rcases mem_insert.1 hq with h | h
              · exfalso
                rw [h] at hqw
                rcases hqw with h1 | h1
                · rw [← h1] at hq0w
                  exact hv ((hends P v).2 ⟨q0, h0, hq0w⟩)
                · rw [← h1] at hq0w
                  exact hu ((hends P u).2 ⟨q0, h0, hq0w⟩)
              · exact hP.eq_of_mem h h0 hqw hq0w
        have hmem : insert (v, u) P ∈ C := by
          simp only [C, mem_filter, mem_univ, true_and]
          exact hP'
        have h1 := hPmax _ hmem
        have h2 := card_lt_card (ssubset_insert hnotin)
        omega
  · obtain ⟨M, hMv, hM, -⟩ := matching_of_pairing G (ends P) P hP
    exact ⟨M, hMv, hM⟩

namespace Aux

/-- One pair: `(1+y*)^m 2^{-ψ_pr m} ≤ y*² + 4·2^{-m/2} y* + 2^{-m}` for `m ≥ 2`
(`PDRate.pd_rate`, first claim of `lem:fa-pd-rate`). -/
theorem pair_bound (m : ℕ) (hm : 2 ≤ m) :
    (1 + ystar) ^ m * (2:ℝ) ^ (-(ωpr * m))
      ≤ ystar ^ 2 + 4 * (2:ℝ) ^ (-(m:ℝ) / 2) * ystar + (2:ℝ) ^ (-(m:ℝ)) := by
  have hy := ystar_pos
  set A := ystar ^ 2 + 4 * (2:ℝ) ^ (-(m:ℝ) / 2) * ystar + (2:ℝ) ^ (-(m:ℝ)) with hA
  have hA0 : 0 < A := by
    have h1 : 0 < (2:ℝ) ^ (-(m:ℝ)) := by positivity
    have h2 : 0 ≤ 4 * (2:ℝ) ^ (-(m:ℝ) / 2) * ystar := by positivity
    have h3 : 0 ≤ ystar ^ 2 := sq_nonneg _
    linarith
  have h1 := pd_rate.1 m hm
  unfold hpd at h1
  rw [← hA] at h1
  have hm0 : (0:ℝ) < m := by exact_mod_cast (show 0 < m by omega)
  have h2 : Real.logb 2 (1 + ystar) - ωpr ≤ (1 / (m:ℝ)) * Real.logb 2 A := by linarith
  have h3 : Real.logb 2 (1 + ystar) * m + -(ωpr * m) ≤ Real.logb 2 A := by
    calc Real.logb 2 (1 + ystar) * m + -(ωpr * m)
        = (m:ℝ) * (Real.logb 2 (1 + ystar) - ωpr) := by ring
      _ ≤ (m:ℝ) * ((1 / (m:ℝ)) * Real.logb 2 A) := mul_le_mul_of_nonneg_left h2 hm0.le
      _ = Real.logb 2 A := by field_simp
  have hL : (2:ℝ) ^ (Real.logb 2 (1 + ystar) * m) = (1 + ystar) ^ m := by
    rw [Real.rpow_mul (by norm_num), Real.rpow_logb (by norm_num) (by norm_num) (by linarith),
      Real.rpow_natCast]
  calc (1 + ystar) ^ m * (2:ℝ) ^ (-(ωpr * m))
      = (2:ℝ) ^ (Real.logb 2 (1 + ystar) * m + -(ωpr * m)) := by
        rw [Real.rpow_add (by norm_num), hL]
    _ ≤ (2:ℝ) ^ (Real.logb 2 A) := Real.rpow_le_rpow_of_exponent_le (by norm_num) h3
    _ = A := Real.rpow_logb (by norm_num) (by norm_num) hA0

end Aux

/-- `lem:fa-pd-rate`, second claim. The hypothesis `hG` (no isolated vertex) is the paper's,
kept literally; it follows from `hS` by `noIsolated_of_pairedDom`. -/
theorem pd_rate_W (G : SimpleGraph V) [DecidableRel G.Adj] (hG : ∀ v, ∃ u, G.Adj v u)
    (S : Finset V) (hS : IsPairedDom G S) :
    (1 + ystar) ^ Fintype.card V * (2:ℝ) ^ (-(ωpr * Fintype.card V)) ≤ pdW G S ystar := by
  obtain ⟨hdom, M, hMv, hM⟩ := hS
  obtain ⟨P, hP, -⟩ := pairing_of_matching G S M hMv hM
  obtain ⟨anc, ha⟩ := exists_anchor G S hdom
  have hy0 : 0 ≤ ystar := Aux.ystar_pos.le
  set c : ℝ := (1 + ystar) * (2:ℝ) ^ (-ωpr) with hcdef
  have hc0 : 0 ≤ c := mul_nonneg (by linarith) (Real.rpow_nonneg (by norm_num) _)
  have hc : ∀ m : ℕ, (1 + ystar) ^ m * (2:ℝ) ^ (-(ωpr * m)) = c ^ m := by
    intro m
    rw [hcdef, mul_pow, ← Real.rpow_natCast ((2:ℝ) ^ (-ωpr)), ← Real.rpow_mul (by norm_num),
      show -(ωpr * (m:ℝ)) = -ωpr * m by ring]
  have hcard := card_eq_sum_pairs G S P hP anc ha
  calc (1 + ystar) ^ Fintype.card V * (2:ℝ) ^ (-(ωpr * Fintype.card V))
      = c ^ Fintype.card V := hc _
    _ = ∏ q ∈ P, c ^ (2 + ancDeg S anc q.1 + ancDeg S anc q.2) := by
        rw [prod_pow_eq_pow_sum, ← hcard]
    _ ≤ ∏ q ∈ P, Ωpair ystar (ancDeg S anc q.1) (ancDeg S anc q.2) := by
        apply prod_le_prod₀ (fun q _ => pow_nonneg hc0 _)
        intro q _
        rw [← hc]
        exact (Aux.pair_bound _ (by omega)).trans (Ωpair_amgm ystar hy0 _ _)
    _ ≤ pdW G S ystar := (pd_point G S P hP anc ha).2 ystar hy0

/-- Optional: condition (⋆) of `thm:fw-main` at rate 0.70502 and `Γ = 1`
(proof of `thm:fa-pd`). -/
theorem pd_star (G : SimpleGraph V) [DecidableRel G.Adj] (S : Finset V) (hS : IsPairedDom G S) :
    MLS.Star (pdG G) S S.card (70502 / 10 ^ 5) 1 := by
  have hW := pd_rate_W G (noIsolated_of_pairedDom G S hS) S hS
  have hy0 : 0 ≤ ystar := Aux.ystar_pos.le
  apply MLS.star_of_W (pdG G) S S.card rfl _ 1 ystar one_pos hy0
  rw [div_one]
  refine le_trans ?_ hW
  apply mul_le_mul_of_nonneg_left _ (pow_nonneg (by linarith) _)
  apply Real.rpow_le_rpow_of_exponent_le (by norm_num)
  have h1 := pd_constants.2.2.1
  have hn : (0:ℝ) ≤ Fintype.card V := Nat.cast_nonneg _
  nlinarith

/-- Optional: success probability of MLS at rate 0.70502, `Γ = 1`, for `k = |S|`,
with the extension algorithm replaced by its specification `ExtYes`. -/
theorem pd_success (G : SimpleGraph V) [DecidableRel G.Adj] (S : Finset V) (hS : IsPairedDom G S)
    (κ : ℝ) (hκ : 0 < κ) :
    1 - Real.exp (-κ) ≤
      (trialMeasure S.card (70502 / 10 ^ 5) 1 κ
        {o | Accepts (IsPairedDom G) (pdG G) S.card (70502 / 10 ^ 5) 1 κ o}).toReal :=
  MLS.mls_success (IsPairedDom G) (pdG G) (fun _ _ => Nat.cast_nonneg _) S.card (card_le_univ S)
    (70502 / 10 ^ 5) 1 κ (by norm_num) le_rfl hκ S hS rfl (pd_star G S hS)

end General

section Tight

/-- Edges of one double star: centres 0, 1; pendants 2, 3 at 0 and 4, 5 at 1. -/
def dsEdge (a b : Fin 6) : Prop :=
  (a = 0 ∧ (b = 1 ∨ b = 2 ∨ b = 3)) ∨ (a = 1 ∧ (b = 4 ∨ b = 5))

instance instDecidableRelDsEdge : DecidableRel dsEdge := fun a b => by unfold dsEdge; infer_instance

/-- `G_L`: the disjoint union of `L` double stars. (Not `GL`, which is Mathlib notation.) -/
def dstarGraph (L : ℕ) : SimpleGraph (Fin L × Fin 6) :=
  SimpleGraph.fromRel fun p q => p.1 = q.1 ∧ dsEdge p.2 q.2

/-- Needed although Mathlib has `DecidableRel (SimpleGraph.fromRel r).Adj`: instance search
does not unfold the definition `dstarGraph`. `inferInstanceAs` is an allowed form. -/
instance instDecidableRelDstarGraph (L : ℕ) : DecidableRel (dstarGraph L).Adj := fun p q =>
  decidable_of_iff (p ≠ q ∧ ((p.1 = q.1 ∧ dsEdge p.2 q.2) ∨ (q.1 = p.1 ∧ dsEdge q.2 p.2)))
    (SimpleGraph.fromRel_adj (fun p q : Fin L × Fin 6 => p.1 = q.1 ∧ dsEdge p.2 q.2) p q).symm

/-- `S*`, the `2L` centres. -/
def Sstar (L : ℕ) : Finset (Fin L × Fin 6) := univ ×ˢ ({0, 1} : Finset (Fin 6))

namespace Aux

theorem dsE01 : dsEdge 0 1 := by decide

theorem dsEdge_irrefl : ∀ a : Fin 6, ¬ dsEdge a a := by decide

theorem dsCover : ∀ r : Fin 6, r = 0 ∨ r = 1 ∨ dsEdge 0 r ∨ dsEdge 1 r := by decide

theorem dsPend2 : ∀ x : Fin 6, (dsEdge 2 x ∨ dsEdge x 2) ↔ x = 0 := by decide

theorem dsPend4 : ∀ x : Fin 6, (dsEdge 4 x ∨ dsEdge x 4) ↔ x = 1 := by decide

theorem dsAdj_iff (L : ℕ) (p q : Fin L × Fin 6) :
    (dstarGraph L).Adj p q ↔ p.1 = q.1 ∧ (dsEdge p.2 q.2 ∨ dsEdge q.2 p.2) := by
  unfold dstarGraph
  rw [SimpleGraph.fromRel_adj]
  constructor
  · rintro ⟨_, h | h⟩
    · exact ⟨h.1, Or.inl h.2⟩
    · exact ⟨h.1.symm, Or.inr h.2⟩
  · rintro ⟨h1, h | h⟩
    · refine ⟨fun heq => ?_, Or.inl ⟨h1, h⟩⟩
      subst heq
      exact dsEdge_irrefl _ h
    · refine ⟨fun heq => ?_, Or.inr ⟨h1.symm, h⟩⟩
      subst heq
      exact dsEdge_irrefl _ h

theorem pend_adj_two {L : ℕ} (i : Fin L) (w : Fin L × Fin 6)
    (h : (dstarGraph L).Adj (i, 2) w) : w = (i, 0) := by
  rw [dsAdj_iff] at h
  obtain ⟨h1, h2⟩ := h
  have h3 : w.2 = 0 := (dsPend2 w.2).1 h2
  exact Prod.ext h1.symm h3

theorem pend_adj_four {L : ℕ} (i : Fin L) (w : Fin L × Fin 6)
    (h : (dstarGraph L).Adj (i, 4) w) : w = (i, 1) := by
  rw [dsAdj_iff] at h
  obtain ⟨h1, h2⟩ := h
  have h3 : w.2 = 1 := (dsPend4 w.2).1 h2
  exact Prod.ext h1.symm h3

theorem Sstar_mem_iff {L : ℕ} (p : Fin L × Fin 6) : p ∈ Sstar L ↔ p.2 = 0 ∨ p.2 = 1 := by
  simp [Sstar, Finset.mem_product]

theorem card_Sstar (L : ℕ) : (Sstar L).card = 2 * L := by
  unfold Sstar
  rw [Finset.card_product, Finset.card_univ, Fintype.card_fin]
  have h2 : ({0, 1} : Finset (Fin 6)).card = 2 := by decide
  rw [h2]
  ring

theorem mem_of_pendant {L : ℕ} (S : Finset (Fin L × Fin 6)) (hS : IsPairedDom (dstarGraph L) S)
    (p c : Fin L × Fin 6) (hpc : ∀ w, (dstarGraph L).Adj p w → w = c) : c ∈ S := by
  unfold IsPairedDom IsDominating at hS
  obtain ⟨hdom, M, hMv, hMm⟩ := hS
  by_cases hp : p ∈ S
  · have hpM : p ∈ M.verts := by
      rw [hMv]
      exact Finset.mem_coe.2 hp
    obtain ⟨w, hw, -⟩ := hMm hpM
    have hwc : w = c := hpc w (M.adj_sub hw)
    have hwp : M.Adj w p := by
      exact M.symm.symm _ _ hw
    have hwM : w ∈ M.verts := M.edge_vert hwp
    rw [hMv] at hwM
    rw [← hwc]
    exact Finset.mem_coe.1 hwM
  · rcases hdom p with h | ⟨u, hu, hadj⟩
    · exact absurd h hp
    · have huc : u = c := hpc u hadj
      rw [← huc]
      exact hu

theorem dom_Sstar (L : ℕ) : IsDominating (dstarGraph L) (Sstar L) := by
  unfold IsDominating
  rintro ⟨i, r⟩
  rcases dsCover r with h | h | h | h
  · exact Or.inl ((Sstar_mem_iff (i, r)).2 (Or.inl h))
  · exact Or.inl ((Sstar_mem_iff (i, r)).2 (Or.inr h))
  · exact Or.inr ⟨(i, 0), (Sstar_mem_iff (i, 0)).2 (Or.inl rfl),
      (dsAdj_iff L (i, r) (i, 0)).2 ⟨rfl, Or.inr h⟩⟩
  · exact Or.inr ⟨(i, 1), (Sstar_mem_iff (i, 1)).2 (Or.inr rfl),
      (dsAdj_iff L (i, r) (i, 1)).2 ⟨rfl, Or.inr h⟩⟩

theorem exists_matching (L : ℕ) :
    ∃ M : (dstarGraph L).Subgraph, M.verts = (Sstar L : Set (Fin L × Fin 6)) ∧ M.IsMatching := by
  have hadj : ∀ p q : Fin L × Fin 6,
      (p.1 = q.1 ∧ ((p.2 = 0 ∧ q.2 = 1) ∨ (p.2 = 1 ∧ q.2 = 0))) → (dstarGraph L).Adj p q := by
    rintro p q ⟨h1, h2 | h2⟩
    · exact (dsAdj_iff L p q).2 ⟨h1, Or.inl (by rw [h2.1, h2.2]; exact dsE01)⟩
    · exact (dsAdj_iff L p q).2 ⟨h1, Or.inr (by rw [h2.1, h2.2]; exact dsE01)⟩
  have hvert : ∀ p q : Fin L × Fin 6,
      (p.1 = q.1 ∧ ((p.2 = 0 ∧ q.2 = 1) ∨ (p.2 = 1 ∧ q.2 = 0))) →
        p ∈ (Sstar L : Set (Fin L × Fin 6)) := by
    rintro p q ⟨_, h2 | h2⟩
    · exact Finset.mem_coe.2 ((Sstar_mem_iff p).2 (Or.inl h2.1))
    · exact Finset.mem_coe.2 ((Sstar_mem_iff p).2 (Or.inr h2.1))
  refine ⟨{ verts := (Sstar L : Set (Fin L × Fin 6)),
            Adj := fun p q => p.1 = q.1 ∧ ((p.2 = 0 ∧ q.2 = 1) ∨ (p.2 = 1 ∧ q.2 = 0)),
            adj_sub := by
              intro v w h
              exact hadj v w h,
            edge_vert := by
              intro v w h
              exact hvert v w h,
            symm := ⟨by
              intro v w h
              obtain ⟨h1, h2 | h2⟩ := h
              · exact ⟨h1.symm, Or.inr ⟨h2.2, h2.1⟩⟩
              · exact ⟨h1.symm, Or.inl ⟨h2.2, h2.1⟩⟩⟩ }, rfl, ?_⟩
  intro v hv
  have hv' : v.2 = 0 ∨ v.2 = 1 := (Sstar_mem_iff v).1 (Finset.mem_coe.1 hv)
  rcases hv' with h | h
  · refine ⟨(v.1, 1), ⟨rfl, Or.inl ⟨h, rfl⟩⟩, ?_⟩
    rintro w ⟨h1, h2 | h2⟩
    · exact Prod.ext h1.symm h2.2
    · exact absurd (h.symm.trans h2.1) (by decide)
  · refine ⟨(v.1, 0), ⟨rfl, Or.inr ⟨h, rfl⟩⟩, ?_⟩
    rintro w ⟨h1, h2 | h2⟩
    · exact absurd (h.symm.trans h2.1) (by decide)
    · exact Prod.ext h1.symm h2.2

end Aux

theorem dstarGraph_noIsolated (L : ℕ) : ∀ v, ∃ u, (dstarGraph L).Adj v u := by
  rintro ⟨i, r⟩
  rcases Aux.dsCover r with h | h | h | h
  · subst h
    exact ⟨(i, 1), (Aux.dsAdj_iff L (i, 0) (i, 1)).2 ⟨rfl, Or.inl Aux.dsE01⟩⟩
  · subst h
    exact ⟨(i, 0), (Aux.dsAdj_iff L (i, 1) (i, 0)).2 ⟨rfl, Or.inr Aux.dsE01⟩⟩
  · exact ⟨(i, 0), (Aux.dsAdj_iff L (i, r) (i, 0)).2 ⟨rfl, Or.inr h⟩⟩
  · exact ⟨(i, 1), (Aux.dsAdj_iff L (i, r) (i, 1)).2 ⟨rfl, Or.inr h⟩⟩

/-- The proof's stronger claim: every paired dominating set contains all centres. -/
theorem Sstar_subset (L : ℕ) (S : Finset (Fin L × Fin 6)) (hS : IsPairedDom (dstarGraph L) S) :
    Sstar L ⊆ S := by
  rintro ⟨i, r⟩ hv
  rcases (Aux.Sstar_mem_iff (i, r)).1 hv with h | h
  · obtain rfl : r = 0 := h
    exact Aux.mem_of_pendant S hS (i, 2) (i, 0) (fun w hw => Aux.pend_adj_two i w hw)
  · obtain rfl : r = 1 := h
    exact Aux.mem_of_pendant S hS (i, 4) (i, 1) (fun w hw => Aux.pend_adj_four i w hw)

/-- `prop:fa-pd-tight`, graph part. -/
theorem pd_tight_unique (L : ℕ) :
    IsPairedDom (dstarGraph L) (Sstar L) ∧ (Sstar L).card = 2 * L ∧
    ∀ S : Finset (Fin L × Fin 6), IsPairedDom (dstarGraph L) S → S.card ≤ 2 * L → S = Sstar L := by
  refine ⟨?_, Aux.card_Sstar L, ?_⟩
  · unfold IsPairedDom
    exact ⟨Aux.dom_Sstar L, Aux.exists_matching L⟩
  · intro S hS hcard
    have hsub := Sstar_subset L S hS
    refine (Finset.eq_of_subset_of_card_le hsub ?_).symm
    rw [Aux.card_Sstar]
    exact hcard

namespace Aux

/-- Anchors at the centres of the double stars. -/
def ctrAnc (L : ℕ) (p : Fin L × Fin 6) : Fin L × Fin 6 := (p.1, if p.2.val ≤ 3 then 0 else 1)

/-- The pairs `u_i v_i` of the centres. -/
def ctrPairs (L : ℕ) : Finset ((Fin L × Fin 6) × (Fin L × Fin 6)) :=
  univ.image (fun i : Fin L => ((i, 0), (i, 1)))

theorem ds_pend_eq : ∀ a b : Fin 6, ¬ (b = 0 ∨ b = 1) → (dsEdge a b ∨ dsEdge b a) →
    a = (if b.val ≤ 3 then 0 else 1) := by decide

theorem ds_anc_edge : ∀ b : Fin 6, ¬ (b = 0 ∨ b = 1) → dsEdge (if b.val ≤ 3 then 0 else 1) b := by
  decide

theorem ctr_pairing (L : ℕ) : IsPairing (dstarGraph L) (Sstar L) (ctrPairs L) := by
  have hmem : ∀ q, q ∈ ctrPairs L ↔ ∃ i : Fin L, ((i, 0), (i, 1)) = q := by
    intro q; simp [ctrPairs]
  refine ⟨?_, ?_⟩
  · intro q hq
    obtain ⟨i, rfl⟩ := (hmem q).1 hq
    exact ⟨(Sstar_mem_iff _).2 (Or.inl rfl), (Sstar_mem_iff _).2 (Or.inr rfl),
      (dsAdj_iff L _ _).2 ⟨rfl, Or.inl dsE01⟩⟩
  · rintro ⟨i, c⟩ hw
    have hc := (Sstar_mem_iff (i, c)).1 hw
    refine ⟨((i, 0), (i, 1)), ⟨(hmem _).2 ⟨i, rfl⟩, ?_⟩, ?_⟩
    · rcases hc with h | h
      · exact Or.inl (Prod.ext rfl h.symm)
      · exact Or.inr (Prod.ext rfl h.symm)
    · rintro q ⟨hq, hqw⟩
      obtain ⟨j, rfl⟩ := (hmem q).1 hq
      have : j = i := by rcases hqw with h | h <;> exact congrArg Prod.fst h
      rw [this]

theorem ctr_anchor (L : ℕ) : IsAnchor (dstarGraph L) (Sstar L) (ctrAnc L) := by
  rintro ⟨i, b⟩ hv
  have hb : ¬ (b = 0 ∨ b = 1) := fun h => hv ((Sstar_mem_iff (i, b)).2 h)
  refine ⟨(Sstar_mem_iff _).2 ?_, (dsAdj_iff L _ _).2 ⟨rfl, Or.inr (ds_anc_edge b hb)⟩⟩
  simp only [ctrAnc]
  split_ifs <;> simp

theorem ctr_deg (L : ℕ) (i : Fin L) (c : Fin 6) (hc : c = 0 ∨ c = 1) :
    ancDeg (Sstar L) (ctrAnc L) (i, c) = 2 := by
  unfold ancDeg
  have h : (univ.filter (fun v : Fin L × Fin 6 => v ∉ Sstar L ∧ ctrAnc L v = (i, c)))
      = (univ.filter (fun x : Fin 6 => ¬ (x = 0 ∨ x = 1) ∧
          (if x.val ≤ 3 then (0 : Fin 6) else 1) = c)).image (fun x => (i, x)) := by
    ext ⟨j, x⟩
    simp only [mem_filter, mem_univ, true_and, mem_image, Sstar_mem_iff, ctrAnc, Prod.mk.injEq]
    constructor
    · rintro ⟨h1, h2, h3⟩; exact ⟨x, ⟨h1, h3⟩, h2.symm, rfl⟩
    · rintro ⟨y, ⟨h1, h3⟩, rfl, rfl⟩; exact ⟨h1, rfl, h3⟩
  rw [h, card_image_of_injective _ (fun a b hab => (Prod.ext_iff.1 hab).2)]
  rcases hc with rfl | rfl <;> decide

theorem card_ctrPairs (L : ℕ) : (ctrPairs L).card = L := by
  unfold ctrPairs
  rw [card_image_of_injective _ (fun a b h => congrArg Prod.fst (congrArg Prod.fst h)), card_univ,
    Fintype.card_fin]

/-- With anchors at the centres, the first inequality of `lem:fa-pd-point` is an equality. -/
theorem und_eq (L : ℕ) (X : Finset (Fin L × Fin 6)) (hX : X ⊆ Sstar L) :
    (und (dstarGraph L) X).card = pdRhs (Sstar L) (ctrPairs L) (ctrAnc L) X := by
  apply le_antisymm ((pd_point _ _ _ (ctr_pairing L) _ (ctr_anchor L)).1 X hX)
  set A := univ.filter (fun v => v ∉ Sstar L ∧ ctrAnc L v ∉ X) with hA
  set Pf := (ctrPairs L).filter (fun q => q.1 ∉ X ∧ q.2 ∉ X) with hPf
  set E := Pf.biUnion (fun q => ({q.1, q.2} : Finset (Fin L × Fin 6))) with hE
  have hP := ctr_pairing L
  have hEc : E.card = 2 * Pf.card := by
    rw [hE, card_biUnion]
    · rw [sum_congr rfl (fun q hq => card_pair (hP.fst_ne_snd (mem_filter.1 hq).1)), sum_const,
        smul_eq_mul, mul_comm]
    · intro q hq q' hq' hne
      simp only [Function.onFun]
      rw [Finset.disjoint_left]
      intro w hw hw'
      simp only [mem_insert, mem_singleton] at hw hw'
      exact hne (hP.eq_of_mem (mem_filter.1 hq).1 (mem_filter.1 hq').1
        (by rcases hw with h | h <;> [left; right] <;> exact h.symm)
        (by rcases hw' with h | h <;> [left; right] <;> exact h.symm))
  have hdis : Disjoint A E := by
    rw [Finset.disjoint_left]
    intro v hvA hvE
    have h1 := (mem_filter.1 hvA).2.1
    obtain ⟨q, hq, hvq⟩ := mem_biUnion.1 hvE
    have := hP.1 q (mem_filter.1 hq).1
    simp only [mem_insert, mem_singleton] at hvq
    rcases hvq with h | h
    · rw [h] at h1; exact h1 this.1
    · rw [h] at h1; exact h1 this.2.1
  have hsub : A ∪ E ⊆ und (dstarGraph L) X := by
    intro v hv
    simp only [und, mem_sdiff, mem_univ, true_and, CDS.mem_closedNbhd, not_or, not_exists,
      not_and]
    rcases mem_union.1 hv with hvA | hvE
    · obtain ⟨hvS, hanc⟩ := (mem_filter.1 hvA).2
      refine ⟨fun h => hvS (hX h), fun x hx hadj => hanc ?_⟩
      have hb : ¬ (v.2 = 0 ∨ v.2 = 1) := fun h => hvS ((Sstar_mem_iff v).2 h)
      obtain ⟨h1, h2⟩ := (dsAdj_iff L x v).1 hadj
      have hx2 := ds_pend_eq x.2 v.2 hb h2
      have : x = ctrAnc L v := Prod.ext h1 hx2
      rw [← this]; exact hx
    · obtain ⟨q, hq, hvq⟩ := mem_biUnion.1 hvE
      obtain ⟨hqP, hq1, hq2⟩ := mem_filter.1 hq
      obtain ⟨i, -, rfl⟩ := mem_image.1 hqP
      simp only [mem_insert, mem_singleton] at hvq
      refine ⟨by rcases hvq with h | h <;> rw [h] <;> assumption, fun x hx hadj => ?_⟩
      have hx2 := (Sstar_mem_iff x).1 (hX hx)
      have hx1 : x.1 = i := by
        have := ((dsAdj_iff L x v).1 hadj).1
        rcases hvq with h | h <;> rw [h] at this <;> exact this
      rcases hx2 with h | h
      · have : x = (i, 0) := Prod.ext hx1 h
        rw [this] at hx; exact hq1 hx
      · have : x = (i, 1) := Prod.ext hx1 h
        rw [this] at hx; exact hq2 hx
  calc pdRhs (Sstar L) (ctrPairs L) (ctrAnc L) X = A.card + 2 * Pf.card := rfl
    _ = (A ∪ E).card := by rw [card_union_of_disjoint hdis, hEc]
    _ ≤ (und (dstarGraph L) X).card := card_le_card hsub

end Aux

/-- `W_{S*}(y) = (y² + y/2 + 1/64)^L` (proof of `prop:fa-pd-tight`). -/
theorem pd_tight_W (L : ℕ) (y : ℝ) :
    pdW (dstarGraph L) (Sstar L) y = (y ^ 2 + y / 2 + 1 / 64) ^ L := by
  have hP := Aux.ctr_pairing L
  have ha := Aux.ctr_anchor L
  rw [pdW_eq]
  have h1 : ∑ X ∈ (Sstar L).powerset, y ^ X.card * (2:ℝ) ^ (-((und (dstarGraph L) X).card : ℝ))
      = ∑ X ∈ (Sstar L).powerset,
          y ^ X.card * (2:ℝ) ^ (-(pdRhs (Sstar L) (Aux.ctrPairs L) (Aux.ctrAnc L) X : ℝ)) :=
    sum_congr rfl fun X hX => by rw [Aux.und_eq L X (mem_powerset.1 hX)]
  rw [h1, pd_point_factor _ _ _ hP _ ha]
  have h2 : ∀ q ∈ Aux.ctrPairs L, Ωpair y (ancDeg (Sstar L) (Aux.ctrAnc L) q.1)
      (ancDeg (Sstar L) (Aux.ctrAnc L) q.2) = y ^ 2 + y / 2 + 1 / 64 := by
    intro q hq
    obtain ⟨i, -, rfl⟩ := mem_image.1 hq
    show Ωpair y (ancDeg (Sstar L) (Aux.ctrAnc L) (i, 0)) (ancDeg (Sstar L) (Aux.ctrAnc L) (i, 1))
      = _
    rw [Aux.ctr_deg L i 0 (Or.inl rfl), Aux.ctr_deg L i 1 (Or.inr rfl)]
    unfold Ωpair
    simp only [Aux.two_rpow_neg_nat]
    ring
  rw [prod_congr rfl h2, prod_const, Aux.card_ctrPairs]

theorem hpd6_eq (y : ℝ) :
    hpd 6 y = Real.logb 2 (1 + y) - (1 / 6) * Real.logb 2 (y ^ 2 + y / 2 + 1 / 64) := by
  have h1 : (2:ℝ) ^ (-(6:ℝ) / 2) = 1 / 8 := by
    rw [show -(6:ℝ) / 2 = ((-3 : ℤ) : ℝ) by norm_num, Real.rpow_intCast]
    norm_num
  have h2 : (2:ℝ) ^ (-(6:ℝ)) = 1 / 64 := by
    rw [show -(6:ℝ) = ((-6 : ℤ) : ℝ) by norm_num, Real.rpow_intCast]
    norm_num
  unfold hpd
  rw [h1, h2, show y ^ 2 + 4 * (1 / 8) * y + 1 / 64 = y ^ 2 + y / 2 + 1 / 64 by ring]

namespace Aux

theorem hpd6_fun : hpd 6 = fun y : ℝ => Real.logb 2 (1 + y) - (1 / 6) * Real.logb 2 (y ^ 2 + y / 2 + 1 / 64) :=
  funext hpd6_eq

theorem hpd6_cont : ContinuousOn (hpd 6) (Set.Ici 0) := by
  rw [hpd6_fun]
  have hL1 : ContinuousOn (fun x : ℝ => Real.log (1 + x)) (Set.Ici 0) :=
    ContinuousOn.log (by fun_prop) (fun x hx => by
      have hx' : (0:ℝ) ≤ x := hx
      exact (show (0:ℝ) < 1 + x by linarith).ne')
  have hL2 : ContinuousOn (fun x : ℝ => Real.log (x ^ 2 + x / 2 + 1 / 64)) (Set.Ici 0) :=
    ContinuousOn.log (by fun_prop) (fun x hx => by
      have hx' : (0:ℝ) ≤ x := hx
      have := sq_nonneg x
      exact (show (0:ℝ) < x ^ 2 + x / 2 + 1 / 64 by linarith).ne')
  exact (hL1.div_const (Real.log 2)).sub (continuousOn_const.mul (hL2.div_const (Real.log 2)))

theorem den_pos (y : ℝ) (hy : 0 < y) :
    0 < Real.log 2 * (6 * (y ^ 2 + y / 2 + 1 / 64) * (1 + y)) := by
  have hQ0 : 0 < y ^ 2 + y / 2 + 1 / 64 := by
    have := sq_nonneg y
    linarith
  exact mul_pos (Real.log_pos one_lt_two) (mul_pos (mul_pos (by norm_num) hQ0) (by linarith))

theorem hasDeriv_pos (y : ℝ) (hy : 0 < y) :
    HasDerivAt (hpd 6) ((4 * y ^ 2 + y / 2 - 13 / 32) /
      (Real.log 2 * (6 * (y ^ 2 + y / 2 + 1 / 64) * (1 + y)))) y := by
  have hQ0 : 0 < y ^ 2 + y / 2 + 1 / 64 := by
    have := sq_nonneg y
    linarith
  have hP0 : (0:ℝ) < 1 + y := by linarith
  have hlog2 : 0 < Real.log 2 := Real.log_pos one_lt_two
  have hQne : y ^ 2 + y / 2 + 1 / 64 ≠ 0 := hQ0.ne'
  have hPne : (1:ℝ) + y ≠ 0 := hP0.ne'
  have hlne : Real.log 2 ≠ 0 := hlog2.ne'
  have hA : HasDerivAt (fun x : ℝ => Real.log (1 + x)) (1 / (1 + y)) y :=
    ((hasDerivAt_id' y).const_add 1).log hPne
  have hQ : HasDerivAt (fun x : ℝ => x ^ 2 + x / 2 + 1 / 64) (2 * y + 1 / 2) y :=
    (((hasDerivAt_pow 2 y).add ((hasDerivAt_id' y).div_const 2)).add_const (1 / 64 : ℝ)).congr_deriv
      (by norm_num)
  have hB : HasDerivAt (fun x : ℝ => Real.log (x ^ 2 + x / 2 + 1 / 64))
      ((2 * y + 1 / 2) / (y ^ 2 + y / 2 + 1 / 64)) y :=
    hQ.log hQne
  have hC := (hA.div_const (Real.log 2)).sub ((hB.div_const (Real.log 2)).const_mul (1 / 6 : ℝ))
  have hkey : 1 / (1 + y) / Real.log 2
      - 1 / 6 * ((2 * y + 1 / 2) / (y ^ 2 + y / 2 + 1 / 64) / Real.log 2)
      = (4 * y ^ 2 + y / 2 - 13 / 32) / (Real.log 2 * (6 * (y ^ 2 + y / 2 + 1 / 64) * (1 + y))) := by
    field_simp
    ring
  rw [hpd6_fun]
  exact hC.congr_deriv hkey

theorem hpd6_anti : StrictAntiOn (hpd 6) (Set.Icc 0 ystar) := by
  apply strictAntiOn_of_deriv_neg (convex_Icc 0 ystar) (hpd6_cont.mono Set.Icc_subset_Ici_self)
  intro τ hτ
  rw [interior_Icc] at hτ
  rw [(hasDeriv_pos τ hτ.1).deriv]
  apply div_neg_of_neg_of_pos
  · rw [N_factor τ]
    exact mul_neg_of_neg_of_pos (mul_neg_of_pos_of_neg (by norm_num) (by linarith [hτ.2]))
      (by linarith [Real.sqrt_nonneg 3, hτ.1])
  · exact den_pos τ hτ.1

theorem hpd6_mono : StrictMonoOn (hpd 6) (Set.Ici ystar) := by
  apply strictMonoOn_of_deriv_pos (convex_Ici ystar)
    (hpd6_cont.mono (Set.Ici_subset_Ici.mpr ystar_pos.le))
  intro τ hτ
  rw [interior_Ici] at hτ
  have hτ' : ystar < τ := hτ
  have hτ0 : 0 < τ := lt_trans ystar_pos hτ'
  rw [(hasDeriv_pos τ hτ0).deriv]
  apply div_pos
  · rw [N_factor τ]
    exact mul_pos (mul_pos (by norm_num) (by linarith)) (by linarith [Real.sqrt_nonneg 3])
  · exact den_pos τ hτ0

theorem argmin_strict (y : ℝ) (hy : 0 ≤ y) (hne : y ≠ ystar) : ωpr < hpd 6 y := by
  unfold ωpr
  rcases lt_or_gt_of_ne hne with hlt | hgt
  · exact hpd6_anti ⟨hy, hlt.le⟩ ⟨ystar_pos.le, le_rfl⟩ hlt
  · exact hpd6_mono (Set.mem_Ici.mpr le_rfl) (Set.mem_Ici.mpr hgt.le) hgt

end Aux

/-- `prop:fa-pd-tight`, first sentence, critical point. -/
theorem pd_tight_crit :
    0 < ystar ∧
    (∀ y : ℝ, 0 < y → DifferentiableAt ℝ (hpd 6) y) ∧
    ∀ y : ℝ, 0 < y → (deriv (hpd 6) y = 0 ↔ y = ystar) := by
  refine ⟨Aux.ystar_pos, fun y hy => (Aux.hasDeriv_pos y hy).differentiableAt, fun y hy => ?_⟩
  rw [(Aux.hasDeriv_pos y hy).deriv]
  constructor
  · intro h
    rcases div_eq_zero_iff.mp h with h1 | h1
    · have h2 : 4 * (y - ystar) * (y - (-1 - 3 * Real.sqrt 3) / 16) = 0 := by
        rw [← Aux.N_factor y]
        exact h1
      rcases mul_eq_zero.mp h2 with h3 | h3
      · rcases mul_eq_zero.mp h3 with h4 | h4
        · norm_num at h4
        · linarith
      · exfalso
        linarith [Real.sqrt_nonneg 3]
    · exact absurd h1 (Aux.den_pos y hy).ne'
  · intro h
    have hN : 4 * ystar ^ 2 + ystar / 2 - 13 / 32 = 0 := by
      unfold ystar
      linear_combination (9 / 64 : ℝ) * Aux.sqrt3_sq
    rw [h, hN, zero_div]

/-- `prop:fa-pd-tight`, first sentence, minimum: `min_{y ≥ 0} h_6(y) = h_6(y*)`. -/
theorem pd_tight_min : 0 ≤ ystar ∧ ∀ y : ℝ, 0 ≤ y → ωpr ≤ hpd 6 y := by
  refine ⟨Aux.ystar_pos.le, fun y hy => ?_⟩
  by_cases h : y = ystar
  · subst h
    unfold ωpr
    exact le_rfl
  · exact (Aux.argmin_strict y hy h).le

/-- Optional: `y*` is the only minimizer of `h_6` on `[0, ∞)`. -/
theorem pd_tight_argmin : ∀ y : ℝ, 0 ≤ y → y ≠ ystar → ωpr < hpd 6 y := by
  intro y hy hne
  exact Aux.argmin_strict y hy hne

/-- `(1+y)^n / W_{S*}(y) = 2^{n h_6(y)}` with `n = 6L`. -/
theorem pd_tight_ratio (L : ℕ) (y : ℝ) (hy : 0 ≤ y) :
    (1 + y) ^ (6 * L) = (2:ℝ) ^ (((6 * L : ℕ) : ℝ) * hpd 6 y) * pdW (dstarGraph L) (Sstar L) y := by
  set Q := y ^ 2 + y / 2 + 1 / 64 with hQ
  have hQ0 : 0 < Q := by have := sq_nonneg y; linarith
  have hP0 : 0 < 1 + y := by linarith
  rw [pd_tight_W, hpd6_eq, ← hQ]
  have e : ((6 * L : ℕ) : ℝ) * (Real.logb 2 (1 + y) - 1 / 6 * Real.logb 2 Q)
      = Real.logb 2 (1 + y) * ((6 * L : ℕ) : ℝ) + -(Real.logb 2 Q * (L : ℝ)) := by
    push_cast; ring
  rw [e, Real.rpow_add (by norm_num), Real.rpow_neg (by norm_num), Real.rpow_mul (by norm_num),
    Real.rpow_mul (by norm_num), Real.rpow_logb (by norm_num) (by norm_num) hP0,
    Real.rpow_logb (by norm_num) (by norm_num) hQ0, Real.rpow_natCast, Real.rpow_natCast,
    mul_assoc, inv_mul_cancel₀ (pow_ne_zero _ hQ0.ne'), mul_one]

theorem pd_tight_W_le (L : ℕ) (y : ℝ) (hy : 0 ≤ y) :
    pdW (dstarGraph L) (Sstar L) y ≤ (1 + y) ^ (6 * L) * (2:ℝ) ^ (-(ωpr * (6 * L : ℕ))) := by
  have hr := pd_tight_ratio L y hy
  have hW0 : 0 ≤ pdW (dstarGraph L) (Sstar L) y := by
    rw [pd_tight_W]; exact pow_nonneg (by nlinarith [sq_nonneg y]) _
  have hm := pd_tight_min.2 y hy
  set n : ℝ := ((6 * L : ℕ) : ℝ) with hn
  have hn0 : 0 ≤ n := Nat.cast_nonneg _
  have h1 : (1:ℝ) ≤ (2:ℝ) ^ (n * hpd 6 y) * (2:ℝ) ^ (-(ωpr * n)) := by
    rw [← Real.rpow_add (by norm_num)]
    apply Real.one_le_rpow (by norm_num)
    nlinarith
  calc pdW (dstarGraph L) (Sstar L) y
      ≤ pdW (dstarGraph L) (Sstar L) y * ((2:ℝ) ^ (n * hpd 6 y) * (2:ℝ) ^ (-(ωpr * n))) :=
        le_mul_of_one_le_right hW0 h1
    _ = (1 + y) ^ (6 * L) * (2:ℝ) ^ (-(ωpr * n)) := by rw [hr]; ring

namespace Aux

theorem card_dstar (L : ℕ) : Fintype.card (Fin L × Fin 6) = 6 * L := by
  rw [Fintype.card_prod, Fintype.card_fin, Fintype.card_fin, mul_comm]

end Aux

/-- Proof of `prop:fa-pd-tight`: `max_t μ_t(S*)/C(n,t) ≤ (n+1) 2^{-ψ_pr n}`. -/
theorem pd_tight_moments (L : ℕ) (t : ℕ) (ht : t ≤ 2 * L) :
    mu (pdG (dstarGraph L)) (Sstar L) (2 * L) t / ((6 * L).choose t : ℝ)
      ≤ (((6 * L : ℕ) : ℝ) + 1) * (2:ℝ) ^ (-(ωpr * (6 * L : ℕ))) := by
  have hcard : (Sstar L).card = 2 * L := (pd_tight_unique L).2.1
  obtain ⟨y, hy, hle⟩ := MLSNec.fw_gf_upper (pdG (dstarGraph L)) (Sstar L) (2 * L) hcard t ht
  rw [Aux.card_dstar] at hle
  have hW : W (pdG (dstarGraph L)) (Sstar L) (2 * L) y = pdW (dstarGraph L) (Sstar L) y := by
    unfold pdW; rw [hcard]
  rw [hW] at hle
  have hWle := pd_tight_W_le L y hy
  have hC : (0:ℝ) < (6 * L).choose t := Nat.cast_pos.2 (Nat.choose_pos (by omega))
  have hP : (0:ℝ) < (1 + y) ^ (6 * L) := pow_pos (by linarith) _
  rw [div_le_iff₀ hC]
  have h2 : mu (pdG (dstarGraph L)) (Sstar L) (2 * L) t * (1 + y) ^ (6 * L)
      ≤ ((((6 * L : ℕ) : ℝ) + 1) * (2:ℝ) ^ (-(ωpr * (6 * L : ℕ))) * ((6 * L).choose t : ℝ))
          * (1 + y) ^ (6 * L) := by
    calc mu (pdG (dstarGraph L)) (Sstar L) (2 * L) t * (1 + y) ^ (6 * L)
        ≤ (((6 * L : ℕ) : ℝ) + 1) * ((6 * L).choose t : ℝ) * pdW (dstarGraph L) (Sstar L) y := hle
      _ ≤ (((6 * L : ℕ) : ℝ) + 1) * ((6 * L).choose t : ℝ) *
            ((1 + y) ^ (6 * L) * (2:ℝ) ^ (-(ωpr * (6 * L : ℕ)))) :=
          mul_le_mul_of_nonneg_left hWle (by positivity)
      _ = _ := by ring
  exact le_of_mul_le_mul_right h2 hP

/-- Proof of `prop:fa-pd-tight`: "a trial for `k = 2L` accepts only if its sample lies in `S*`", for outcomes
whose samples have their nominal sizes; the accepting trial also has `g ≤ θ`. -/
theorem pd_tight_accepts (L : ℕ) (ψ Γ κ : ℝ)
    (o : Slot (Fintype.card (Fin L × Fin 6)) (2 * L) ψ Γ κ → Finset (Fin L × Fin 6))
    (ho : ∀ j, (o j).card = (j.1.1 : ℕ))
    (hA : Accepts (IsPairedDom (dstarGraph L)) (pdG (dstarGraph L)) (2 * L) ψ Γ κ o) :
    ∃ j, o j ⊆ Sstar L ∧ pdG (dstarGraph L) (o j) (2 * L - j.1.1) ≤ ((j.1.2 : ℕ) : ℝ) := by
  obtain ⟨j, hg, Y, hdisj, hY, hsol⟩ := hA
  refine ⟨j, ?_, hg⟩
  have ht : (j.1.1 : ℕ) ≤ 2 * L := Nat.lt_succ_iff.1 j.1.1.isLt
  have hcard : (o j ∪ Y).card ≤ 2 * L := by
    rw [card_union_of_disjoint hdisj, ho j]; omega
  have := (pd_tight_unique L).2.2 _ hsol hcard
  rw [← this]
  exact subset_union_left

namespace Aux

/-- For each `L`, the acceptance probability is at most the bound of `prop:fw-necessary`. -/
theorem prob_le (L : ℕ) (ψ' Γ κ : ℝ) (h0 : 0 ≤ ψ') (hΓ : 1 ≤ Γ) (hκ : 0 < κ) :
    (trialMeasure (U := Fin L × Fin 6) (2 * L) ψ' Γ κ
        {o | Accepts (IsPairedDom (dstarGraph L)) (pdG (dstarGraph L)) (2 * L) ψ' Γ κ o}).toReal
      ≤ MLSNec.Pnec (6 * L) (2 * L) ψ' Γ κ * (2:ℝ) ^ (ψ' * ((6 * L : ℕ) : ℝ)) *
          ((((6 * L : ℕ) : ℝ) + 1) * (2:ℝ) ^ (-(ωpr * (6 * L : ℕ)))) := by
  have hU := card_dstar L
  have hk : 2 * L ≤ Fintype.card (Fin L × Fin 6) := by rw [hU]; omega
  have hcard : (Sstar L).card = 2 * L := (pd_tight_unique L).2.1
  have hfac := trialMeasure_factor_prob (U := Fin L × Fin 6) (2 * L) hk ψ' Γ κ
  set μ := trialMeasure (U := Fin L × Fin 6) (2 * L) ψ' Γ κ with hμ
  haveI : MeasureTheory.IsProbabilityMeasure μ := by
    rw [hμ]; unfold trialMeasure
    have := hfac
    infer_instance
  set N := {o : Slot (Fintype.card (Fin L × Fin 6)) (2 * L) ψ' Γ κ → Finset (Fin L × Fin 6) |
    ∃ j, (o j).card ≠ (j.1.1 : ℕ)} with hNdef
  set E := {o : Slot (Fintype.card (Fin L × Fin 6)) (2 * L) ψ' Γ κ → Finset (Fin L × Fin 6) |
    ∃ j, o j ⊆ Sstar L ∧ pdG (dstarGraph L) (o j) (2 * L - j.1.1) ≤ ((j.1.2 : ℕ) : ℝ)}
    with hEdef
  have hN : μ N = 0 := MLSNec.trialMeasure_card_null (2 * L) ψ' Γ κ
  have hsub : {o | Accepts (IsPairedDom (dstarGraph L)) (pdG (dstarGraph L)) (2 * L) ψ' Γ κ o}
      ⊆ N ∪ E := by
    intro o ho
    by_cases h : ∃ j, (o j).card ≠ (j.1.1 : ℕ)
    · exact Or.inl h
    · push Not at h
      exact Or.inr (pd_tight_accepts L ψ' Γ κ o h ho)
  have hle : μ {o | Accepts (IsPairedDom (dstarGraph L)) (pdG (dstarGraph L)) (2 * L) ψ' Γ κ o}
      ≤ μ E := by
    calc μ {o | Accepts (IsPairedDom (dstarGraph L)) (pdG (dstarGraph L)) (2 * L) ψ' Γ κ o}
        ≤ μ (N ∪ E) := MeasureTheory.measure_mono hsub
      _ ≤ μ N + μ E := MeasureTheory.measure_union_le N E
      _ = μ E := by rw [hN, zero_add]
  have hB : ∀ t ≤ (Sstar L).card, mu (pdG (dstarGraph L)) (Sstar L) (2 * L) t /
      ((Fintype.card (Fin L × Fin 6)).choose t : ℝ)
        ≤ (((6 * L : ℕ) : ℝ) + 1) * (2:ℝ) ^ (-(ωpr * (6 * L : ℕ))) := by
    intro t ht
    rw [hU]
    exact pd_tight_moments L t (hcard ▸ ht)
  have hnec := MLSNec.mls_necessary (pdG (dstarGraph L)) (2 * L) hk ψ' Γ κ h0 hΓ hκ (Sstar L)
    hcard.le _ hB
  calc (μ {o | Accepts (IsPairedDom (dstarGraph L)) (pdG (dstarGraph L)) (2 * L) ψ' Γ κ o}).toReal
      ≤ (μ E).toReal := ENNReal.toReal_mono (MeasureTheory.measure_ne_top μ E) hle
    _ ≤ MLSNec.Pnec (Fintype.card (Fin L × Fin 6)) (2 * L) ψ' Γ κ *
          (2:ℝ) ^ (ψ' * (Fintype.card (Fin L × Fin 6) : ℝ)) *
          ((((6 * L : ℕ) : ℝ) + 1) * (2:ℝ) ^ (-(ωpr * (6 * L : ℕ)))) := hnec
    _ = _ := by rw [hU]

end Aux

/-- `prop:fa-pd-tight`, last claim, for the trial model of `MLS`. -/
theorem pd_tight_prob (ψ' Γ κ : ℝ) (h0 : 0 ≤ ψ') (hψ : ψ' < ωpr) (hΓ : 1 ≤ Γ) (hκ : 0 < κ) :
    Filter.Tendsto
      (fun L : ℕ => (trialMeasure (U := Fin L × Fin 6) (2 * L) ψ' Γ κ
        {o | Accepts (IsPairedDom (dstarGraph L)) (pdG (dstarGraph L)) (2 * L) ψ' Γ κ o}).toReal)
      Filter.atTop (nhds 0) := by
  set a : ℝ := 6 * ψ' with ha_def
  set b : ℝ := Real.logb 2 Γ + 3 with hb_def
  have hlogΓ : 0 ≤ Real.logb 2 Γ := Real.logb_nonneg (by norm_num) hΓ
  have ha : 0 ≤ a := by rw [ha_def]; linarith
  have hb : 0 ≤ b := by rw [hb_def]; linarith
  set r : ℝ := (2:ℝ) ^ (6 * (ψ' - ωpr)) with hr_def
  have hr0 : 0 < r := by positivity
  have hr1 : r < 1 := Real.rpow_lt_one_of_one_lt_of_neg (by norm_num) (by linarith)
  set C : ℝ := 8 * Γ * 2 * (a + b) * (κ * (a + b) + 1) * 7 with hC_def
  have hbound : ∀ L : ℕ, (trialMeasure (U := Fin L × Fin 6) (2 * L) ψ' Γ κ
      {o | Accepts (IsPairedDom (dstarGraph L)) (pdG (dstarGraph L)) (2 * L) ψ' Γ κ o}).toReal
        ≤ C * (((L : ℝ) + 1) ^ 4 * r ^ L) := by
    intro L
    refine (Aux.prob_le L ψ' Γ κ h0 hΓ hκ).trans ?_
    unfold MLSNec.Pnec
    set Θ := cap (6 * L) ψ' Γ with hΘ
    have hx : 0 ≤ ψ' * ((6 * L : ℕ) : ℝ) + Real.logb 2 Γ := add_nonneg (by positivity) hlogΓ
    have hc := Nat.ceil_lt_add_one hx
    have hΘr : (Θ : ℝ) < ψ' * ((6 * L : ℕ) : ℝ) + Real.logb 2 Γ + 2 := by
      rw [hΘ]; unfold cap; push_cast at hc ⊢; linarith
    have hL0 : (0:ℝ) ≤ L := Nat.cast_nonneg _
    have e2 : (Θ : ℝ) + 1 ≤ (a + b) * ((L : ℝ) + 1) := by
      rw [ha_def, hb_def]
      push_cast at hΘr
      nlinarith [mul_nonneg hb hL0]
    have e1 : ((2 * L : ℕ) : ℝ) + 1 ≤ 2 * ((L : ℝ) + 1) := by push_cast; linarith
    have e3 : κ * ((Θ : ℝ) + 1) + 1 ≤ (κ * (a + b) + 1) * ((L : ℝ) + 1) := by
      nlinarith [mul_le_mul_of_nonneg_left e2 hκ.le]
    have e4 : ((6 * L : ℕ) : ℝ) + 1 ≤ 7 * ((L : ℝ) + 1) := by push_cast; linarith
    have p0 : (0:ℝ) ≤ 8 * Γ := by linarith
    have p2 : (0:ℝ) ≤ (Θ : ℝ) + 1 := by positivity
    have p3 : (0:ℝ) ≤ κ * ((Θ : ℝ) + 1) + 1 := by
      have := mul_nonneg hκ.le p2; linarith
    have p4 : (0:ℝ) ≤ ((6 * L : ℕ) : ℝ) + 1 := by positivity
    have hy1 : (0:ℝ) ≤ 2 * ((L : ℝ) + 1) := by positivity
    have hy2 : (0:ℝ) ≤ (a + b) * ((L : ℝ) + 1) := mul_nonneg (by linarith) (by positivity)
    have hy3 : (0:ℝ) ≤ (κ * (a + b) + 1) * ((L : ℝ) + 1) := by
      have := mul_nonneg hκ.le (add_nonneg ha hb)
      exact mul_nonneg (by linarith) (by positivity)
    have q1 : 8 * Γ * (((2 * L : ℕ) : ℝ) + 1) ≤ 8 * Γ * (2 * ((L : ℝ) + 1)) :=
      mul_le_mul_of_nonneg_left e1 p0
    have q2 := mul_le_mul q1 e2 p2 (mul_nonneg p0 hy1)
    have q3 := mul_le_mul q2 e3 p3 (mul_nonneg (mul_nonneg p0 hy1) hy2)
    have q4 := mul_le_mul q3 e4 p4 (mul_nonneg (mul_nonneg (mul_nonneg p0 hy1) hy2) hy3)
    have hexp : (2:ℝ) ^ (ψ' * ((6 * L : ℕ) : ℝ)) * (2:ℝ) ^ (-(ωpr * ((6 * L : ℕ) : ℝ))) = r ^ L := by
      rw [← Real.rpow_add (by norm_num), hr_def, ← Real.rpow_natCast, ← Real.rpow_mul (by norm_num)]
      congr 1; push_cast; ring
    calc _ = (8 * Γ * (((2 * L : ℕ) : ℝ) + 1) * ((Θ : ℝ) + 1) * (κ * ((Θ : ℝ) + 1) + 1) *
            (((6 * L : ℕ) : ℝ) + 1)) * r ^ L := by rw [← hexp]; ring
      _ ≤ (8 * Γ * (2 * ((L : ℝ) + 1)) * ((a + b) * ((L : ℝ) + 1)) *
            ((κ * (a + b) + 1) * ((L : ℝ) + 1)) * (7 * ((L : ℝ) + 1))) * r ^ L :=
          mul_le_mul_of_nonneg_right q4 (pow_nonneg hr0.le _)
      _ = C * (((L : ℝ) + 1) ^ 4 * r ^ L) := by rw [hC_def]; ring
  have hlim : Filter.Tendsto (fun L : ℕ => C * (((L : ℝ) + 1) ^ 4 * r ^ L)) Filter.atTop
      (nhds 0) := by
    have h1 := tendsto_pow_const_mul_const_pow_of_abs_lt_one 4 (r := r)
      (by rw [abs_of_pos hr0]; exact hr1)
    have h2 := h1.comp (Filter.tendsto_add_atTop_nat 1)
    have h3 : Filter.Tendsto (fun L : ℕ => (((L + 1 : ℕ) : ℝ) ^ 4 * r ^ (L + 1)) * r⁻¹)
        Filter.atTop (nhds (0 * r⁻¹)) := h2.mul_const _
    rw [zero_mul] at h3
    have h4 := h3.const_mul C
    rw [mul_zero] at h4
    refine h4.congr fun L => ?_
    show C * ((((L + 1 : ℕ) : ℝ) ^ 4 * r ^ (L + 1)) * r⁻¹) = C * (((L : ℝ) + 1) ^ 4 * r ^ L)
    rw [pow_succ r L, Nat.cast_add, Nat.cast_one,
      show ((L : ℝ) + 1) ^ 4 * (r ^ L * r) * r⁻¹ = ((L : ℝ) + 1) ^ 4 * r ^ L * (r * r⁻¹) by ring,
      mul_inv_cancel₀ hr0.ne', mul_one]
  exact squeeze_zero (fun L => ENNReal.toReal_nonneg) hbound hlim

/-- `prop:fa-pd-tight`, assembled. -/
theorem fa_pd_tight :
    (0 < ystar ∧
      (∀ y : ℝ, 0 < y → DifferentiableAt ℝ (hpd 6) y) ∧
      (∀ y : ℝ, 0 < y → (deriv (hpd 6) y = 0 ↔ y = ystar)) ∧
      0 ≤ ystar ∧ ∀ y : ℝ, 0 ≤ y → ωpr ≤ hpd 6 y) ∧
    (∀ L : ℕ, IsPairedDom (dstarGraph L) (Sstar L) ∧ (Sstar L).card = 2 * L ∧
      ∀ S : Finset (Fin L × Fin 6), IsPairedDom (dstarGraph L) S → S.card ≤ 2 * L →
        S = Sstar L) ∧
    ∀ ψ' Γ κ : ℝ, 0 ≤ ψ' → ψ' < ωpr → 1 ≤ Γ → 0 < κ →
      Filter.Tendsto
        (fun L : ℕ => (trialMeasure (U := Fin L × Fin 6) (2 * L) ψ' Γ κ
          {o | Accepts (IsPairedDom (dstarGraph L)) (pdG (dstarGraph L)) (2 * L) ψ' Γ κ o}).toReal)
        Filter.atTop (nhds 0) :=
  ⟨⟨pd_tight_crit.1, pd_tight_crit.2.1, pd_tight_crit.2.2, pd_tight_min.1, pd_tight_min.2⟩,
    pd_tight_unique, fun ψ' Γ κ h0 hψ hΓ hκ => pd_tight_prob ψ' Γ κ h0 hψ hΓ hκ⟩

end Tight

namespace Examples

/-- E1: `pd_rate_W` for one double star. -/
theorem ex1_rate_W :
    (1 + ystar) ^ Fintype.card (Fin 1 × Fin 6) *
        (2:ℝ) ^ (-(ωpr * Fintype.card (Fin 1 × Fin 6)))
      ≤ pdW (dstarGraph 1) (Sstar 1) ystar :=
  pd_rate_W (dstarGraph 1) (dstarGraph_noIsolated 1) (Sstar 1) (pd_tight_unique 1).1

def dsAnc (p : Fin 1 × Fin 6) : Fin 1 × Fin 6 := (p.1, if p.2.val ≤ 3 then 0 else 1)

theorem ex2_point :
    IsPairing (dstarGraph 1) (Sstar 1) {((0, 0), (0, 1))} ∧
    IsAnchor (dstarGraph 1) (Sstar 1) dsAnc ∧
    ancDeg (Sstar 1) dsAnc (0, 0) = 2 ∧ ancDeg (Sstar 1) dsAnc (0, 1) = 2 ∧
    ∀ y : ℝ, 0 ≤ y →
      ∏ q ∈ ({((0, 0), (0, 1))} : Finset ((Fin 1 × Fin 6) × (Fin 1 × Fin 6))),
          Ωpair y (ancDeg (Sstar 1) dsAnc q.1) (ancDeg (Sstar 1) dsAnc q.2)
        ≤ pdW (dstarGraph 1) (Sstar 1) y := by
  have hcov : ∀ w : Fin 1 × Fin 6, w ∈ Sstar 1 → w = (0, 0) ∨ w = (0, 1) := by decide
  have hP : IsPairing (dstarGraph 1) (Sstar 1) {((0, 0), (0, 1))} := by
    refine ⟨?_, ?_⟩
    · intro q hq
      rw [Finset.mem_singleton] at hq
      subst hq
      exact ⟨by decide, by decide, by decide⟩
    · intro w hw
      refine ⟨((0, 0), (0, 1)), ⟨Finset.mem_singleton_self _, ?_⟩, ?_⟩
      · rcases hcov w hw with rfl | rfl
        · exact Or.inl rfl
        · exact Or.inr rfl
      · intro q hq
        exact Finset.mem_singleton.1 hq.1
  have ha : IsAnchor (dstarGraph 1) (Sstar 1) dsAnc := by
    unfold IsAnchor
    decide
  refine ⟨hP, ha, by decide, by decide, (pd_point (dstarGraph 1) (Sstar 1) _ hP dsAnc ha).2⟩

def pathG : SimpleGraph (Fin 6) := SimpleGraph.fromRel fun i j => j.val = i.val + 1
instance instDecidableRelPathG : DecidableRel pathG.Adj :=
  inferInstanceAs (DecidableRel (SimpleGraph.fromRel fun i j : Fin 6 => j.val = i.val + 1).Adj)

def pathAnc (v : Fin 6) : Fin 6 := if v = 0 then 1 else if v = 5 then 4 else v

theorem ex3_path :
    IsPairing pathG {1, 2, 3, 4} {(1, 2), (3, 4)} ∧ IsAnchor pathG {1, 2, 3, 4} pathAnc ∧
    (und pathG {2}).card = 3 ∧ pdRhs {1, 2, 3, 4} {(1, 2), (3, 4)} pathAnc {2} = 4 := by
  have hP : IsPairing pathG {1, 2, 3, 4} {(1, 2), (3, 4)} := by
    refine ⟨by decide, ?_⟩
    have key : ∀ w ∈ ({1, 2, 3, 4} : Finset (Fin 6)),
        ∃ q ∈ ({(1, 2), (3, 4)} : Finset (Fin 6 × Fin 6)),
          (q.1 = w ∨ q.2 = w) ∧
            ∀ q' ∈ ({(1, 2), (3, 4)} : Finset (Fin 6 × Fin 6)),
              (q'.1 = w ∨ q'.2 = w) → q' = q := by decide
    intro w hw
    obtain ⟨q, hq, hcov, huniq⟩ := key w hw
    exact ⟨q, ⟨hq, hcov⟩, fun q' hq' => huniq q' hq'.1 hq'.2⟩
  have ha : IsAnchor pathG {1, 2, 3, 4} pathAnc := by
    unfold IsAnchor
    decide
  exact ⟨hP, ha, by decide, by decide⟩

/-- E4: `pd_tight_prob` at `ψ' = 7/10`, `Γ = 2`, `κ = 1`. -/
theorem ex4_tight_prob :
    Filter.Tendsto
      (fun L : ℕ => (trialMeasure (U := Fin L × Fin 6) (2 * L) (7 / 10) 2 1
        {o | Accepts (IsPairedDom (dstarGraph L)) (pdG (dstarGraph L)) (2 * L) (7 / 10) 2 1 o}).toReal)
      Filter.atTop (nhds 0) :=
  pd_tight_prob (7 / 10) 2 1 (by norm_num) (lt_of_lt_of_le (by norm_num) pd_rate.2.1) (by norm_num)
    one_pos

/-- E5: the event of (c) is not null by construction. -/
theorem ex5_success (L : ℕ) :
    1 - Real.exp (-1) ≤
      (trialMeasure (U := Fin L × Fin 6) (Sstar L).card (70502 / 10 ^ 5) 1 1
        {o | Accepts (IsPairedDom (dstarGraph L)) (pdG (dstarGraph L)) (Sstar L).card
          (70502 / 10 ^ 5) 1 1 o}).toReal :=
  pd_success (dstarGraph L) (Sstar L) (pd_tight_unique L).1 1 one_pos

/-- E6: the boundary `ψ' = ψ_pr`. -/
theorem ex6_boundary (L : ℕ) :
    1 - Real.exp (-1) ≤
      (trialMeasure (U := Fin L × Fin 6) (2 * L) ωpr 1 1
        {o | Accepts (IsPairedDom (dstarGraph L)) (pdG (dstarGraph L)) (2 * L) ωpr 1 1 o}).toReal := by
  have hcard := (pd_tight_unique L).2.1
  have hU : 2 * L ≤ Fintype.card (Fin L × Fin 6) := by
    rw [Fintype.card_prod, Fintype.card_fin, Fintype.card_fin]; omega
  have hω : 0 ≤ ωpr := le_trans (by norm_num) pd_rate.2.1
  apply MLS.mls_success (IsPairedDom (dstarGraph L)) (pdG (dstarGraph L))
    (fun _ _ => Nat.cast_nonneg _) (2 * L) hU ωpr 1 1 hω le_rfl one_pos (Sstar L)
    (pd_tight_unique L).1 hcard
  apply MLS.star_of_W (pdG (dstarGraph L)) (Sstar L) (2 * L) hcard ωpr 1 ystar one_pos
    pd_tight_min.1
  rw [div_one]
  have := pd_rate_W (dstarGraph L) (dstarGraph_noIsolated L) (Sstar L) (pd_tight_unique L).1
  unfold pdW at this
  rw [hcard] at this
  exact this

end Examples

end MaxLeafFormal.PDGraph