OAI/Combinatorics/LowSpaceSubsetSum/Separators/SeparatorEntropy.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

The sharp separator entropy estimate

This is the exact estimate sep:sharp in the manuscript. No positive exponential error is inserted: the maximum is exactly 1 - h(1/4). We use its natural-log expansion and an algebraic certificate for the sign of the second derivative.

  1. def OAI.LowSpaceSubsetSum.separatorAlpha line 17
  2. def OAI.LowSpaceSubsetSum.separatorX line 19
  3. def OAI.LowSpaceSubsetSum.separatorY line 21
  4. def OAI.LowSpaceSubsetSum.separatorZ line 24
  5. def OAI.LowSpaceSubsetSum.separatorW line 27
  6. def OAI.LowSpaceSubsetSum.separatorEntropy line 30
  7. def OAI.LowSpaceSubsetSum.separatorLogEntropy line 34
  8. def OAI.LowSpaceSubsetSum.separatorLogDeriv line 39
  9. def OAI.LowSpaceSubsetSum.separatorLogDeriv2 line 43
  10. theorem OAI.LowSpaceSubsetSum.separatorAlpha_bounds line 47
  11. theorem OAI.LowSpaceSubsetSum.separatorZ_eq line 58
  12. theorem OAI.LowSpaceSubsetSum.separatorW_eq line 62
  13. theorem OAI.LowSpaceSubsetSum.separator_positive line 66
  14. theorem OAI.LowSpaceSubsetSum.hasDerivAt_separatorX line 84
  15. theorem OAI.LowSpaceSubsetSum.hasDerivAt_separatorZ line 87
  16. theorem OAI.LowSpaceSubsetSum.hasDerivAt_separatorW line 92
  17. theorem OAI.LowSpaceSubsetSum.hasDerivAt_separatorLogEntropy line 98
  18. theorem OAI.LowSpaceSubsetSum.hasDerivAt_separatorLogDeriv line 110
  19. theorem OAI.LowSpaceSubsetSum.separatorLogDeriv2_neg line 124

    Source documentation

    An exact factorization certifies the sign without any numerical slack.

    private theorem separatorLogDeriv2_neg {k : ℝ}
    (hk : k ∈ Set.Icc (1 / 6) (1 / 3)) : separatorLogDeriv2 k < 0 := by
…

    Mentions: OAI.LowSpaceSubsetSum.separatorLogDeriv2

  20. theorem OAI.LowSpaceSubsetSum.separatorLogEntropy_concaveOn line 145
  21. theorem OAI.LowSpaceSubsetSum.separatorLogDeriv_quarter line 160
  22. theorem OAI.LowSpaceSubsetSum.separatorLogEntropy_le_quarter line 177
  23. theorem OAI.LowSpaceSubsetSum.binEntropy_perspective line 190
  24. theorem OAI.LowSpaceSubsetSum.separatorEntropy_eq_logEntropy line 202
  25. theorem OAI.LowSpaceSubsetSum.separatorEntropy_quarter line 221
  26. theorem OAI.LowSpaceSubsetSum.separatorEntropy_le line 229

    Source documentation

    The manuscript's sharp separator bound, with no positive exponential error.

    theorem separatorEntropy_le {k : ℝ} (hk : k ∈ Set.Icc (1 / 6) (1 / 3)) :
    separatorEntropy k ≤ 1 - binaryEntropy (1 / 4) := by
…

    Mentions: OAI.LowSpaceSubsetSum.separatorEntropy, OAI.LowSpaceSubsetSum.binaryEntropy