If every candidate's loss is measurable and a.e. valued in [a, b] under Q, every training-generated trajectory is admissible for F, and the resulting uniform-deviation failure event is measurable, then on an i.i.d. panel of size n drawn from Q, measured cumulative empirical-loss progress exceeds population-loss progress by more than 2 · deltaFiniteExperts (card ι) n (b - a) δ with probability at most ENNReal.ofReal δ.
DeclAuditCP.auditBlind_finiteTrajectory_goodhart
∀ {Ωtrain : Type u_1} {Z : Type u_2} {ι : Type u_3} [inst : MeasurableSpace Ωtrain] [inst_1 : MeasurableSpace Z]
[inst_2 : Fintype ι] [Nonempty ι] (μtrain : AuditCP.AuditSampleLaw Ωtrain) [MeasureTheory.IsProbabilityMeasure μtrain]
(Q : AuditCP.AuditSampleLaw Z) [MeasureTheory.IsProbabilityMeasure Q] (n : ℕ),
0 < n →
∀ (a b : ℝ),
a < b →
∀ (δ : ℝ),
0 < δ →
δ ≤ 1 →
∀ (loss : ι → Z → ℝ),
(∀ (i : ι), Measurable (loss i)) →
(∀ (i : ι), ∀ᵐ (z : Z) ∂Q, loss i z ∈ Set.Icc a b) →
∀ (F : Ωtrain → AuditCP.AuditEnvelope ι) (g : Ωtrain → AuditCP.AuditTrajectory ι),
(∀ (t : Ωtrain), AuditCP.Admissible (g t) (F t)) →
MeasurableSet
{p |
¬AuditCP.UniformDev (F p.1) (fun i => AuditCP.empiricalLoss loss i p.2)
(fun i => AuditCP.populationLoss Q loss i)
(AuditCP.deltaFiniteExperts (Fintype.card ι) n (b - a) δ)} →
∀ (T : ℕ),
(MeasureTheory.Measure.prod μtrain (MeasureTheory.Measure.pi fun x => Q))
{p |
AuditCP.cumCP (fun i => AuditCP.empiricalLoss loss i p.2) (g p.1) T >
AuditCP.cumCP (fun i => AuditCP.populationLoss Q loss i) (g p.1) T +
2 * AuditCP.deltaFiniteExperts (Fintype.card ι) n (b - a) δ} ≤
ENNReal.ofReal δTopicAuditing
Arguments
| DOI | Author | Date |
|---|---|---|
| MTH.R-2026-6015 | Dhruv Gupta | 2026-09-24T00:00:00Z |
DOIMTH.C-2026-6015
Cite
Verification
- Library
- AuditCP.StructuralAudit
- Statement digest
- 3b7d52c7568c
- First verified
- 2026-09-24T00:00:00Z