Identical until bad: a common part, per-step costs, and coupled games

THEORY.md

@@ -220,6 +220,36 @@ G\big(x^n, (y, 0)^n\big) = H\big(x^n, (y, 0)^n\big)
 \mathrm{Adv}_P(G^-, H^-) \le \Pr[P \text{ wins } G] = \Pr[P \text{ wins } H] .
 ```
 
+**Identical until bad** is proved in two layers. At the systems level, two random systems $`R_1`$
+and $`R_2`$ have transcript probabilities that both lie above a common part $`g`$ with
+$`g([]) = 1`$. A step from a possible transcript $`h`$ by an admitted query $`x`$ loses
+$`g(h) - \sum_y g(h, x, y)`$ of the common part. If each step loses at most
+$`\beta(h, x)\, R_1(h)`$, and the [cost][transcriptCost] of each possible transcript, the sum of
+$`\beta`$ over its steps, is at most $`\varepsilon`$, then by the union bound over the steps every
+compatible environment [stays in the common part][RandomSystem.one_sub_le_sum_tSupp] with
+probability at least $`1 - \varepsilon`$, and the two systems are
+[within][RandomSystem.transcriptDistance_le_of_transcriptCost_le] $`\varepsilon`$ of each other:
+
+```math
+g(h) - \sum_y g(h, x, y) \le \beta(h, x)\, R_1(h), \qquad
+\sum_{k < |h|} \beta(h_1 \cdots h_k,\ x_{k+1}) \le \varepsilon
+\quad \Longrightarrow \quad
+\Delta(R_1, R_2) \le \varepsilon .
+```
+
+Games are on top of this. On a game $`G`$, the part with every MBO unset lies below the visible
+system, and a step loses from it the probability that $`G`$ sets the MBO at that step. Suppose
+that, from every transcript with every MBO unset, $`G`$ sets the MBO at the next query $`x`$ with
+probability at most $`\beta(h, x)`$ times the probability of the transcript. The mass missing from
+the unset part along the transcripts of a winner is the winning probability, so every winner
+[wins with probability at most][Domain.Distinguisher.winProbability_le_of_transcriptCost_le]
+$`\varepsilon`$. Two games equivalent as games have the same unset part, which is therefore a
+common part of their visible systems, and the per-step costs bound its missing mass: the visible
+systems are [within][RandomSystem.GameEquivalent.transcriptDistance_visible_le] $`\varepsilon`$ of
+each other. Two discrete games are equivalent as games when they are
+[coupled][PDG.gameEquivalent_behavior_of_isCoupling]: a joint law of the two [1, Theorem 2] whose
+pairs have one condition and systems that answer alike while the condition does not hold.
+
 **Attachment**: the library defines the action of a PDC $`\alpha`$ on a game by its
 [MBO-forwarding lift][PDCBehavior.liftMBO] $`\hat\alpha`$: the lift runs $`\alpha`$, which does not see
 the inside MBOs, and gives each outside reply the MBO of the latest inside reply. CR18 states this
@@ -888,8 +918,8 @@ agreeing with a map on a finite set $`S`$: there are $`\lvert Y \rvert^{\lvert X
 [RandomSystem.ofPDSClass_bijective]: src/RandomSystems/Cumulative/Presentation.lean#L312
 [RandomSystem.sLaw]: src/RandomSystems/Cumulative/CumulativeObservation.lean#L179
 [RandomSystem.Compatible]: src/RandomSystems/Cumulative/CumulativeObservation.lean#L197
-[RandomSystem.eq_iff_sLaw]: src/RandomSystems/Cumulative/CumulativeObservation.lean#L503
-[RandomSystem.eq_iff_sLaw_fixedQueries]: src/RandomSystems/Cumulative/CumulativeObservation.lean#L517
+[RandomSystem.eq_iff_sLaw]: src/RandomSystems/Cumulative/CumulativeObservation.lean#L534
+[RandomSystem.eq_iff_sLaw_fixedQueries]: src/RandomSystems/Cumulative/CumulativeObservation.lean#L548
 [RandomSystem.mix]: src/RandomSystems/Cumulative/CumulativeOperations.lean#L45
 [RandomSystem.parallel]: src/RandomSystems/Cumulative/CumulativeOperations.lean#L130
 [IsDDC]: src/RandomSystems/DDC/DDC.lean#L127
@@ -960,16 +990,22 @@ agreeing with a map on a finite set $`S`$: there are $`\lvert Y \rvert^{\lvert X
 [PDG]: src/RandomSystems/Game/DiscreteMBO.lean#L54
 [PDG.ofFunction]: src/RandomSystems/Game/FunctionGame.lean#L37
 [RandomSystem.MonotoneMBO]: src/RandomSystems/Game/MBO.lean#L305
-[RandomSystem.visible]: src/RandomSystems/Game/MBO.lean#L314
-[DDE.blindMBO]: src/RandomSystems/Game/MBO.lean#L407
-[RandomSystem.winProbability]: src/RandomSystems/Game/MBO.lean#L477
-[RandomSystem.ConditionallyEquivalent]: src/RandomSystems/Game/MBO.lean#L520
-[Domain.Distinguisher.advantage_le_winProbability]: src/RandomSystems/Game/MBO.lean#L753
-[Domain.Distinguisher.winProbability_le_of_unsetProbability]: src/RandomSystems/Game/MBO.lean#L948
-[RandomSystem.transcriptDistance_visible_le_of_unsetProbability]: src/RandomSystems/Game/MBO.lean#L973
-[RandomSystem.GameEquivalent]: src/RandomSystems/Game/MBO.lean#L534
-[Domain.Distinguisher.winProbability_eq_of_gameEquivalent]: src/RandomSystems/Game/MBO.lean#L857
-[Domain.Distinguisher.advantage_le_winProbability_of_gameEquivalent]: src/RandomSystems/Game/MBO.lean#L871
+[RandomSystem.visible]: src/RandomSystems/Game/MBO.lean#L340
+[DDE.blindMBO]: src/RandomSystems/Game/MBO.lean#L410
+[RandomSystem.winProbability]: src/RandomSystems/Game/MBO.lean#L480
+[RandomSystem.ConditionallyEquivalent]: src/RandomSystems/Game/MBO.lean#L523
+[Domain.Distinguisher.advantage_le_winProbability]: src/RandomSystems/Game/MBO.lean#L756
+[Domain.Distinguisher.winProbability_le_of_unsetProbability]: src/RandomSystems/Game/MBO.lean#L951
+[RandomSystem.transcriptDistance_visible_le_of_unsetProbability]: src/RandomSystems/Game/MBO.lean#L976
+[RandomSystem.GameEquivalent]: src/RandomSystems/Game/MBO.lean#L537
+[Domain.Distinguisher.winProbability_eq_of_gameEquivalent]: src/RandomSystems/Game/MBO.lean#L860
+[Domain.Distinguisher.advantage_le_winProbability_of_gameEquivalent]: src/RandomSystems/Game/MBO.lean#L874
+[transcriptCost]: src/RandomSystems/Distance/UntilBad.lean#L38
+[RandomSystem.one_sub_le_sum_tSupp]: src/RandomSystems/Distance/UntilBad.lean#L65
+[RandomSystem.transcriptDistance_le_of_transcriptCost_le]: src/RandomSystems/Distance/UntilBad.lean#L146
+[Domain.Distinguisher.winProbability_le_of_transcriptCost_le]: src/RandomSystems/Game/UntilBad.lean#L148
+[RandomSystem.GameEquivalent.transcriptDistance_visible_le]: src/RandomSystems/Game/UntilBad.lean#L177
+[PDG.gameEquivalent_behavior_of_isCoupling]: src/RandomSystems/Game/UntilBad.lean#L209
 [PDCBehavior.liftMBO]: src/RandomSystems/Game/MBOAttachment.lean#L455
 [PDCBehavior.liftMBO_id]: src/RandomSystems/Game/MBOAttachment.lean#L495
 [PDCBehavior.liftMBO_comp]: src/RandomSystems/Game/MBOAttachment.lean#L1515
@@ -1247,10 +1283,10 @@ agreeing with a map on a finite set $`S`$: there are $`\lvert Y \rvert^{\lvert X
 [not_supAgreement_disagreement_le_every_pair]: src/Probability/MultiCoupling.lean#L778
 [supAgreement]: src/Probability/MultiCoupling.lean#L87
 [supAgreement_eq_weight_overlapDist]: src/Probability/MultiCoupling.lean#L397
-[Distribution]: src/Probability/Distribution.lean#L55
-[ProbDist]: src/Probability/Distribution.lean#L148
-[isProbDist]: src/Probability/Distribution.lean#L127
-[mass]: src/Probability/Distribution.lean#L216
+[Distribution]: src/Probability/Distribution.lean#L56
+[ProbDist]: src/Probability/Distribution.lean#L149
+[isProbDist]: src/Probability/Distribution.lean#L128
+[mass]: src/Probability/Distribution.lean#L217
 [fTransform]: src/Probability/Distribution.lean#L587
 [prod]: src/Probability/Distribution.lean#L942
 [pi]: src/Probability/Distribution.lean#L1583

src/Probability/Distribution.lean

@@ -30,7 +30,8 @@ Lanzenberger–Maurer, *Coupling of Random Systems*, Definitions 1, 2 and 4.
 ## Main results
 
 * the mass calculus: additivity, complements, monotonicity, `mass_le_weight`;
-  `abs_mass_sub_le_of_le`: laws above a common part differ by at most the rest
+  `mass_sub_mass_le_of_le`, `abs_mass_sub_le_of_le`: laws above a common part differ by at most
+  the rest
 * pushforward: `mass_fTransform`, `weight_fTransform`, `fTransform_comp`,
   `fTransform_prod`, `fTransform_equiv_uniform`
 * products: `prod_apply`, `weight_prod`, `mass_prod_fst`, `mass_prod_snd`,
@@ -342,44 +343,43 @@ theorem mass_mono {A : Type*} {X : Distribution A} (hX : X.NonNeg) {P Q : A →
   · simp [hP, h a hP]
   · by_cases hQ : Q a <;> simp [hP, hQ, hX a]
 
-/-- **A common part bounds the difference of masses**: two laws of weight one that both lie
-above `ν` differ on every event by at most the weight they do not share with `ν`,
-`|μ₁(P) − μ₂(P)| ≤ 1 − |ν|`. -/
-theorem abs_mass_sub_le_of_le {A : Type*} {μ₁ μ₂ ν : Distribution A} (h₁ : μ₁.weight = 1)
-    (h₂ : μ₂.weight = 1) (hν₁ : ∀ a, ν a ≤ μ₁ a) (hν₂ : ∀ a, ν a ≤ μ₂ a) (P : A → Prop) :
-    |μ₁.mass P - μ₂.mass P| ≤ 1 - ν.weight := by
-  -- Plan. Each μ splits as ν + (μ − ν), with μ − ν ≥ 0 of weight 1 − |ν|. So
-  -- μ(P) − ν(P) = (μ − ν)(P) lies in [0, 1 − |ν|] for μ = μ₁ and μ = μ₂, and
-  --   |μ₁(P) − μ₂(P)| = |(μ₁(P) − ν(P)) − (μ₂(P) − ν(P))| ≤ 1 − |ν|.
+/-- **A common part bounds the difference of masses**, one side: if `μ₁` has weight one and both
+`μ₁` and `μ₂` lie above `ν`, then `μ₁` exceeds `μ₂` on every event by at most the weight `μ₁` does
+not share with `ν`, `μ₁(P) − μ₂(P) ≤ 1 − |ν|`. -/
+theorem mass_sub_mass_le_of_le {A : Type*} {μ₁ μ₂ ν : Distribution A} (h₁ : μ₁.weight = 1)
+    (hν₁ : ∀ a, ν a ≤ μ₁ a) (hν₂ : ∀ a, ν a ≤ μ₂ a) (P : A → Prop) :
+    μ₁.mass P - μ₂.mass P ≤ 1 - ν.weight := by
+  -- Plan. Each μ above ν splits as ν + (μ − ν), with μ − ν ≥ 0. So
+  --   μ₁(P) − μ₂(P) = (μ₁ − ν)(P) − (μ₂ − ν)(P) ≤ (μ₁ − ν)(P) ≤ |μ₁ − ν| = 1 − |ν|.
   -- Mass is additive, ν + (μ − ν) = μ: so (μ − ν)(P) = μ(P) − ν(P).
   have hsub : ∀ μ : Distribution A, (μ - ν).mass P = μ.mass P - ν.mass P := by
     intro μ
     have := mass_add ν (μ - ν) P
     rw [add_sub_cancel] at this
     linarith
-  -- For μ of weight 1 above ν: 0 ≤ μ(P) − ν(P) ≤ 1 − |ν|.
-  have hbound : ∀ μ : Distribution A, μ.weight = 1 → (∀ a, ν a ≤ μ a) →
-      0 ≤ μ.mass P - ν.mass P ∧ μ.mass P - ν.mass P ≤ 1 - ν.weight := by
-    intro μ hw hle
-    -- μ − ν ≥ 0 pointwise.
-    have hnn : (μ - ν).NonNeg := fun a => by
-      simp only [Finsupp.coe_sub, Pi.sub_apply, sub_nonneg]
-      exact hle a
-    rw [← hsub]
-    refine ⟨hnn.mass_nonneg P, ?_⟩
-    -- |μ − ν| = |μ| − |ν| = 1 − |ν|: additivity on the sure event.
-    have hwt : (μ - ν).weight = 1 - ν.weight := by
-      have := mass_add ν (μ - ν) (fun _ => True)
-      rw [add_sub_cancel, mass_true, mass_true, mass_true, hw] at this
-      linarith
-    -- A mass of the nonnegative μ − ν is at most its weight.
-    rw [← hwt]
-    exact mass_le_weight hnn P
-  -- Both differences lie in [0, 1 − |ν|], so theirs is at most 1 − |ν| in absolute value.
-  obtain ⟨hlo₁, hhi₁⟩ := hbound μ₁ h₁ hν₁
-  obtain ⟨hlo₂, hhi₂⟩ := hbound μ₂ h₂ hν₂
-  rw [abs_le]
-  constructor <;> linarith
+  -- μ − ν ≥ 0 pointwise, for μ above ν.
+  have hnn : ∀ μ : Distribution A, (∀ a, ν a ≤ μ a) → (μ - ν).NonNeg := fun μ hle a => by
+    simp only [Finsupp.coe_sub, Pi.sub_apply, sub_nonneg]
+    exact hle a
+  -- |μ₁ − ν| = |μ₁| − |ν| = 1 − |ν|: additivity on the sure event.
+  have hwt : (μ₁ - ν).weight = 1 - ν.weight := by
+    have := mass_add ν (μ₁ - ν) (fun _ => True)
+    rw [add_sub_cancel, mass_true, mass_true, mass_true, h₁] at this
+    linarith
+  -- (μ₂ − ν)(P) ≥ 0, and a mass of the nonnegative μ₁ − ν is at most its weight.
+  have hlo := (hnn μ₂ hν₂).mass_nonneg P
+  have hhi := mass_le_weight (hnn μ₁ hν₁) P
+  rw [hsub] at hlo hhi
+  linarith
+
+/-- **A common part bounds the difference of masses**: two laws of weight one that both lie
+above `ν` differ on every event by at most the weight they do not share with `ν`,
+`|μ₁(P) − μ₂(P)| ≤ 1 − |ν|`. -/
+theorem abs_mass_sub_le_of_le {A : Type*} {μ₁ μ₂ ν : Distribution A} (h₁ : μ₁.weight = 1)
+    (h₂ : μ₂.weight = 1) (hν₁ : ∀ a, ν a ≤ μ₁ a) (hν₂ : ∀ a, ν a ≤ μ₂ a) (P : A → Prop) :
+    |μ₁.mass P - μ₂.mass P| ≤ 1 - ν.weight :=
+  -- The one-sided bound, for μ₁ over μ₂ and for μ₂ over μ₁.
+  abs_sub_le_iff.mpr ⟨mass_sub_mass_le_of_le h₁ hν₁ hν₂ P, mass_sub_mass_le_of_le h₂ hν₂ hν₁ P⟩
 
 /-- **A single atom is below the mass of any event it satisfies**: `X a ≤ X(P)`
 when `P a`.  Non-negativity is what makes the other summands harmless — the

src/RandomSystems.lean

@@ -36,10 +36,12 @@ import RandomSystems.Distance.HCoefficient
 import RandomSystems.Distance.ParallelObservation
 import RandomSystems.Distance.Restriction
 import RandomSystems.Distance.Transcript
+import RandomSystems.Distance.UntilBad
 import RandomSystems.Game.DiscreteMBO
 import RandomSystems.Game.FunctionGame
 import RandomSystems.Game.MBO
 import RandomSystems.Game.MBOAttachment
+import RandomSystems.Game.UntilBad
 import RandomSystems.PDS.Conditional
 import RandomSystems.PDS.Filter
 import RandomSystems.PDS.Function

src/RandomSystems/Cumulative/CumulativeObservation.lean

@@ -223,50 +223,81 @@ theorem tSupp_possible : ∀ {m h}, h ∈ tSupp R σ m → R h ≠ 0 := by
     · have he : h = p := Finset.mem_singleton.mp hh
       exact he ▸ ih hp
 
-theorem sum_tSupp (hC : Compatible R σ) : ∀ m, ∑ h ∈ tSupp R σ m, (if Good σ m h then R h else 0) = 1 := by
+/-- **One more round**: a sum over the transcripts of `σ` within `m + 1` rounds is the sum, over
+the transcripts within `m` rounds, of the sum over their extensions by the possible replies to
+the next query of `σ`, or of the transcript itself when `σ` has stopped. -/
+theorem sum_tSupp_succ (f : List (A × B) → ℝ) (m : ℕ) :
+    ∑ h ∈ tSupp R σ (m + 1), f h = ∑ h ∈ tSupp R σ m,
+      if hd : (σ (h.map Prod.snd)).Dom then
+        ∑ y ∈ (R.extensionLaw h ((σ (h.map Prod.snd)).get hd)).support,
+          f (h ++ [((σ (h.map Prod.snd)).get hd, y)])
+      else f h := by
+  -- The transcripts within m + 1 rounds are the union, over the transcripts h within m rounds,
+  -- of the extensions of h by one round, or of h itself; the union is disjoint.
+  rw [tSupp, Finset.sum_biUnion]
+  · refine Finset.sum_congr rfl fun h _ => ?_
+    split_ifs with hd
+    -- Distinct replies give distinct extensions.
+    · exact Finset.sum_image fun y _ y' _ e => by simpa using e
+    · exact Finset.sum_singleton _ _
+  -- Disjointness. A transcript within m rounds has at most m rounds, and exactly m when σ asks
+  -- a further query; so an extension by one round has m + 1 rounds and a kept transcript at most
+  -- m, and a transcript is determined by any extension of it by one round.
+  · intro h hh h' hh' hne
+    rw [Function.onFun, Finset.disjoint_left]
+    intro g hg hg'
+    have hlen : ∀ p ∈ tSupp R σ m,
+        p.length ≤ m ∧ ((σ (p.map Prod.snd)).Dom → p.length = m) := by
+      intro p hp
+      rcases (tSupp_good hp).2 with hl | ⟨hl, hs⟩
+      · exact ⟨hl.le, fun _ => hl⟩
+      · exact ⟨hl.le, fun hd => absurd hd hs⟩
+    split_ifs at hg hg' with e1 e2 e2
+    -- Both extended: the extensions agree, so do the transcripts.
+    · obtain ⟨y, -, rfl⟩ := Finset.mem_image.mp hg
+      obtain ⟨y', -, e⟩ := Finset.mem_image.mp hg'
+      exact hne (List.append_inj' e rfl).1.symm
+    -- One extended, one kept: m + 1 rounds against at most m.
+    · obtain ⟨y, -, rfl⟩ := Finset.mem_image.mp hg
+      have hl := congrArg List.length (Finset.mem_singleton.mp hg')
+      simp only [List.length_append, List.length_singleton] at hl
+      have := (hlen h hh).2 e1
+      have := (hlen h' hh').1
+      omega
+    · obtain ⟨y', -, e⟩ := Finset.mem_image.mp hg'
+      have hl := congrArg List.length (e.trans (Finset.mem_singleton.mp hg))
+      simp only [List.length_append, List.length_singleton] at hl
+      have := (hlen h' hh').2 e2
+      have := (hlen h hh).1
+      omega
+    -- Both kept: both are the transcript g.
+    · exact hne ((Finset.mem_singleton.mp hg).symm.trans (Finset.mem_singleton.mp hg'))
+
+theorem sum_tSupp (hC : Compatible R σ) :
+    ∀ m, ∑ h ∈ tSupp R σ m, (if Good σ m h then R h else 0) = 1 := by
   intro m
   induction m with
   | zero => simp [tSupp, Good, Done, cons_nil, R.mass_nil]
   | succ m ih =>
-    rw [tSupp, Finset.sum_biUnion]
-    · rw [← ih]
-      refine Finset.sum_congr rfl fun h hh => ?_
-      obtain ⟨hc, hd'⟩ := tSupp_good hh
-      rw [if_pos ⟨hc, hd'⟩]
-      split_ifs with hd
-      · rw [Finset.sum_image (fun y _ y' _ e => by simpa using e)]
-        rw [← sum_extension R h ((σ (h.map Prod.snd)).get hd)
-          (hC h _ hc (tSupp_possible hh) (Part.get_mem hd))]
-        refine Finset.sum_congr rfl fun y _ => ?_
-        have hl : h.length = m := by
-          rcases hd' with h | ⟨_, h⟩
-          · exact h
-          · exact absurd hd h
-        rw [if_pos ⟨cons_snoc.mpr ⟨hc, Part.get_mem hd⟩, Or.inl (by simp [hl])⟩]
-      · rw [Finset.sum_singleton,
-          if_pos ⟨hc, Or.inr ⟨by rcases hd' with h | ⟨h, _⟩ <;> omega, hd⟩⟩]
-    · intro h hh h' hh' hne
-      simp only [Function.onFun]
-      rw [Finset.disjoint_left]
-      intro g hg hg'
-      obtain ⟨hc, hd⟩ := tSupp_good (m := m) hh
-      obtain ⟨hc', hd'⟩ := tSupp_good (m := m) hh'
-      split_ifs at hg hg' with e1 e2 e2
-      · obtain ⟨y, -, rfl⟩ := Finset.mem_image.mp hg
-        obtain ⟨y', -, e⟩ := Finset.mem_image.mp hg'
-        exact hne (List.append_inj' e rfl).1.symm
-      · obtain ⟨y, -, rfl⟩ := Finset.mem_image.mp hg
-        rw [Finset.mem_singleton] at hg'
-        have hl : h.length = m := by rcases hd with h | ⟨_, h⟩; exact h; exact absurd e1 h
-        have := congrArg List.length hg'
-        rcases hd' with h | ⟨h, _⟩ <;> simp at this <;> omega
-      · obtain ⟨y', -, e⟩ := Finset.mem_image.mp hg'
-        rw [Finset.mem_singleton] at hg
-        have hl : h'.length = m := by rcases hd' with h | ⟨_, h⟩; exact h; exact absurd e2 h
-        have := congrArg List.length (e.trans hg)
-        rcases hd with h | ⟨h, _⟩ <;> simp at this <;> omega
-      · rw [Finset.mem_singleton] at hg hg'
-        exact hne (hg.symm.trans hg')
+    -- One more round: each transcript h within m rounds keeps its probability, spread over its
+    -- extensions when σ asks a further query.
+    rw [sum_tSupp_succ, ← ih]
+    refine Finset.sum_congr rfl fun h hh => ?_
+    obtain ⟨hc, hd'⟩ := tSupp_good hh
+    rw [if_pos (show Good σ m h from ⟨hc, hd'⟩)]
+    by_cases hd : (σ (h.map Prod.snd)).Dom
+    -- σ asks x after h, admitted by compatibility: the possible replies to x weigh R h, and each
+    -- extension of h has m + 1 rounds.
+    · rw [dif_pos hd, ← sum_extension R h ((σ (h.map Prod.snd)).get hd)
+        (hC h _ hc (tSupp_possible hh) (Part.get_mem hd))]
+      have hl : h.length = m := by
+        rcases hd' with hl | ⟨_, hs⟩
+        · exact hl
+        · exact absurd hd hs
+      refine Finset.sum_congr rfl fun y _ => ?_
+      rw [if_pos ⟨cons_snoc.mpr ⟨hc, Part.get_mem hd⟩, Or.inl (by simp [hl])⟩]
+    -- σ has stopped: h is complete within m + 1 rounds too.
+    · rw [dif_neg hd, if_pos ⟨hc, Or.inr ⟨by rcases hd' with hl | ⟨hl, _⟩ <;> omega, hd⟩⟩]
 
 /-- **The transcript law is a probability distribution.** -/
 theorem sLaw_isProbDist (hC : Compatible R σ) (n : ℕ) : (sLaw R σ n).isProbDist := by