OAI/Combinatorics/HadwigerCounterexample/FiniteEntropy.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

Finite Entropy

  1. def OAI.HadwigerCounterexample.negEnt line 17
  2. def OAI.HadwigerCounterexample.midLaw line 18
  3. theorem OAI.HadwigerCounterexample.tot_continuous line 20
  4. theorem OAI.HadwigerCounterexample.pr_continuous line 22
  5. theorem OAI.HadwigerCounterexample.negEnt_continuous line 24
  6. theorem OAI.HadwigerCounterexample.closed_isLaw line 28
  7. theorem OAI.HadwigerCounterexample.compact_isLaw line 42
  8. theorem OAI.HadwigerCounterexample.negEnt_le_zero line 48
  9. theorem OAI.HadwigerCounterexample.log_bound line 52
  10. theorem OAI.HadwigerCounterexample.log_card_le_negEnt line 65
  11. theorem OAI.HadwigerCounterexample.negEnt_gap_elem line 80
  12. theorem OAI.HadwigerCounterexample.negEnt_gap_on_zero line 89
  13. theorem OAI.HadwigerCounterexample.negEnt_gap line 97

    Source documentation

    Mixing two laws incurs a quantified entropy gap if one gives mass to a set missed by the other. This midpoint bound suffices without a support lemma.

    theorem negEnt_gap {w v : Wgt α} (hw : ∀ x, 0 ≤ w x) (hv : ∀ x, 0 ≤ v x)
    (p : α → Prop) (hp : ∀ x, p x → v x = 0) :
    pr w p * Real.log 2 ≤ negEnt w + negEnt v - 2 * negEnt (midLaw w v) := by
…

    Mentions: OAI.HadwigerCounterexample.Wgt, OAI.HadwigerCounterexample.pr, OAI.HadwigerCounterexample.negEnt, OAI.HadwigerCounterexample.midLaw

  14. theorem OAI.HadwigerCounterexample.mid_tot line 110
  15. theorem OAI.HadwigerCounterexample.midLaw_pr line 114
  16. theorem OAI.HadwigerCounterexample.mid_isLaw line 121