Side.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

Accounting for the side label

lemma OAI.FourierLLogL.Dyadic.Thermal.cert_S_energy line 14
lemma OAI.FourierLLogL.Dyadic.Thermal.local_channel_energy line 23
lemma OAI.FourierLLogL.Dyadic.Thermal.side_entropy line 42
Source documentation
Absolute information cap wrt a fixed comparison law on z.
```
lemma side_entropy {n : ℕ} {p : Node} {h err : ℝ} {A : Form M}
    (H : Certified h err n p A) (x : Grid M) (hx : x ∈ p.block M) :
    (channel A x).Ex (fun z => log (channel A x z) -
      log (channel (place p M) (p.start M) z)) ≤ F A-log p.invlen+300 := by
…
```
Mentions: OAI.FourierLLogL.Dyadic.Node, OAI.FourierLLogL.Dyadic.Thermal.Form, OAI.FourierLLogL.Dyadic.Thermal.H, OAI.FourierLLogL.Dyadic.Thermal.Certified, OAI.FourierLLogL.Dyadic.Grid, OAI.FourierLLogL.Dyadic.Thermal.channel, OAI.FourierLLogL.Dyadic.Thermal.place, OAI.FourierLLogL.Dyadic.Thermal.F
lemma OAI.FourierLLogL.Dyadic.Thermal.log_input_bound line 60
lemma OAI.FourierLLogL.Dyadic.Thermal.cut_sum_bound line 73
lemma OAI.FourierLLogL.Dyadic.Thermal.log_side_ratio line 81

lemma OAI.FourierLLogL.Dyadic.Thermal.product_entropy_bound line 89

Source documentation

General positive-product estimate. The extra factor of two in the testing volume allows a predictable child mask.

lemma product_entropy_bound {p p' : Node} {a : Grid M → ℝ} (hp : p.ok M) (hv : p.below p')
    {n : ℕ} {h err : ℝ} {A : Form M} (H : Certified h err n p' A)
    {P : Law (Grid M)} (ht : PieceLaw p a P) (hl : l ≤ M) (hh : M-l ≤ p.lev)
    {d : ℝ} (h1 : ∀ x, a x ≤ exp d) (hm : exp (-d) ≤ p.avg a) (B : Bool)
    (Q : Grid l → Grid M → ℝ) (hQ : ∀ x z, 0 < Q x z)
    (hQ' : ∀ z, expU (fun x => Q x z) ≤ 1) :
    (P.withNext (channel A)).Ex (fun xz => if xz.1∈(p.child B).block M then
      log (Q (cut hl xz.1) xz.2) else 0) ≤
        2*d + log p.invlen - log ((2:ℝ)^(M-l)) + F A - log p'.invlen + 301 := by
…

Mentions: OAI.FourierLLogL.Dyadic.Node, OAI.FourierLLogL.Dyadic.Grid, OAI.FourierLLogL.Dyadic.Thermal.Form, OAI.FourierLLogL.Dyadic.Thermal.H, OAI.FourierLLogL.Dyadic.Thermal.Certified, OAI.FourierLLogL.Law, OAI.FourierLLogL.Dyadic.Thermal.PieceLaw, OAI.FourierLLogL.Dyadic.expU, OAI.FourierLLogL.Dyadic.Thermal.channel, OAI.FourierLLogL.Dyadic.cut, OAI.FourierLLogL.Dyadic.Thermal.F