The H-coefficient bound for random systems

THEORY.md

@@ -158,6 +158,21 @@ with $`D'`$ [sees the transcript law of the system itself][RandomSystem.sLaw_res
 [does not increase the distance][RandomSystem.transcriptDistance_restrict_le],
 $`\Delta(R \restriction D', S \restriction D') \le \Delta(R, S)`$.
 
+**H-coefficient bound**: under an environment $`E`$, the transcript law of $`R`$ gives each
+transcript $`h`$ that $`E`$ produces the probability $`R(h)`$, and the others zero; the restriction
+is the same for $`S`$, so a ratio of the two systems' probabilities on the good transcripts is a
+ratio of their transcript laws. For $`R`$ and $`S`$ replying at the queried label, Patarin's
+H-coefficient technique then
+[bounds the distance][RandomSystem.transcriptDistance_le_add_of_ratio_on_good] by the error
+$`\varepsilon_1`$ of the ratio and the bound $`\varepsilon_2`$ on the bad transcripts under $`S`$:
+
+```math
+(1 - \varepsilon_1)\, S(h) \le R(h) \ \text{ for } h \notin \mathrm{Bad}, \quad
+\Pr_{\mathrm{tr}(S, E, n)}[\mathrm{Bad}] \le \varepsilon_2 \ \text{ for all } E, n
+\quad \Longrightarrow \quad
+\Delta(R, S) \le \varepsilon_1 + \varepsilon_2 .
+```
+
 ### 1.5 Games
 
 A [**game**][RandomSystem.MonotoneMBO] is a random system whose replies carry a bit, the MBO,
@@ -924,6 +939,7 @@ agreeing with a map on a finite set $`S`$: there are $`\lvert Y \rvert^{\lvert X
 [RandomSystem.restrict_restrict]: src/RandomSystems/Distance/Restriction.lean#L67
 [RandomSystem.sLaw_restrict]: src/RandomSystems/Distance/Restriction.lean#L98
 [RandomSystem.transcriptDistance_restrict_le]: src/RandomSystems/Distance/Restriction.lean#L129
+[RandomSystem.transcriptDistance_le_add_of_ratio_on_good]: src/RandomSystems/Distance/HCoefficient.lean#L40
 [MC]: src/RandomSystems/Game/DiscreteMBO.lean#L46
 [DDG]: src/RandomSystems/Game/DiscreteMBO.lean#L50
 [PDG]: src/RandomSystems/Game/DiscreteMBO.lean#L54

src/RandomSystems.lean

@@ -32,6 +32,7 @@ import RandomSystems.Distance.Absorption
 import RandomSystems.Distance.Coupling
 import RandomSystems.Distance.Decision
 import RandomSystems.Distance.Distinguisher
+import RandomSystems.Distance.HCoefficient
 import RandomSystems.Distance.ParallelObservation
 import RandomSystems.Distance.Restriction
 import RandomSystems.Distance.Transcript

src/RandomSystems/Distance/HCoefficient.lean

@@ -0,0 +1,85 @@
+import RandomSystems.Distance.Decision
+
+/-!
+# The H-coefficient bound for random systems
+
+The H-coefficient technique bounds the distance of a real system `R` from an ideal system `S`:
+if every transcript outside a set of bad transcripts is at least `1 - ε₁` times as likely for
+`R` as for `S`, and the bad transcripts have probability at most `ε₂` in the transcript law of
+`S` under every compatible query-bounded environment, the transcript distance is at most
+`ε₁ + ε₂`. The transcript law of a system under an environment is the system's probability of
+the transcript, restricted to the transcripts the environment produces. The restriction is the
+same for both systems, so the ratio of the systems' probabilities is a ratio of their
+transcript laws, and the bound for distributions applies under every environment.
+
+Sources: Patarin's H-coefficient technique, in the form for distributions
+`Probability.statDist_le_probBad_add_of_ratio_on_good`.
+
+## Main results
+
+* `RandomSystem.transcriptDistance_le_add_of_ratio_on_good`: the H-coefficient bound on the
+  transcript distance
+-/
+
+namespace SystemAlgebra
+
+open Probability
+open scoped NNReal
+
+variable {I : Type} [Fintype I] {X Y : I → Type} [∀ i, Fintype (X i)] [∀ i, Fintype (Y i)]
+  {𝒟 : Domain (Σ i, X i) (Σ i, Y i)}
+
+namespace RandomSystem
+
+/-- **The H-coefficient bound for random systems** (Patarin's H-coefficient technique; the
+form for distributions is `statDist_le_probBad_add_of_ratio_on_good`): if every transcript `h`
+outside `Bad` has `(1 - ε₁) · S(h) ≤ R(h)`, where `R(h)` is the probability that `R` replies
+with the replies of `h` to its queries, and under every compatible query-bounded environment
+the bad transcripts have probability at most `ε₂` in the transcript law of the ideal system `S`,
+then the real system `R` is within `ε₁ + ε₂` of `S`. -/
+theorem transcriptDistance_le_add_of_ratio_on_good
+    {R S : RandomSystem (Σ i, X i) (Σ i, Y i) 𝒟}
+    (hR : R.RepliesAtQueriedInterface) (hS : S.RepliesAtQueriedInterface)
+    {Bad : List ((Σ i, X i) × (Σ i, Y i)) → Prop} {ε₁ ε₂ : ℝ≥0}
+    (hratio : ∀ h, ¬ Bad h → (1 - ε₁) * S h ≤ R h)
+    (hbad : ∀ (E : DDE (Σ i, X i) (Σ i, Y i)) (n : ℕ), QueryBounded n E → 𝒟.Compatible E →
+      probBad (S.sLaw E.1 n) Bad ≤ ε₂) :
+    R.transcriptDistance S ≤ ε₁ + ε₂ := by
+  -- Plan:
+  -- 1. The transcript distance is a supremum over environments, so it suffices to bound the
+  --    statistical distance of the transcript laws under one compatible environment `E`,
+  --    bounded to `n` queries:
+  --
+  --        E ──x──▶ R            E ──x──▶ S
+  --          ◀──y──                ◀──y──
+  --       tr(R, E, n)           tr(S, E, n)
+  --
+  -- 2. Both transcript laws are probability distributions.
+  -- 3. The ratio on good transcripts carries over from the systems to the transcript laws.
+  -- 4. The bound for distributions bounds the statistical distance of the transcript laws by
+  --    `Pr_{tr(S, E, n)}[Bad] + ε₁`, which is at most `ε₁ + ε₂`.
+  rw [← ENNReal.coe_add]
+  refine transcriptDistance_le fun E n hn hc => ?_
+  -- Step 2: `E` is compatible with every system on `𝒟` that replies at the queried interface,
+  -- so the transcript laws of `R` and `S` have weight one.
+  have hRlaw := R.sLaw_isProbDist (hc R hR) n
+  have hSlaw := S.sLaw_isProbDist (hc S hS) n
+  -- Step 3: `tr(R, E, n)(h) = [h follows E within n queries] · R(h)`, and likewise for `S`
+  -- with the same indicator. On a transcript `E` produces both sides are the systems'
+  -- probabilities, so the ratio is the hypothesis; elsewhere both sides are zero.
+  have hlaw : ∀ h, ¬ Bad h → (1 - ε₁) * S.sLaw E.1 n h ≤ R.sLaw E.1 n h := by
+    intro h hh
+    rw [sLaw_apply, sLaw_apply]
+    split_ifs
+    · exact hratio h hh
+    · rw [mul_zero]
+  -- Step 4: the H-coefficient bound for distributions, with the law of `R` as the real and
+  -- the law of `S` as the ideal distribution, then the bound `ε₂` on the bad transcripts.
+  have hdist := statDist_le_probBad_add_of_ratio_on_good _ _ Bad ε₁ hRlaw.1 hSlaw.1
+    (hRlaw.weight_eq.trans hSlaw.weight_eq.symm) hSlaw.weight_eq.le hlaw
+  push_cast
+  linarith [hbad E n hn hc]
+
+end RandomSystem
+
+end SystemAlgebra

src/Tests/Axioms/Systems.lean

@@ -150,6 +150,9 @@ parallel composition, distance and games, and the counterexamples, depend only o
 #print axioms SystemAlgebra.Domain.Distinguisher.exists_absorbAll
 #print axioms SystemAlgebra.Domain.Distinguisher.exists_absorbRight
 
+-- RandomSystems.Distance.HCoefficient
+#print axioms SystemAlgebra.RandomSystem.transcriptDistance_le_add_of_ratio_on_good
+
 -- RandomSystems.Distance.ParallelObservation
 #print axioms SystemAlgebra.Domain.DecisionCompatible.absorbRight
 #print axioms SystemAlgebra.RandomSystem.decisionProbability_parallel