OAI/NumberTheory/TwoPoint/Bounds/DecoderComparison.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.TwoPointCorrelations.uniformAverage_mono line 12
2. lemma OAI.TwoPointCorrelations.uniformAverage_sum line 16
3. lemma OAI.TwoPointCorrelations.abs_uniformAverage_sub_le line 21
4. lemma OAI.TwoPointCorrelations.uniformAverage_coordinate line 30
5. def OAI.TwoPointCorrelations.decodedResidues line 42
6. lemma OAI.TwoPointCorrelations.decodedResidues_jitter line 46
7. lemma OAI.TwoPointCorrelations.decoded_coordinate_error line 55
8. def OAI.TwoPointCorrelations.eventIndicator line 76
9. lemma OAI.TwoPointCorrelations.eventIndicator_difference_le_coordinate_errors line 78
10. theorem OAI.TwoPointCorrelations.decoder_event_error line 105

    Source documentation

    Every event has decoding error at most the sum of the coordinate errors. This statement imposes no circuit assumption; circuits enter only in the comparison of the encoded distributions.

    theorem decoder_event_error {m B : ℕ} (s : Fin m → ℕ) [∀ i, NeZero (s i)]
        (E : (∀ i, ZMod (s i)) → Bool) (r : ∀ i, ZMod (s i)) :
        |eventIndicator E r - uniformAverage (fun j : Fin m → Fin (2 ^ B) =>
          eventIndicator E (decodedResidues s B (crtJitterBits s B r j)))| ≤
            ∑ i : Fin m, (s i : ℝ) / (2 ^ B : ℕ) := by
    …

    Mentions: OAI.TwoPointCorrelations.eventIndicator, OAI.TwoPointCorrelations.uniformAverage, OAI.TwoPointCorrelations.decodedResidues, OAI.TwoPointCorrelations.crtJitterBits

11. theorem OAI.TwoPointCorrelations.decoder_event_error_averaged line 122

    Source documentation

    The same decoder bound holds after averaging over an arbitrary finite law of origins represented as a uniformly sampled finite map.

    theorem decoder_event_error_averaged {α : Type*} [Fintype α] [Nonempty α]
        {m B : ℕ} (s : Fin m → ℕ) [∀ i, NeZero (s i)]
        (E : (∀ i, ZMod (s i)) → Bool) (r : α → ∀ i, ZMod (s i)) :
        |uniformAverage (fun x => eventIndicator E (r x)) -
          uniformAverage (fun x => uniformAverage (fun j : Fin m → Fin (2 ^ B) =>
            eventIndicator E (decodedResidues s B (crtJitterBits s B (r x) j))))| ≤
          ∑ i : Fin m, (s i : ℝ) / (2 ^ B : ℕ) := by
    …

    Mentions: OAI.TwoPointCorrelations.uniformAverage, OAI.TwoPointCorrelations.eventIndicator, OAI.TwoPointCorrelations.decodedResidues, OAI.TwoPointCorrelations.crtJitterBits