From df43feee34e2009602b69fecf2a6c4b5481d7f65 Mon Sep 17 00:00:00 2001 From: Marc Ilunga Date: Mon, 12 Oct 2026 17:50:38 +0100 Subject: [PATCH] Identical until bad: a common part, per-step costs, and coupled games MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Systems level (`RandomSystems/Distance/UntilBad.lean`): `transcriptCost β h`, the sum over the steps of a transcript of the cost `β p x` of the query `x` after the prefix `p`. The potential argument, proved once, is `RandomSystem.one_sub_le_sum_tSupp`: if `g` lies below a random system `R`, `g [] = 1`, each step from a possible transcript by an admitted query loses at most `β h x · R h` of `g`, and every possible transcript costs at most `ε`, then the transcripts of a compatible environment within `n` rounds carry at least `1 - ε` of `g` (the union bound over the steps; no source among the references). `RandomSystem.transcriptDistance_le_of_transcriptCost_le` follows: random systems above a common part are within `ε`, via the common-part lemma. A bound per query is the case `β h x = β x`. Games (`RandomSystems/Game/UntilBad.lean`): the part of a game with every MBO unset lies below its visible system, and a step loses from it the probability that the game sets the MBO (`RandomSystem.mass_unsetMBOs_sub_sum_le`). A game that, from every transcript with every MBO unset, sets the MBO at the next query with probability at most `β h x` times the probability of the unset transcript is won with probability at most `ε`, by a deterministic and by a probabilistic distinguisher (the potential argument on the unset part and the visible system, then `exists_unset_winProbability`). `RandomSystem.GameEquivalent.transcriptDistance_visible_le`: two games equivalent as games have the same unset part, a common part of their visible systems, and the per-step costs of the first bound its missing mass, so the visible systems are within `ε` by the systems-level corollary; neither game needs to be monotone, and only the first needs to reply at the queried interface. `PDG.gameEquivalent_behavior_of_isCoupling`: two discrete games with a joint law (Lanzenberger–Maurer, Theorem 2) whose pairs share the condition and answer alike while it does not hold are equivalent as games (CR18, Definition 4.16; Maurer 2002, Definition 5). Below: `Distribution.mass_sub_mass_le_of_le`, the one-sided common-part bound, which needs only the first law to have weight one; `abs_mass_sub_le_of_le` now applies it twice. `RandomSystem.sum_tSupp_succ`, a sum over the transcripts within `m + 1` rounds as a sum over those within `m` rounds and their extensions; `sum_tSupp` now uses it. `RandomSystem.sum_tagMBO`, the replies with both MBOs weigh the transcript, extracted from the proof of `RandomSystem.visible`. THEORY.md §1.5 gets a paragraph; `#print axioms` lines for the five endpoints. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01E7GPy1oUx164NSZsxJT3N9 --- THEORY.md | 68 +++-- src/Probability/Distribution.lean | 66 ++--- src/RandomSystems.lean | 2 + .../Cumulative/CumulativeObservation.lean | 111 +++++--- src/RandomSystems/Distance/UntilBad.lean | 196 ++++++++++++++ src/RandomSystems/Game/MBO.lean | 53 ++-- src/RandomSystems/Game/UntilBad.lean | 254 ++++++++++++++++++ src/Tests/Axioms/Systems.lean | 9 + 8 files changed, 645 insertions(+), 114 deletions(-) create mode 100644 src/RandomSystems/Distance/UntilBad.lean create mode 100644 src/RandomSystems/Game/UntilBad.lean diff --git a/THEORY.md b/THEORY.md index 351b515..b717af8 100644 --- a/THEORY.md +++ b/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 diff --git a/src/Probability/Distribution.lean b/src/Probability/Distribution.lean index 299bfe8..1c74683 100644 --- a/src/Probability/Distribution.lean +++ b/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 diff --git a/src/RandomSystems.lean b/src/RandomSystems.lean index 560aab0..64e17ec 100644 --- a/src/RandomSystems.lean +++ b/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 diff --git a/src/RandomSystems/Cumulative/CumulativeObservation.lean b/src/RandomSystems/Cumulative/CumulativeObservation.lean index 7747260..7c1dd7e 100644 --- a/src/RandomSystems/Cumulative/CumulativeObservation.lean +++ b/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 diff --git a/src/RandomSystems/Distance/UntilBad.lean b/src/RandomSystems/Distance/UntilBad.lean new file mode 100644 index 0000000..634f89f --- /dev/null +++ b/src/RandomSystems/Distance/UntilBad.lean @@ -0,0 +1,196 @@ +import RandomSystems.Distance.Decision + +/-! +# Identical until bad + +Two random systems whose transcript probabilities both lie above a common part `g`, whole at the +empty transcript, are within the probability of leaving the common part. This file bounds that +probability step by step. A step from a possible transcript `h` by an admitted query `x` loses +`g h - ∑ y, g (h ++ [(x, y)])` of the common part; if this is at most `β h x` times the +probability of `h`, and the cost of every possible transcript, the sum of `β` over its steps, is +at most `ε`, then every compatible environment stays in the common part with probability at least +`1 - ε`. This is the union bound over the steps, proved by a potential: the cost of the steps +taken, minus the probability lost, does not decrease in expectation from one round to the next. + +## Main definitions + +* `transcriptCost β h`: the cost of the transcript `h`, the sum of `β` over its steps + +## Main results + +* `RandomSystem.one_sub_le_sum_tSupp`: a compatible environment sees the common part with + probability at least one minus the largest cost of a possible transcript +* `RandomSystem.transcriptDistance_le_of_transcriptCost_le`: two random systems above a common + part are within the largest cost of a possible transcript +-/ + +namespace SystemAlgebra + +open Probability +open scoped NNReal + +section Cost + +variable {A B : Type} + +/-- **The cost of a transcript**: the sum, over the steps of `h`, of the cost `β p x` of the +query `x` after the transcript `p` before it, `∑ₖ β (h₁ ⋯ hₖ) xₖ₊₁`. -/ +def transcriptCost (β : List (A × B) → A → ℝ) : List (A × B) → ℝ + | [] => 0 + | z :: t => β [] z.1 + transcriptCost (fun p x => β (z :: p) x) t + +/-- One more step adds its cost. -/ +theorem transcriptCost_snoc (β : List (A × B) → A → ℝ) (h : List (A × B)) (x : A) (y : B) : + transcriptCost β (h ++ [(x, y)]) = transcriptCost β h + β h x := by + -- Induction on h, for every β: peel the first step off both sides. + induction h generalizing β with + | nil => simp [transcriptCost] + | cons z t ih => + simp only [List.cons_append, transcriptCost, ih] + ring + +end Cost + +namespace RandomSystem + +section Potential + +variable {A B : Type} [Fintype A] [Fintype B] {D : Domain A B} + +/-- **A compatible environment stays in the common part**: if `g` lies below the random system +`R` and is whole at the empty transcript, each step from a possible transcript `h` by an admitted +query `x` loses at most `β h x · R h` of `g`, and every possible transcript costs at most `ε`, +then the transcripts of a compatible strategy `σ` within `n` rounds that `R` makes possible carry +at least `1 - ε` of `g`. This is the union bound over the steps. -/ +theorem one_sub_le_sum_tSupp {R : RandomSystem A B D} {σ : List B →. A} (hC : R.Compatible σ) + {g : List (A × B) → ℝ} (hg : ∀ h, g h ≤ R h) (hnil : g [] = 1) + {β : List (A × B) → A → ℝ} + (hloss : ∀ h x, R h ≠ 0 → D h x → g h - ∑ y, g (h ++ [(x, y)]) ≤ β h x * R h) {ε : ℝ} + (hcost : ∀ h, R h ≠ 0 → transcriptCost β h ≤ ε) (n : ℕ) : + 1 - ε ≤ ∑ h ∈ tSupp R σ n, g h := by + -- Plan. Write c(h) for the cost of h. + -- 1. The potential of a transcript is Φ(h) = c(h)·R(h) − (R(h) − g(h)): the cost of the steps + -- taken, minus the probability lost from g. + -- 2. One step does not decrease it in total: for a possible h and an admitted query x, + -- Φ(h) ≤ Σ_y Φ(h, x, y) over the possible replies y. + -- 3. Round by round, Φ([]) ≤ Σ_h Φ(h) over the transcripts h of σ within n rounds. + -- 4. Φ([]) = 0, c(h) ≤ ε and Σ_h R(h) = 1, so 0 ≤ ε − 1 + Σ_h g(h). + classical + set Φ : List (A × B) → ℝ := fun h => transcriptCost β h * R h - (R h - g h) with hΦ + -- Step 2. + have step : ∀ h x, R h ≠ 0 → D h x → + Φ h ≤ ∑ y ∈ (R.extensionLaw h x).support, Φ (h ++ [(x, y)]) := by + intro h x hp hx + -- The possible replies to x weigh R(h). + have hR := R.sum_extension h x hx + -- Off the possible replies, g ≤ R = 0; so the possible replies carry at least Σ_y g(h, x, y). + have hoff : ∑ y ∈ Finset.univ \ (R.extensionLaw h x).support, g (h ++ [(x, y)]) ≤ 0 := + Finset.sum_nonpos fun y hy => by + have h0 : R (h ++ [(x, y)]) = 0 := by + have := (Finset.mem_sdiff.mp hy).2 + rwa [Finsupp.notMem_support_iff, extensionLaw_apply] at this + exact h0 ▸ hg _ + have hsplit := Finset.sum_sdiff (f := fun y => g (h ++ [(x, y)])) + (Finset.subset_univ (R.extensionLaw h x).support) + -- The step costs β h x: Σ_y Φ(h, x, y) = (c(h) + β h x)·R(h) − R(h) + Σ_y g(h, x, y). + have e : ∑ y ∈ (R.extensionLaw h x).support, Φ (h ++ [(x, y)]) = + (transcriptCost β h + β h x) * R h - R h + + ∑ y ∈ (R.extensionLaw h x).support, g (h ++ [(x, y)]) := by + simp only [hΦ, transcriptCost_snoc] + rw [Finset.sum_sub_distrib, Finset.sum_sub_distrib, ← Finset.mul_sum, hR] + ring + -- With the loss g(h) − Σ_y g(h, x, y) ≤ β h x · R(h), this is at least Φ(h). + rw [e, hΦ] + linarith [hloss h x hp hx] + -- Step 3. + have grow : ∀ m, Φ [] ≤ ∑ h ∈ tSupp R σ m, Φ h := by + intro m + induction m with + | zero => simp [tSupp] + | succ m ih => + -- One more round: each transcript of σ within m rounds is extended by the possible + -- replies to the next query of σ, admitted by compatibility, or kept if σ has stopped. + rw [sum_tSupp_succ] + refine ih.trans (Finset.sum_le_sum fun h hh => ?_) + split_ifs with hd + · exact step h _ (tSupp_possible hh) + (hC h _ (tSupp_good hh).1 (tSupp_possible hh) (Part.get_mem hd)) + · exact le_rfl + -- Step 4. Φ([]) = 0·1 − (1 − 1) = 0. + have hΦnil : Φ [] = 0 := by simp [hΦ, transcriptCost, R.mass_nil, hnil] + -- The transcript law of σ has weight one. + have hone : ∑ h ∈ tSupp R σ n, R h = 1 := by + rw [← sum_tSupp hC n] + exact Finset.sum_congr rfl fun h hh => (if_pos (tSupp_good hh)).symm + -- Σ_h c(h)·R(h) ≤ ε·Σ_h R(h) = ε. + have hcR : ∑ h ∈ tSupp R σ n, transcriptCost β h * R h ≤ ε := by + calc ∑ h ∈ tSupp R σ n, transcriptCost β h * R h ≤ ∑ h ∈ tSupp R σ n, ε * R h := + Finset.sum_le_sum fun h hh => + mul_le_mul_of_nonneg_right (hcost h (tSupp_possible hh)) (R.mass_nonneg h) + _ = ε := by rw [← Finset.mul_sum, hone, mul_one] + have hgrow := grow n + rw [hΦnil, hΦ, Finset.sum_sub_distrib, Finset.sum_sub_distrib] at hgrow + linarith + +end Potential + +variable {I : Type} [Fintype I] {X Y : I → Type} [∀ i, Fintype (X i)] [∀ i, Fintype (Y i)] + {𝒟 : Domain (Σ i, X i) (Σ i, Y i)} + +/-- **Random systems identical until bad are within the cost of their steps**: if `g` lies below +the random systems `R₁` and `R₂` and is whole at the empty transcript, each step of `R₁` from a +possible transcript `h` by an admitted query `x` loses at most `β h x · R₁ h` of `g`, and every +possible transcript of `R₁` costs at most `ε`, then `R₁` is within `ε` of `R₂`. A bound `β x` +per query is the case `β h x = β x`, in which the cost of a transcript is the sum of the costs of +its queries. -/ +theorem transcriptDistance_le_of_transcriptCost_le + {R₁ R₂ : RandomSystem (Σ i, X i) (Σ i, Y i) 𝒟} (hR₁ : R₁.RepliesAtQueriedInterface) + {g : List ((Σ i, X i) × (Σ i, Y i)) → ℝ} (hg₁ : ∀ h, g h ≤ R₁ h) (hg₂ : ∀ h, g h ≤ R₂ h) + (hnil : g [] = 1) {β : List ((Σ i, X i) × (Σ i, Y i)) → (Σ i, X i) → ℝ} + (hloss : ∀ h x, R₁ h ≠ 0 → 𝒟 h x → g h - ∑ y, g (h ++ [(x, y)]) ≤ β h x * R₁ h) + {ε : ℝ≥0} (hcost : ∀ h, R₁ h ≠ 0 → transcriptCost β h ≤ ε) : + R₁.transcriptDistance R₂ ≤ ε := by + -- Plan. Under an environment E compatible with the domain, bounded to n queries: + -- + -- E ──x──▶ R₁ E ──x──▶ R₂ + -- ◀──y── ◀──y── + -- + -- the transcript laws μ₁ and μ₂ both lie above ν, the part of g on the transcripts of E + -- within n rounds that R₁ makes possible, and μ₁ has weight one. So + -- δ(μ₁, μ₂) = μ₁(P) − μ₂(P) (P: the transcripts more likely under R₁) + -- ≤ 1 − |ν| (Distribution.mass_sub_mass_le_of_le) + -- ≤ ε (one_sub_le_sum_tSupp). + classical + refine transcriptDistance_le fun E n _ hc => ?_ + have hC := hc R₁ hR₁ + -- ν: g on the transcripts of E within n rounds that R₁ makes possible. + let ν : Distribution (List ((Σ i, X i) × (Σ i, Y i))) := + Finsupp.onFinset (tSupp R₁ E.1 n) (fun h => if h ∈ tSupp R₁ E.1 n then g h else 0) + fun h hh => by + by_contra hn + exact hh (if_neg hn) + have hν : ∀ h, ν h = if h ∈ tSupp R₁ E.1 n then g h else 0 := fun _ => Finsupp.onFinset_apply + -- ν lies below both transcript laws: on its transcripts both laws are the systems' + -- probabilities, and elsewhere ν is zero. + have below : ∀ R : RandomSystem (Σ i, X i) (Σ i, Y i) 𝒟, (∀ h, g h ≤ R h) → + ∀ h, ν h ≤ R.sLaw E.1 n h := by + intro R hgR h + rw [hν] + split_ifs with hh + · rw [sLaw_apply, if_pos (tSupp_good hh)] + exact hgR h + · exact sLaw_nonNeg n h + -- |ν| ≥ 1 − ε, by the potential argument. + have hw : 1 - (ε : ℝ) ≤ ν.weight := by + rw [Distribution.weight_eq_sum_of_support_subset ν Finsupp.support_onFinset_subset] + refine (one_sub_le_sum_tSupp hC hg₁ hnil hloss hcost n).trans_eq + (Finset.sum_congr rfl fun h hh => ?_) + rw [hν, if_pos hh] + -- δ(μ₁, μ₂) = μ₁(P) − μ₂(P) ≤ 1 − |ν| ≤ ε. + rw [statDist_eq_mass_sub_mass_pos] + linarith [Distribution.mass_sub_mass_le_of_le (R₁.sLaw_isProbDist hC n).2 (below R₁ hg₁) + (below R₂ hg₂) fun h => R₂.sLaw E.1 n h < R₁.sLaw E.1 n h] + +end RandomSystem + +end SystemAlgebra diff --git a/src/RandomSystems/Game/MBO.lean b/src/RandomSystems/Game/MBO.lean index faa7983..c81e3fa 100644 --- a/src/RandomSystems/Game/MBO.lean +++ b/src/RandomSystems/Game/MBO.lean @@ -308,6 +308,32 @@ def RandomSystem.MonotoneMBO {D : Domain A (Σ j, withMBO Y j)} variable {E : List A → Prop} {m : ℕ} {hE : ∀ h, E h → h.length ≤ m} +open scoped Classical in +/-- **The replies with both MBOs** to a query after a transcript `k` weigh `k` if the query is +admitted, and nothing otherwise. -/ +theorem RandomSystem.sum_tagMBO (G : RandomSystem A (Σ j, withMBO Y j) (Domain.ofInputs E m hE)) + (k : List (A × Σ j, withMBO Y j)) (x : A) : + ∑ y : Σ j, Y j, (G (k ++ [(x, tagMBO false y)]) + G (k ++ [(x, tagMBO true y)])) = + if E (k.map Prod.fst ++ [x]) then G k else 0 := by + -- This is the weight of G's extension law at k and x. + have hw := G.extensionLaw_weight k x + rw [Distribution.weight, Finsupp.sum_fintype _ _ (fun _ => rfl)] at hw + simp only [extensionLaw_apply, Domain.ofInputs_apply] at hw + -- Reindex the replies with MBOs as pairs (reply, MBO). + have hsum : ∑ y : Σ j, Y j, + (G (k ++ [(x, tagMBO false y)]) + G (k ++ [(x, tagMBO true y)])) = + ∑ y : Σ j, withMBO Y j, G (k ++ [(x, y)]) := by + let e : (Σ j, Y j) × Bool ≃ Σ j, withMBO Y j := + { toFun := fun p => tagMBO p.2 p.1 + invFun := fun y => (forgetMBO y, y.2.2) + left_inv := fun _ => rfl + right_inv := fun _ => rfl } + rw [Finset.sum_add_distrib, ← e.sum_comp, Fintype.sum_prod_type_right] + simp only [Fintype.sum_bool] + exact add_comm _ _ + rw [hsum, hw] + congr + open scoped Classical in /-- **The visible system** `S⁻` of a game, which ignores the MBO (CR18, Definition 4.18): the probability of a transcript, whatever the MBOs. -/ @@ -323,39 +349,16 @@ noncomputable def RandomSystem.visible -- The weights of the replies y to x after h: y ↦ G⁻ (h ++ [(x, y)]). refine ⟨Finsupp.equivFunOnFinite.symm fun y => sumMBO G (h ++ [(x, y)]), fun y => rfl, ?_⟩ - -- In G, the replies to x after k, with both MBOs, weigh G k if x is admitted, else 0. - have reply : ∀ k : List (A × Σ j, withMBO Y j), - ∑ y : Σ j, Y j, (G (k ++ [(x, tagMBO false y)]) + G (k ++ [(x, tagMBO true y)])) = - if E (k.map Prod.fst ++ [x]) then G k else 0 := by - intro k - -- This is the weight of G's extension law at k and x. - have hw := G.extensionLaw_weight k x - rw [Distribution.weight, Finsupp.sum_fintype _ _ (fun _ => rfl)] at hw - simp only [extensionLaw_apply, Domain.ofInputs_apply] at hw - -- Reindex the replies with MBOs as pairs (reply, MBO). - have hsum : ∑ y : Σ j, Y j, - (G (k ++ [(x, tagMBO false y)]) + G (k ++ [(x, tagMBO true y)])) = - ∑ y : Σ j, withMBO Y j, G (k ++ [(x, y)]) := by - let e : (Σ j, Y j) × Bool ≃ Σ j, withMBO Y j := - { toFun := fun p => tagMBO p.2 p.1 - invFun := fun y => (forgetMBO y, y.2.2) - left_inv := fun _ => rfl - right_inv := fun _ => rfl } - rw [Finset.sum_add_distrib, ← e.sum_comp, Fintype.sum_prod_type_right] - simp only [Fintype.sum_bool] - exact add_comm _ _ - rw [hsum, hw] - congr -- Write (y, b) for the reply y with MBO b and [φ] for the indicator of φ. Then -- Σ_y G⁻ (h ++ [(x, y)]) -- = Σ_y sumMBO (k ↦ G (k ++ [(x, (y, 0))]) + G (k ++ [(x, (y, 1))])) h (sumMBO_snoc) -- = sumMBO (k ↦ Σ_y (G (k ++ [(x, (y, 0))]) + G (k ++ [(x, (y, 1))]))) h (sumMBO_sum) - -- = sumMBO (k ↦ [E (queries of k ++ [x])] · G k) h (reply) + -- = sumMBO (k ↦ [E (queries of k ++ [x])] · G k) h (sum_tagMBO) -- = [E (queries of h ++ [x])] · sumMBO G h (sumMBO_ite) rw [Distribution.weight, Finsupp.sum_fintype _ _ (fun _ => rfl)] simp only [Finsupp.coe_equivFunOnFinite_symm, sumMBO_snoc] rw [← sumMBO_sum] - simp only [reply, Domain.ofInputs_apply] + simp only [G.sum_tagMBO, Domain.ofInputs_apply] exact sumMBO_ite (fun xs => E (xs ++ [x])) G h⟩ theorem RandomSystem.visible_apply diff --git a/src/RandomSystems/Game/UntilBad.lean b/src/RandomSystems/Game/UntilBad.lean new file mode 100644 index 0000000..21f47ce --- /dev/null +++ b/src/RandomSystems/Game/UntilBad.lean @@ -0,0 +1,254 @@ +import RandomSystems.Distance.UntilBad +import RandomSystems.Game.DiscreteMBO +import Probability.Coupling + +/-! +# Games identical until bad + +The part of a game with every MBO unset lies below its visible system, and a step from a +transcript `h` by a query `x` loses from it the probability that the game sets the MBO at `x`. +Suppose that, from every transcript with every MBO unset, the game sets the MBO at the next query +`x` with probability at most `β h x` times the probability of the transcript, and that every +possible transcript costs at most `ε`. The union bound over the steps +(`RandomSystem.one_sub_le_sum_tSupp`) then bounds the mass missing from the unset part along the +transcripts of a winner, which is the winning probability: every winner wins with probability at +most `ε`. Two games equivalent as games have the same unset part, so it is a common part of +their visible systems, and the per-step costs bound its missing mass: the visible systems are +within `ε` (`RandomSystem.transcriptDistance_le_of_transcriptCost_le`). + +Two discrete games are equivalent as games when they are coupled: a joint law of the two whose +pairs have one condition and systems that answer alike while the condition does not hold. + +Sources: CR18, Definition 4.16 (equivalence as games); Maurer 2002, Definition 5; +Lanzenberger–Maurer, Theorem 2 (a joint distribution, or coupling, of two PDSs). + +## Main results + +* `RandomSystem.mass_unsetMBOs_sub_sum_le`: a step loses from the unset part the probability + that the game sets the MBO +* `RandomSystem.winProbability_le_of_transcriptCost_le`, + `Domain.Distinguisher.winProbability_le_of_transcriptCost_le`: a game that sets the MBO at each + step with probability at most the cost of the step is won with probability at most the largest + cost of a possible transcript +* `RandomSystem.GameEquivalent.transcriptDistance_visible_le`: two games equivalent as games, the + first of which sets the MBO at each step with probability at most its cost, have visible + systems within the largest cost of a possible transcript +* `PDG.gameEquivalent_behavior_of_isCoupling`: coupled discrete games whose systems answer alike + while the condition does not hold are equivalent as games +-/ + +namespace SystemAlgebra + +open Probability +open scoped NNReal + +variable {I : Type} [Fintype I] {X Y : I → Type} [∀ i, Fintype (X i)] [∀ i, Fintype (Y i)] + {E : List (Σ i, X i) → Prop} {m : ℕ} {hE : ∀ h, E h → h.length ≤ m} + +/-! ## The unset part of a game -/ + +/-- The part of a game with every MBO unset lies below its visible system: `G (h with every MBO +unset)` is one term of the sum over the MBOs. -/ +theorem RandomSystem.mass_unsetMBOs_le_visible + (G : RandomSystem (Σ i, X i) (Σ i, withMBO Y i) (Domain.ofInputs E m hE)) + (h : List ((Σ i, X i) × Σ i, Y i)) : G (unsetMBOs h) ≤ G.visible h := by + have := le_sumMBO G.mass_nonneg (unsetMBOs h) + rwa [forgetMBOs_unsetMBOs, ← RandomSystem.visible_apply] at this + +/-- **A step loses from the unset part the probability of setting the MBO**: from a transcript +`h` with every MBO unset, the replies to an admitted query `x` with the MBO unset weigh the +probability of `h` with every MBO unset minus the probability that `G` sets the MBO at `x`. So +if that probability is at most `b` times the probability of `h` with every MBO unset, with +`b ≥ 0`, the unset part loses at most `b` times the probability of `h` in the visible system. -/ +theorem RandomSystem.mass_unsetMBOs_sub_sum_le + (G : RandomSystem (Σ i, X i) (Σ i, withMBO Y i) (Domain.ofInputs E m hE)) + {h : List ((Σ i, X i) × Σ i, Y i)} {x : Σ i, X i} (hx : E (h.map Prod.fst ++ [x])) {b : ℝ} + (hb : 0 ≤ b) (hset : ∑ y, G (unsetMBOs h ++ [(x, tagMBO true y)]) ≤ b * G (unsetMBOs h)) : + G (unsetMBOs h) - ∑ y, G (unsetMBOs (h ++ [(x, y)])) ≤ b * G.visible h := by + -- Unsetting the MBOs keeps the queries, and unsets the MBO of the last reply. + have hfst : (unsetMBOs h).map Prod.fst = h.map Prod.fst := by + simp [unsetMBOs, Function.comp_def] + have hsnoc : ∀ y, unsetMBOs (h ++ [(x, y)]) = unsetMBOs h ++ [(x, tagMBO false y)] := + fun y => by simp [unsetMBOs] + -- The replies to the admitted x with both MBOs weigh G(h unset) (sum_tagMBO), so the loss is + -- the probability that G sets the MBO at x. + have hsum := G.sum_tagMBO (unsetMBOs h) x + rw [hfst, if_pos hx, Finset.sum_add_distrib] at hsum + simp only [hsnoc] + calc G (unsetMBOs h) - ∑ y, G (unsetMBOs h ++ [(x, tagMBO false y)]) + = ∑ y, G (unsetMBOs h ++ [(x, tagMBO true y)]) := by linarith + _ ≤ b * G (unsetMBOs h) := hset + -- G(h unset) ≤ G⁻(h), and b ≥ 0. + _ ≤ b * G.visible h := mul_le_mul_of_nonneg_left (G.mass_unsetMBOs_le_visible h) hb + +/-! ## Winning, bounded by the costs of the steps -/ + +/-- **Winning is bounded by the costs of the steps**, for a deterministic distinguisher: if, from +every transcript `h` with every MBO unset, the game `G` sets the MBO at the next admitted query +`x` with probability at most `β h x` times the probability of `h` with every MBO unset, and every +possible transcript of the visible system costs at most `ε`, then `G` is won with probability at +most `ε`. This is the union bound over the steps. -/ +theorem RandomSystem.winProbability_le_of_transcriptCost_le + {G : RandomSystem (Σ i, X i) (Σ i, withMBO Y i) (Domain.ofInputs E m hE)} + (hG : G.RepliesAtQueriedInterface) (hm : G.MonotoneMBO) + {β : List ((Σ i, X i) × Σ i, Y i) → (Σ i, X i) → ℝ} (hβ : ∀ h x, 0 ≤ β h x) + (hset : ∀ h x, E (h.map Prod.fst ++ [x]) → + ∑ y, G (unsetMBOs h ++ [(x, tagMBO true y)]) ≤ β h x * G (unsetMBOs h)) + {ε : ℝ} (hcost : ∀ h, G.visible h ≠ 0 → transcriptCost β h ≤ ε) + (D : DDD I X Y) (hD : IsDDD D) + (hdc : (Domain.ofInputs E m hE : Domain (Σ i, X i) (Σ i, Y i)).DecisionCompatible D) : + G.winProbability D hD ≤ ε := by + -- Plan. The winner is D's environment e, blind to the MBO, for n rounds: + -- + -- ┌────────────────┐ ───── x ─────▶ ┌───┐ + -- │ W = blindMBO e │ │ G │ + -- └────────────────┘ ◀─── (y, a) ── └───┘ + -- + -- Write g(h) = G(h with every MBO 0), the unset part of G, and G⁻ for the visible system. + -- 1. Γ_D(G) = 1 − |ν|, with ν the unset part on the transcripts of e within n rounds + -- (exists_unset_winProbability). + -- 2. g ≤ G⁻, and a step from h by an admitted x loses from g the probability that G sets the + -- MBO at x: + -- g(h) − Σ_y g(h, x, y) = Σ_y G(h unset, (x, (y, 1))) ≤ β h x · g(h) ≤ β h x · G⁻(h). + -- 3. The union bound over the steps, for G⁻ and g (one_sub_le_sum_tSupp): |ν| ≥ 1 − ε. + -- Step 1. + obtain ⟨ν, hν, hwin⟩ := G.exists_unset_winProbability hG hm D hD hdc + set e := ddeOf hD + set n := hD.2.1.choose + -- Step 2. g ≤ G⁻, and the loss of a step (mass_unsetMBOs_sub_sum_le). + have hgV := G.mass_unsetMBOs_le_visible + have hloss : ∀ h x, G.visible h ≠ 0 → (Domain.ofInputs E m hE) h x → + G (unsetMBOs h) - ∑ y, G (unsetMBOs (h ++ [(x, y)])) ≤ β h x * G.visible h := + fun h x _ hx => G.mass_unsetMBOs_sub_sum_le hx (hβ h x) (hset h x hx) + -- Step 3. G⁻ is compatible with e, as D is compatible with the input domain; the union + -- bound over the steps gives the unset part at least 1 − ε on the transcripts of e. + have hpot := G.visible.one_sub_le_sum_tSupp (hdc.environment hD _ hG.visible) hgV G.mass_nil + hloss hcost n + -- |ν| is that mass: ν is the unset part on the transcripts of e, and lives on those that G⁻ + -- makes possible, since g ≤ G⁻. + have hsupp : ν.support ⊆ tSupp G.visible e.1 n := by + intro h hh + rw [Finsupp.mem_support_iff, hν] at hh + split_ifs at hh with hgood + · exact mem_tSupp hgood (ne_of_gt (lt_of_lt_of_le + (lt_of_le_of_ne (G.mass_nonneg _) (Ne.symm hh)) (hgV h))) + · exact absurd rfl hh + have hw : ν.weight = ∑ h ∈ tSupp G.visible e.1 n, G (unsetMBOs h) := by + rw [Distribution.weight_eq_sum_of_support_subset ν hsupp] + exact Finset.sum_congr rfl fun h hh => by rw [hν, if_pos (tSupp_good hh)] + -- Γ_D(G) = 1 − |ν| ≤ ε. + rw [hwin, hw] + linarith + +/-- **Winning is bounded by the costs of the steps**: if, from every transcript `h` with every +MBO unset, the game `G` sets the MBO at the next admitted query `x` with probability at most +`β h x` times the probability of `h` with every MBO unset, and every possible transcript of the +visible system costs at most `ε`, then every distinguisher wins `G` with probability at most +`ε`. -/ +theorem Domain.Distinguisher.winProbability_le_of_transcriptCost_le + (P : (Domain.ofInputs E m hE : Domain (Σ i, X i) (Σ i, Y i)).Distinguisher) + {G : RandomSystem (Σ i, X i) (Σ i, withMBO Y i) (Domain.ofInputs E m hE)} + (hG : G.RepliesAtQueriedInterface) (hm : G.MonotoneMBO) + {β : List ((Σ i, X i) × Σ i, Y i) → (Σ i, X i) → ℝ} (hβ : ∀ h x, 0 ≤ β h x) + (hset : ∀ h x, E (h.map Prod.fst ++ [x]) → + ∑ y, G (unsetMBOs h ++ [(x, tagMBO true y)]) ≤ β h x * G (unsetMBOs h)) + {ε : ℝ} (hcost : ∀ h, G.visible h ≠ 0 → transcriptCost β h ≤ ε) : + P.winProbability G ≤ ε := by + -- Γ_P(G) = Σ_D P(D)·Γ_D(G) ≤ Σ_D P(D)·ε = ε. + calc P.winProbability G ≤ P.1.sum fun _ w => w * ε := by + -- Termwise, by the deterministic case scaled by P(D) ≥ 0. + simp only [Domain.Distinguisher.winProbability, Finsupp.sum] + exact Finset.sum_le_sum fun D _ => mul_le_mul_of_nonneg_left + (RandomSystem.winProbability_le_of_transcriptCost_le hG hm hβ hset hcost D.1 D.2.1 + D.2.2) (P.2.1 D) + _ = ε := by + -- Σ_D P(D)·ε = (Σ_D P(D))·ε = ε, as P's weights sum to 1. + simp only [Finsupp.sum, ← Finset.sum_mul] + rw [show (∑ D ∈ P.1.support, P.1 D) = 1 from P.2.2, one_mul] + +/-- **Games identical until bad**: two games equivalent as games, such that from every +transcript `h` with every MBO unset the first sets the MBO at the next admitted query `x` with +probability at most `β h x` times the probability of `h` with every MBO unset, and every possible +transcript of its visible system costs at most `ε`, have visible systems within `ε`. Equivalence +as games (CR18, Definition 4.16; Maurer 2002, Definition 5) makes the part of the games with every +MBO unset common to both: it lies below both visible systems. The per-step costs bound the mass +missing from it, `RandomSystem.transcriptDistance_le_of_transcriptCost_le`. Neither game needs to +be monotone, and only the first needs to reply at the queried interface. -/ +theorem RandomSystem.GameEquivalent.transcriptDistance_visible_le + {G H : RandomSystem (Σ i, X i) (Σ i, withMBO Y i) (Domain.ofInputs E m hE)} + (hG : G.RepliesAtQueriedInterface) (he : G.GameEquivalent H) + {β : List ((Σ i, X i) × Σ i, Y i) → (Σ i, X i) → ℝ} (hβ : ∀ h x, 0 ≤ β h x) + (hset : ∀ h x, E (h.map Prod.fst ++ [x]) → + ∑ y, G (unsetMBOs h ++ [(x, tagMBO true y)]) ≤ β h x * G (unsetMBOs h)) + {ε : ℝ≥0} (hcost : ∀ h, G.visible h ≠ 0 → transcriptCost β h ≤ ε) : + G.visible.transcriptDistance H.visible ≤ ε := + -- An environment plays the visible systems, which drop the MBO: + -- + -- ┌───┐ ──x──▶ ┌───┐ ┌───┐ ──x──▶ ┌───┐ + -- │ E │ │ G │ ──▶ a (dropped) │ E │ │ H │ ──▶ a (dropped) + -- └───┘ ◀──y── └───┘ └───┘ ◀──y── └───┘ + -- + -- The common part is g(h) = G(h with every MBO 0), whole at the empty transcript: + -- g ≤ G⁻ (one term of the sum over the MBOs) + -- g(h) = H(h with every MBO 0) ≤ H⁻ (equivalence as games, then the same for H) + -- A step of G⁻ loses from g the probability that G sets the MBO, at most β h x · G⁻(h) + -- (mass_unsetMBOs_sub_sum_le), so Δ(G⁻, H⁻) ≤ ε (transcriptDistance_le_of_transcriptCost_le). + RandomSystem.transcriptDistance_le_of_transcriptCost_le hG.visible G.mass_unsetMBOs_le_visible + (fun h => (he h).trans_le (H.mass_unsetMBOs_le_visible h)) G.mass_nil + (fun h x _ hx => G.mass_unsetMBOs_sub_sum_le hx (hβ h x) (hset h x hx)) hcost + +/-! ## Coupled discrete games -/ + +/-- **Coupled discrete games are equivalent as games**: if `J` is a joint distribution of the +discrete games `P₀` and `P₁` (Lanzenberger–Maurer, Theorem 2, printed p. 15: "PDS S ∈ S and +T ∈ T with a joint distribution (or coupling)"), and each pair of deterministic games in its +support has one condition and systems that answer alike while the condition does not hold, then +the games they present are equivalent as games (CR18, Definition 4.16; Maurer 2002, +Definition 5). Two discrete games sampled together, `P₀` and `P₁` the pushforwards of one sample +law `Q` along `f₀` and `f₁`, are the case of `J` the pushforward of `Q` along `(f₀, f₁)`. -/ +theorem PDG.gameEquivalent_behavior_of_isCoupling + {P₀ P₁ : PDG (Σ i, X i) (Σ i, Y i) (Domain.ofInputs E m hE)} (h₀ : P₀.isProbDist) + (h₁ : P₁.isProbDist) + {J : Distribution + ({g : DDG (Σ i, X i) (Σ i, Y i) // HasDomain (Domain.ofInputs E m hE) g.1.1} × + {g : DDG (Σ i, X i) (Σ i, Y i) // HasDomain (Domain.ofInputs E m hE) g.1.1})} + (hJ : Distribution.IsCoupling J P₀ P₁) (condition : ∀ gg ∈ J.support, gg.1.1.2 = gg.2.1.2) + (agree : ∀ gg ∈ J.support, ∀ xs ys, ¬ gg.1.1.2.1 xs → + (Replies gg.1.1.1.1 xs ys ↔ Replies gg.2.1.1.1 xs ys)) : + (P₀.behavior h₀).GameEquivalent (P₁.behavior h₁) := by + -- Each game gives a transcript h with every MBO unset the mass of its deterministic games that + -- reply h with every MBO unset. Both masses are masses of J, the first of an event on the + -- first game of a pair, the second on the second; on each pair in the support of J the two + -- events agree: + -- + -- ┌──────────────┐ + -- │ (g₀, g₁) ~ J │ g₀ ~ P₀, g₁ ~ P₁, one condition c + -- └──────────────┘ + -- g₀ replies h unset ⟺ s₀ replies h ∧ ¬ c(queries of h) + -- ⟺ s₁ replies h ∧ ¬ c(queries of h) (they answer alike until c) + -- ⟺ g₁ replies h unset. + intro h + rcases List.eq_nil_or_concat h with rfl | ⟨p, z, rfl⟩ + -- The empty transcript: both games give it probability one. + · exact ((P₀.behavior h₀).mass_nil).trans ((P₁.behavior h₁).mass_nil).symm + · rw [List.concat_eq_append] + -- Unsetting the MBOs keeps the queries and tags each reply with MBO 0. + have hfst : (unsetMBOs (p ++ [z])).map Prod.fst = (p ++ [z]).map Prod.fst := by + simp [unsetMBOs, Function.comp_def] + have hsnd : (unsetMBOs (p ++ [z])).map Prod.snd = + ((p ++ [z]).map Prod.snd).map (tagMBO false) := by + simp [unsetMBOs, Function.comp_def] + -- Both masses as masses of J: P₀ and P₁ are its marginals. + rw [PDG.behavior_apply, PDG.behavior_apply, ← hJ.1, ← hJ.2, Distribution.mass_fTransform, + Distribution.mass_fTransform] + apply Distribution.mass_congr_of_support + intro gg hgg + -- On a nonempty transcript, a game with the MBO replies it unset iff its system replies it + -- and the condition does not hold (replies_withMBO_unset_iff); the condition is common. + rw [hfst, hsnd, DDG.replies_withMBO_unset_iff _ (by simp), + DDG.replies_withMBO_unset_iff _ (by simp), ← condition gg hgg] + -- While the condition does not hold, the two systems answer alike. + exact ⟨fun ⟨hr, hb⟩ => ⟨(agree gg hgg _ _ hb).mp hr, hb⟩, + fun ⟨hr, hb⟩ => ⟨(agree gg hgg _ _ hb).mpr hr, hb⟩⟩ + +end SystemAlgebra diff --git a/src/Tests/Axioms/Systems.lean b/src/Tests/Axioms/Systems.lean index fc5d3aa..4c8e7bc 100644 --- a/src/Tests/Axioms/Systems.lean +++ b/src/Tests/Axioms/Systems.lean @@ -168,6 +168,10 @@ parallel composition, distance and games, and the counterexamples, depend only o #print axioms SystemAlgebra.envProbe_isDDD #print axioms SystemAlgebra.ddeOf_bounded +-- RandomSystems.Distance.UntilBad +#print axioms SystemAlgebra.RandomSystem.one_sub_le_sum_tSupp +#print axioms SystemAlgebra.RandomSystem.transcriptDistance_le_of_transcriptCost_le + -- RandomSystems.Game.DiscreteMBO #print axioms SystemAlgebra.PDG.visible_behavior #print axioms SystemAlgebra.PDG.monotoneMBO_behavior @@ -198,6 +202,11 @@ parallel composition, distance and games, and the counterexamples, depend only o #print axioms SystemAlgebra.Domain.Distinguisher.exists_absorbAll_winProbability #print axioms SystemAlgebra.Domain.SolverBehavior.absorb +-- RandomSystems.Game.UntilBad +#print axioms SystemAlgebra.Domain.Distinguisher.winProbability_le_of_transcriptCost_le +#print axioms SystemAlgebra.RandomSystem.GameEquivalent.transcriptDistance_visible_le +#print axioms SystemAlgebra.PDG.gameEquivalent_behavior_of_isCoupling + -- RandomSystems.PDS.Function #print axioms SystemAlgebra.DDS.ofFunction #print axioms SystemAlgebra.DDS.replies_ofFunction_iff