Entropy.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

Entropy bound (10), in normalized trace notation.

def OAI.GeneralMahler.etL line 13
lemma OAI.GeneralMahler.etL_apply line 16
lemma OAI.GeneralMahler.int_etw line 19
lemma OAI.GeneralMahler.etw_add line 25
lemma OAI.GeneralMahler.ProjField.h_weighted line 32
lemma OAI.GeneralMahler.ProjField.logD_cov line 61
theorem OAI.GeneralMahler.ProjField.entropy10 line 68
Source documentation
entropy bound Eq10. Replacing τ log by logD is a notation choice; see trN_logD_eq.
```
theorem entropy10 {T:Mat m} (he:1+T=q.covMat) :
    logD q.covMat - trN T + etw T (q.Hmat v) - q.delt d + eNt q.edge/8 ≤
      Real.log (chi q.C q.V*chi q.D q.U)/m := by
…
```
Mentions: OAI.GeneralMahler.Mat, OAI.GeneralMahler.logD, OAI.GeneralMahler.trN, OAI.GeneralMahler.etw, OAI.GeneralMahler.eNt, OAI.GeneralMahler.chi