OAI/Analysis/FourierLLogL/Finite/Independent.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

Product laws

  1. def OAI.FourierLLogL.Law.pack line 16
  2. lemma OAI.FourierLLogL.Law.pack_apply line 21
  3. lemma OAI.FourierLLogL.Law.pack_pos line 24
  4. lemma OAI.FourierLLogL.Law.pack_Ex_prod line 35
  5. lemma OAI.FourierLLogL.Law.ext_by_products line 40
  6. lemma OAI.FourierLLogL.Law.sendPack line 57
  7. lemma OAI.FourierLLogL.Law.marginalPack line 65
  8. lemma OAI.FourierLLogL.Law.Ex_pack_proj line 76
  9. lemma OAI.FourierLLogL.Law.sendPack_embedding line 80
  10. lemma OAI.FourierLLogL.Law.crossE_pack line 102
  11. lemma OAI.FourierLLogL.Law.pack_kl line 115
  12. lemma OAI.FourierLLogL.Law.entropy_pack line 122
  13. lemma OAI.FourierLLogL.Law.entropy_coord_bound line 126
  14. lemma OAI.FourierLLogL.Law.H_vec_le line 134
  15. lemma OAI.FourierLLogL.Law.Hcond_vec_le line 139
  16. lemma OAI.FourierLLogL.Law.H_vec_pack line 144
  17. lemma OAI.FourierLLogL.Law.Hcond_vec_pack line 149
  18. lemma OAI.FourierLLogL.Law.pack_withNext line 163

    Source documentation

    Attach an independent new observation per row. When the rows of the initial law are independent, the refined rows remain independent.

    lemma pack_withNext (P : ι → Law α) (Q : ι → α → Law β) :
    ((pack P).withNext (fun v => pack (fun i => Q i (v i)))).send
      (fun (z : (ι→α)×(ι→β)) i => (z.1 i,z.2 i)) =
      pack (fun i => (P i).withNext (Q i)) := by
…

    Mentions: OAI.FourierLLogL.Law, OAI.FourierLLogL.Law.pack, OAI.FourierLLogL.Law.withNext, OAI.FourierLLogL.Law.send