OAI/Probability/TraceReconstruction/Restoration.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.TraceReconstruction.FiniteLaw.approximate_hellinger_transfer line 26
2. def OAI.TraceReconstruction.boundedTraceProjection line 43

   Source documentation

   A total common finite projection. The fallback is never used by a genuine trace of a length-at-most-n input.

   def boundedTraceProjection (n : ℕ) (w : List Bool) : BoundedTrace n :=
   …

   Mentions: OAI.TraceReconstruction.BoundedTrace

3. theorem OAI.TraceReconstruction.boundedTraceProjection_val line 46
4. theorem OAI.TraceReconstruction.listTraceLaw_projection line 50
5. theorem OAI.TraceReconstruction.ApproximatesTrace.projected_tv line 61
6. theorem OAI.TraceReconstruction.HellingerTracePair.sample_tv line 75

   Source documentation

   Restoration for m independent complete observations, not a single concatenated trace.

   theorem HellingerTracePair.sample_tv {q E V : ℝ} {x y : List Bool}
       (C : HellingerTracePair q x y E V) (hq : q∈Set.Icc 0 1)
       (m n : ℕ) (hx : x.length≤n) (hy : y.length≤n) :
       ((listTraceLaw q hq x n hx).product m).tv ((listTraceLaw q hq y n hy).product m) ≤
         Real.sqrt ((m:ℝ)*V)+2*m*E := by
   …

   Mentions: OAI.TraceReconstruction.HellingerTracePair, OAI.TraceReconstruction.listTraceLaw

7. theorem OAI.TraceReconstruction.listDeletionExpectation_comp line 93

   Source documentation

   Independent deletion composes on the actual complete output list.

   theorem listDeletionExpectation_comp (r t : ℝ) (w : List Bool) (F : List Bool→ℝ) :
       listDeletionExpectation r w (fun z=>listDeletionExpectation t z F)=
         listDeletionExpectation (r+(1-r)*t) w F := by
   …

   Mentions: OAI.TraceReconstruction.listDeletionExpectation

8. def OAI.TraceReconstruction.extraDeletion line 103
9. theorem OAI.TraceReconstruction.extraDeletion_bounds line 105
10. theorem OAI.TraceReconstruction.extraDeletion_comp line 112
11. theorem OAI.TraceReconstruction.listTraceLaw_degrade line 117
12. theorem OAI.TraceReconstruction.HellingerTracePair.degraded_sample_tv line 132

    Source documentation

    The requested higher-deletion channel preserves the exact m-sample restoration estimate, through one common per-sample Markov kernel.

    theorem HellingerTracePair.degraded_sample_tv {r q E V : ℝ} {x y : List Bool}
        (C : HellingerTracePair r x y E V) (hr : r∈Set.Ico 0 1) (hq : q∈Set.Icc 0 1)
        (hrq : r≤q) (m n : ℕ) (hx : x.length≤n) (hy : y.length≤n) :
        ((listTraceLaw q hq x n hx).product m).tv ((listTraceLaw q hq y n hy).product m) ≤
          Real.sqrt ((m:ℝ)*V)+2*m*E := by
    …

    Mentions: OAI.TraceReconstruction.HellingerTracePair, OAI.TraceReconstruction.listTraceLaw

13. def OAI.TraceReconstruction.wordOfLength line 157
14. theorem OAI.TraceReconstruction.ofFn_wordOfLength line 159
15. theorem OAI.TraceReconstruction.listTraceLaw_ofFn line 164
16. theorem OAI.TraceReconstruction.listTraceLaw_wordOfLength line 176
17. theorem OAI.TraceReconstruction.ConcreteLevelPair.restored_words line 183

    Source documentation

    Literal exact-length padding and degradation of a level witness.

    theorem ConcreteLevelPair.restored_words {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)
        (n : ℕ) (hN : N≤n) :
        ∃x y : Word n,x≠y ∧ ∀m : ℕ,
          ((completeTraceLaw q hq x).product m).tv ((completeTraceLaw q hq y).product m) ≤
            Real.sqrt ((m:ℝ)*N^(-d))+2*m*U.error := by
    …

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