Games equivalent as games and the fundamental lemma

THEORY.md

@@ -205,6 +205,21 @@ G \mathrel{|\!\equiv} T, \quad \Pr_G[\text{MBO set} \mid x^n] \le \varepsilon \
 \Delta(G^-, T) \le \varepsilon .
 ```
 
+Two games are [**equivalent as games**][RandomSystem.GameEquivalent], $`G \overset{g}{\equiv} H`$,
+when they behave alike as long as the MBO is unset: they give every transcript with every MBO
+unset the same probability [3, Definition 4.16], [4, Definition 5]. A distinguisher then
+[wins both alike][Domain.Distinguisher.winProbability_eq_of_gameEquivalent] [3, Lemma 4.15], and
+by the fundamental lemma its advantage between their visible systems is
+[at most its winning probability][Domain.Distinguisher.advantage_le_winProbability_of_gameEquivalent]
+[3, Lemma 4.16], [4, Lemma 7 and Theorem 1 (i)]: to tell them apart, it must set the MBO. For
+games replying at the queried label:
+
+```math
+G\big(x^n, (y, 0)^n\big) = H\big(x^n, (y, 0)^n\big)
+\quad \Longrightarrow \quad
+\mathrm{Adv}_P(G^-, H^-) \le \Pr[P \text{ wins } G] = \Pr[P \text{ wins } H] .
+```
+
 **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
@@ -944,14 +959,17 @@ agreeing with a map on a finite set $`S`$: there are $`\lvert Y \rvert^{\lvert X
 [DDG]: src/RandomSystems/Game/DiscreteMBO.lean#L50
 [PDG]: src/RandomSystems/Game/DiscreteMBO.lean#L54
 [PDG.ofFunction]: src/RandomSystems/Game/FunctionGame.lean#L37
-[RandomSystem.MonotoneMBO]: src/RandomSystems/Game/MBO.lean#L290
-[RandomSystem.visible]: src/RandomSystems/Game/MBO.lean#L299
-[DDE.blindMBO]: src/RandomSystems/Game/MBO.lean#L392
-[RandomSystem.winProbability]: src/RandomSystems/Game/MBO.lean#L462
-[RandomSystem.ConditionallyEquivalent]: src/RandomSystems/Game/MBO.lean#L505
-[Domain.Distinguisher.advantage_le_winProbability]: src/RandomSystems/Game/MBO.lean#L759
-[Domain.Distinguisher.winProbability_le_of_unsetProbability]: src/RandomSystems/Game/MBO.lean#L838
-[RandomSystem.transcriptDistance_visible_le_of_unsetProbability]: src/RandomSystems/Game/MBO.lean#L863
+[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
 [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
@@ -1229,14 +1247,14 @@ 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#L54
-[ProbDist]: src/Probability/Distribution.lean#L147
-[isProbDist]: src/Probability/Distribution.lean#L126
-[mass]: src/Probability/Distribution.lean#L215
-[fTransform]: src/Probability/Distribution.lean#L547
-[prod]: src/Probability/Distribution.lean#L902
-[pi]: src/Probability/Distribution.lean#L1543
-[uniform]: src/Probability/Distribution.lean#L481
+[Distribution]: src/Probability/Distribution.lean#L55
+[ProbDist]: src/Probability/Distribution.lean#L148
+[isProbDist]: src/Probability/Distribution.lean#L127
+[mass]: src/Probability/Distribution.lean#L216
+[fTransform]: src/Probability/Distribution.lean#L587
+[prod]: src/Probability/Distribution.lean#L942
+[pi]: src/Probability/Distribution.lean#L1583
+[uniform]: src/Probability/Distribution.lean#L521
 [statDist]: src/Probability/StatisticalDistance.lean#L88
 [statDist_triangle]: src/Probability/StatisticalDistance.lean#L243
 [statDist_fTransform_le]: src/Probability/StatisticalDistance.lean#L615

src/Probability/Distribution.lean

@@ -29,7 +29,8 @@ Lanzenberger–Maurer, *Coupling of Random Systems*, Definitions 1, 2 and 4.
 
 ## Main results
 
-* the mass calculus: additivity, complements, monotonicity, `mass_le_weight`
+* 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
 * pushforward: `mass_fTransform`, `weight_fTransform`, `fTransform_comp`,
   `fTransform_prod`, `fTransform_equiv_uniform`
 * products: `prod_apply`, `weight_prod`, `mass_prod_fst`, `mass_prod_snd`,
@@ -341,6 +342,45 @@ 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 − |ν|.
+  -- 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
+
 /-- **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
 signed-carrier form of `Finset.single_le_sum` for `Distribution.mass`.