Signal.lean`

11 declarations, 0 contain sorry, 0 declared as axioms

Entropy cost of changes of signal

def OAI.FourierLLogL.Law.privateH line 15
Source documentation
expected entropy remaining conditional on a signal channel
```
def privateH (P : Law α) (k : α → Law β) :=
…
```
Mentions: OAI.FourierLLogL.Law
lemma OAI.FourierLLogL.Law.privateH_le line 18
lemma OAI.FourierLLogL.Law.signal_cost line 23
lemma OAI.FourierLLogL.Law.privateH_const line 27
lemma OAI.FourierLLogL.Law.Hcond_compare line 35
lemma OAI.FourierLLogL.Law.Hcond_pair_comm line 48
def OAI.FourierLLogL.Law.triple line 52
theorem OAI.FourierLLogL.Law.refine_signal line 56
Source documentation
Increment cost when jointly revealing two signals; the second may depend on x and first.
```
theorem refine_signal (P : Law α) (k : α → Law β) (v : α × β → Law γ)
    (q : β → Law γ) (hq : ∀ x i, 0 < q x i) :
    let R := triple P k v
…
```
Mentions: OAI.FourierLLogL.Law, OAI.FourierLLogL.Law.triple

theorem OAI.FourierLLogL.Law.replace_signal line 86

Source documentation

When retaining the new signal only, the cost increment is smaller.

theorem replace_signal (P : Law α) (k : α → Law β) (v : α → Law γ)
    (q : β → Law γ) (hq : ∀ x i, 0 < q x i) :
    P.privateH k - P.privateH v ≤
      (P.withNext k).Ex (fun x => (v x.1).kl (q x.2)) := by
…

Mentions: OAI.FourierLLogL.Law, OAI.FourierLLogL.Law.Ex, OAI.FourierLLogL.Law.kl

lemma OAI.FourierLLogL.Law.after_channel line 108
Source documentation
Restriction on a deterministic bit or observation w/o revealing labels
```
lemma after_channel (P : Law α) (f : α → β) (k : α → Law γ)
    {b : β} (h : 0 < P.send f b) :
    (P.withNext k).after (fun x => f x.1) b = (P.after f b).withNext k := by
…
```
Mentions: OAI.FourierLLogL.Law, OAI.FourierLLogL.Law.after, OAI.FourierLLogL.Law.withNext
lemma OAI.FourierLLogL.Law.det_channel line 121