OAI/Analysis/FourierLLogL/Finite/Law.lean

GitHub source file

78 declarations, 0 contain sorry, 0 declared as axioms

Finite probability tools used in the compression and the dyadic model

  1. def OAI.FourierLLogL.lawSet line 13
  2. abbrev OAI.FourierLLogL.Law line 16
  3. instance OAI.FourierLLogL.(instance at line 18) line 18
  4. instance OAI.FourierLLogL.(instance at line 22) line 22
  5. lemma OAI.FourierLLogL.Law.ext line 48
  6. lemma OAI.FourierLLogL.Law.nonneg line 51
  7. lemma OAI.FourierLLogL.Law.total line 53
  8. lemma OAI.FourierLLogL.Law.mem_nonempty line 55
  9. def OAI.FourierLLogL.Law.Ex line 60
  10. lemma OAI.FourierLLogL.Law.Ex_const line 62
  11. lemma OAI.FourierLLogL.Law.Ex_add line 65
  12. lemma OAI.FourierLLogL.Law.Ex_sub line 69
  13. lemma OAI.FourierLLogL.Law.Ex_mul line 73
  14. lemma OAI.FourierLLogL.Law.Ex_lmul line 77
  15. lemma OAI.FourierLLogL.Law.Ex_neg line 81
  16. lemma OAI.FourierLLogL.Law.Ex_finset_sum line 85
  17. lemma OAI.FourierLLogL.Law.Ex_mono_mem line 91
  18. lemma OAI.FourierLLogL.Law.Ex_mono line 98
  19. lemma OAI.FourierLLogL.Law.Ex_nonneg line 101
  20. lemma OAI.FourierLLogL.Law.Ex_congr_mem line 104
  21. lemma OAI.FourierLLogL.Law.exists_le_Ex line 109
  22. lemma OAI.FourierLLogL.Law.exists_Ex_le line 121
  23. def OAI.FourierLLogL.Law.prob line 126
  24. lemma OAI.FourierLLogL.Law.prob_eq line 128
  25. lemma OAI.FourierLLogL.Law.prob_nonneg line 131
  26. lemma OAI.FourierLLogL.Law.prob_le_one line 134
  27. lemma OAI.FourierLLogL.Law.mem_le_prob line 138
  28. lemma OAI.FourierLLogL.Law.prob_pos_iff line 146
  29. lemma OAI.FourierLLogL.Law.prob_single line 156
  30. lemma OAI.FourierLLogL.Law.prob_compl line 158
  31. lemma OAI.FourierLLogL.Law.ext_of_Ex line 164
  32. def OAI.FourierLLogL.Law.point line 170
  33. lemma OAI.FourierLLogL.Law.point_apply line 174
  34. lemma OAI.FourierLLogL.Law.Ex_point line 180
  35. def OAI.FourierLLogL.Law.uniform line 183
  36. lemma OAI.FourierLLogL.Law.uniform_apply line 186
  37. def OAI.FourierLLogL.Law.through line 189

    Source documentation

    First draw from P, then apply a channel.

    def through (P : Law α) (k : α → Law β) : Law β :=
…

    Mentions: OAI.FourierLLogL.Law

  38. lemma OAI.FourierLLogL.Law.through_apply line 194
  39. lemma OAI.FourierLLogL.Law.Ex_through line 196
  40. def OAI.FourierLLogL.Law.withNext line 203

    Source documentation

    First draw from P, then apply a channel, retaining the original.

    def withNext (P : Law α) (k : α → Law β) : Law (α × β) :=
…

    Mentions: OAI.FourierLLogL.Law

  41. lemma OAI.FourierLLogL.Law.withNext_apply line 208
  42. lemma OAI.FourierLLogL.Law.Ex_withNext line 211
  43. def OAI.FourierLLogL.Law.tensorP line 216
  44. lemma OAI.FourierLLogL.Law.tensorP_apply line 218
  45. lemma OAI.FourierLLogL.Law.Ex_tensorP line 221
  46. def OAI.FourierLLogL.Law.send line 226

    Source documentation

    Law of a function (random variable).

    def send (P : Law α) (X : α → β) : Law β := P.through (fun x => point (X x))

    Mentions: OAI.FourierLLogL.Law, OAI.FourierLLogL.Law.point

  47. lemma OAI.FourierLLogL.Law.send_apply line 228
  48. lemma OAI.FourierLLogL.Law.Ex_send line 231
  49. lemma OAI.FourierLLogL.Law.send_send line 234
  50. lemma OAI.FourierLLogL.Law.send_id line 238
  51. lemma OAI.FourierLLogL.Law.le_send line 241
  52. lemma OAI.FourierLLogL.Law.send_pos line 244
  53. lemma OAI.FourierLLogL.Law.send_pos_iff line 247
  54. lemma OAI.FourierLLogL.Law.send_congr_mem line 250
  55. lemma OAI.FourierLLogL.Law.send_fst_withNext line 256
  56. lemma OAI.FourierLLogL.Law.send_snd_withNext line 261
  57. lemma OAI.FourierLLogL.Law.send_tensorP line 266
  58. lemma OAI.FourierLLogL.Law.send_fst_tensorP line 271
  59. lemma OAI.FourierLLogL.Law.send_snd_tensorP line 274
  60. def OAI.FourierLLogL.Law.condP line 281

    Source documentation

    Conditional distribution on an event; returns the old law when probability is zero.

    def condP (P : Law α) (p : α → Prop) : Law α :=
…

    Mentions: OAI.FourierLLogL.Law

  61. lemma OAI.FourierLLogL.Law.condP_pos_apply line 288
  62. lemma OAI.FourierLLogL.Law.prob_mul_condP line 296
  63. lemma OAI.FourierLLogL.Law.condP_mem line 306
  64. lemma OAI.FourierLLogL.Law.prob_mul_Ex_condP line 311
  65. def OAI.FourierLLogL.Law.after line 318

    Source documentation

    Post law after observing W=b.

    def after (P : Law α) (W : α → β) (b : β) := P.condP (fun x => W x = b)

    Mentions: OAI.FourierLLogL.Law

  66. lemma OAI.FourierLLogL.Law.send_mul_after line 320
  67. lemma OAI.FourierLLogL.Law.after_mem line 325
  68. lemma OAI.FourierLLogL.Law.after_self_pos line 329
  69. lemma OAI.FourierLLogL.Law.after_Ex_sum line 332
  70. lemma OAI.FourierLLogL.Law.through_after line 342
  71. lemma OAI.FourierLLogL.Law.joint_after line 349
  72. lemma OAI.FourierLLogL.Law.after_send_eq_of_send_pair_eq line 359

    Source documentation

    All expectations agree iff the law agrees, so matching after a get operation can be checked by its marginals.

    lemma after_send_eq_of_send_pair_eq {P : Law α} {Q : Law η}
    {X : α → β} {W : α → γ} {Y : η → β} {V : η → γ}
    (h : P.send (fun a => (X a, W a)) = Q.send (fun a => (Y a, V a)))
    (w : γ) :
    (P.after W w).send X = (Q.after V w).send Y := by
…

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

  73. def OAI.FourierLLogL.Law.mixture line 378

    Source documentation

    Binary mixture; real probability t for the first option.

    def mixture (P Q : Law α) (t : ℝ) (h0 : 0 ≤ t) (h1 : t ≤ 1) : Law α :=
…

    Mentions: OAI.FourierLLogL.Law

  74. lemma OAI.FourierLLogL.Law.mixture_apply line 383
  75. lemma OAI.FourierLLogL.Law.mixture_Ex line 386
  76. lemma OAI.FourierLLogL.Law.le_one line 390
  77. def OAI.FourierLLogL.Law.proportional line 396

    Source documentation

    Change density proportionally to a nonnegative function.

    def proportional (w : α → ℝ) (hw : ∀ x, 0 ≤ w x) (ht : 0 < ∑ x, w x) : Law α :=
…

    Mentions: OAI.FourierLLogL.Law

  78. lemma OAI.FourierLLogL.Law.proportional_apply line 399