OAI/Analysis/FourierLLogL/Compress/ThinChoice.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.FourierLLogL.Compress.Ticket line 12
2. def OAI.FourierLLogL.Compress.gain line 15
3. lemma OAI.FourierLLogL.Compress.perm_uniform line 19
4. lemma OAI.FourierLLogL.Compress.count_frac line 45
5. lemma OAI.FourierLLogL.Compress.choose_tickets line 54

   Source documentation

   Sampling rule for the realized set of tagged input blocks.

   lemma choose_tickets (r n : ℕ) (hr : 0 < r) (hn : 0 < n) (s : Finset (Fin n)) :
       ∃ k : Law (Ticket r n), ∀ (j : Fin r) (f : Fin n → ℝ),
         k.Ex (gain j f) = if r ≤ s.card then (∑ i ∈ s, f i)/n else 0 := by
   …

   Mentions: OAI.FourierLLogL.Law, OAI.FourierLLogL.Compress.Ticket, OAI.FourierLLogL.Compress.gain

6. def OAI.FourierLLogL.Compress.ratio line 87

   Source documentation

   A numerical tag probability.

   private def ratio (a b : ℝ) := min a b/a

7. lemma OAI.FourierLLogL.Compress.ratio_bounds line 89
8. def OAI.FourierLLogL.Compress.tagChance line 96
9. lemma OAI.FourierLLogL.Compress.tag_test line 100
10. lemma OAI.FourierLLogL.Compress.thin_sampler line 109

    Source documentation

    Build a channel from the underlying input to the rejection/selected rows.

    lemma thin_sampler (r n : ℕ) (hr : 0 < r) (hn : n=2*r) (P : Law Ω) (q : Law A)
        (X : Ω → Fin n → A) (ε : ℝ)
        (hε : ∀ i, ((P.send fun x => X x i).tv q) ≤ ε) :
        ∃ (k : Ω → Law (Ticket r n)),
          let R := P.withNext k
    …

    Mentions: OAI.FourierLLogL.Law, OAI.FourierLLogL.Compress.Ticket