OAI/Analysis/FourierLLogL/Compress/Variational.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.FourierLLogL.Compress.Sample line 13
2. def OAI.FourierLLogL.Compress.Emp line 15
3. lemma OAI.FourierLLogL.Compress.Emp_cont line 19
4. lemma OAI.FourierLLogL.Compress.Emp_mixture line 23
5. def OAI.FourierLLogL.Compress.heatMoment line 30

   Source documentation

   Average of exp(-c) on the sum-difference of 2T independent letters.

   def heatMoment (ι : Type) [Fintype ι] [DecidableEq ι] (p : Law α) (tag : α → G) (c : G → ℝ) : ℝ :=
   …

   Mentions: OAI.FourierLLogL.Law

6. lemma OAI.FourierLLogL.Compress.trial_bill_uniform line 37
7. lemma OAI.FourierLLogL.Compress.exp_norm line 52
8. lemma OAI.FourierLLogL.Compress.trial_cost_with_potential line 56

   Source documentation

   The scalar potential dual test used below.

   lemma trial_cost_with_potential (tag : α → G) (c : G → ℝ)
       (E : ℝ) (h : ∀ p : Law α, exp (-E) ≤ heatMoment ι p tag c)
       (a : α → ℝ) :
       ∃ P : Law (Sample ι α G),
         bill tag c (uniform α) P Prod.fst Prod.snd +
           ∑ i : ι, (P.Ex (fun x => a (x.1 i))-(uniform α).Ex a) ≤ E := by
   …

   Mentions: OAI.FourierLLogL.Law, OAI.FourierLLogL.Compress.heatMoment, OAI.FourierLLogL.Compress.Sample, OAI.FourierLLogL.Compress.bill

9. lemma OAI.FourierLLogL.Compress.Emp_linear line 108
10. theorem OAI.FourierLLogL.Compress.noisy_avg line 133

    Source documentation

    Version with uniform averaged one-letter marginal.

    theorem noisy_avg (tag : α → G) (c : G → ℝ) (E : ℝ)
        (h : ∀ p : Law α, exp (-E) ≤ heatMoment ι p tag c) :
        ∃ P : Law (Sample ι α G),
          bill tag c (uniform α) P Prod.fst Prod.snd ≤ E ∧
          Emp P = fun x => Fintype.card ι * uniform α x := by
    …

    Mentions: OAI.FourierLLogL.Law, OAI.FourierLLogL.Compress.heatMoment, OAI.FourierLLogL.Compress.Sample, OAI.FourierLLogL.Compress.bill, OAI.FourierLLogL.Compress.Emp

11. def OAI.FourierLLogL.Compress.appPerm line 162
12. def OAI.FourierLLogL.Compress.exch line 165
13. lemma OAI.FourierLLogL.Compress.same_marginal line 168
14. lemma OAI.FourierLLogL.Compress.Emp_perm line 176
15. theorem OAI.FourierLLogL.Compress.noisy_symm line 184

    Source documentation

    Symmetrize to obtain exact prescribed marginal in each coordinate.

    theorem noisy_symm (tag : α → G) (c : G → ℝ) (E : ℝ)
        (h : ∀ p : Law α, exp (-E) ≤ heatMoment ι p tag c) :
        ∃ P : Law (Sample ι α G),
          bill tag c (uniform α) P Prod.fst Prod.snd ≤ E ∧ exch P ∧
          ∀ i : ι, P.send (fun x => x.1 i) = uniform α := by
    …

    Mentions: OAI.FourierLLogL.Law, OAI.FourierLLogL.Compress.heatMoment, OAI.FourierLLogL.Compress.Sample, OAI.FourierLLogL.Compress.bill, OAI.FourierLLogL.Compress.exch