Testing.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

Testing

Multi-gadget family restoration and common-reference many-hypothesis statistics for every positive success level.

theorem OAI.TraceReconstruction.FiniteLaw.hellingerSq_prod_same_right line 25
def OAI.TraceReconstruction.HellingerTracePair.suffix line 38
theorem OAI.TraceReconstruction.coordinateWord_length_constant line 57
theorem OAI.TraceReconstruction.coordinateWord_injective_equal line 65

theorem OAI.TraceReconstruction.ConcreteLevelPair.restored_family line 83

Source documentation

A fixed family of all binary gadget choices, at exact requested length. Its common-zero member is uniformly close in m-sample TV to every member. This suffices for every fixed positive worst-case success probability.

theorem ConcreteLevelPair.restored_family {r q N Δ d ω F : ℝ} {hr : r∈Set.Icc 0 1}
    {i k : ℕ} (U : ConcreteLevelPair r hr N Δ d ω F i k)
    (hr1 : r<1) (hq : q∈Set.Icc 0 1) (hrq : r≤q) (hk : 1≤k)
    (g n : ℕ) (hN : (g:ℝ)*N≤n) :
    ∃W : (Fin g→Bool)→Word n,Function.Injective W ∧ ∀θ (m : ℕ),
      ((completeTraceLaw q hq (W θ)).product m).tv
        ((completeTraceLaw q hq (W (fun _=>false))).product m) ≤
          Real.sqrt ((m:ℝ)*g*N^(-d))+2*m*g*U.error := by
…

Mentions: OAI.TraceReconstruction.ConcreteLevelPair, OAI.TraceReconstruction.Word, OAI.TraceReconstruction.completeTraceLaw

theorem OAI.TraceReconstruction.FiniteLaw.product_map_expect line 140
theorem OAI.TraceReconstruction.reconstructionSuccess_expect line 162
theorem OAI.TraceReconstruction.IsEstimator.le_one line 169

theorem OAI.TraceReconstruction.family_testing_bound line 176

Source documentation

Many-hypothesis testing using a common reference law. The decoder remains unrestricted, randomized and sees only complete traces.

theorem family_testing_bound {n m g : ℕ} {q s ε : ℝ} (hq : q∈Set.Icc 0 1)
    (W : (Fin g→Bool)→Word n) (hW : Function.Injective W)
    (htv : ∀θ,((completeTraceLaw q hq (W θ)).product m).tv
      ((completeTraceLaw q hq (W (fun _=>false))).product m)≤ε)
    (hm : SufficientBudget n q s m) : s≤1/(2:ℝ)^g+ε := by
…

Mentions: OAI.TraceReconstruction.Word, OAI.TraceReconstruction.completeTraceLaw, OAI.TraceReconstruction.SufficientBudget