OAI/Analysis/FourierLLogL/Compress/Low.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

Initial estimates for contextual costs

  1. lemma OAI.FourierLLogL.Compress.initial_pack line 16
  2. lemma OAI.FourierLLogL.Compress.G_initial line 22
  3. lemma OAI.FourierLLogL.Compress.K_initial line 29
  4. lemma OAI.FourierLLogL.Compress.I_initial line 37
  5. lemma OAI.FourierLLogL.Compress.trial_initial line 43
  6. lemma OAI.FourierLLogL.Compress.K_initial_le line 62
  7. lemma OAI.FourierLLogL.Compress.exact_zero_g line 70
  8. lemma OAI.FourierLLogL.Compress.I_initial_le line 79
  9. lemma OAI.FourierLLogL.Compress.sum_entropy line 89

    Source documentation

    Compare the entropy of the exact sum with the entropy of the perturbed sum and the error.

    lemma sum_entropy {I : Type} [Fintype I] [DecidableEq I]
    (P : Law Ω) (X : Ω → I → A) (U : Ω → G) (tag : A → G)
    (c : G → ℝ) (hc : ∀ x, 0 ≤ c x) (q : Law A) (hcov : covered P X q)
    (Q : Law G) (hQ : ∀ y, 0 < Q y) (L : ℝ) (hL : ∀ y, -log (Q y) = L+c y) :
    let F := bill tag c q P X U
…

    Mentions: OAI.FourierLLogL.Law, OAI.FourierLLogL.Compress.covered, OAI.FourierLLogL.Compress.bill

  10. structure OAI.FourierLLogL.Compress.Starting line 121
  11. lemma OAI.FourierLLogL.Compress.Starting.cover line 133
  12. lemma OAI.FourierLLogL.Compress.Starting.exact_bound line 135
  13. lemma OAI.FourierLLogL.Compress.Starting.I_upper line 147
  14. lemma OAI.FourierLLogL.Compress.Starting.near_small line 157
  15. lemma OAI.FourierLLogL.Compress.Starting.G_upper line 169
  16. lemma OAI.FourierLLogL.Compress.Starting.block_near line 191
  17. lemma OAI.FourierLLogL.Compress.Starting.block_card line 206
  18. lemma OAI.FourierLLogL.Compress.Starting.K_upper line 225