MaxLeafFormal.EncloseH

Source file MaxLeafFormal/EncloseH.lean of the Lean project (how it is built).

import MaxLeafFormal.Enclose
import MaxLeafFormal.MLS

/-!
# Enclosures of the binary entropy (continued from `Enclose`)

`MLS.H2 x = binEntropy x / ln 2` at rational points of `(0, 1)`, from the logarithm enclosures of
`MaxLeafFormal.Enclose`.
-/

namespace MaxLeafFormal.Enclose

/-- An enclosure of `binEntropy x = -x ln x - (1 - x) ln (1 - x)`, for `0 < x < 1`. -/
def entQ (x : ℚ) (n prec : ℕ) : QI :=
  ((QI.smul (-x) (lnQ x n prec)).add (QI.smul (-(1 - x)) (lnQ (1 - x) n prec))).round prec

/-- An enclosure of `H2 x = binEntropy x / ln 2`, for `0 < x < 1`. -/
def H2Q (x : ℚ) (n prec : ℕ) : QI := ((entQ x n prec).div (ln2Pos n prec)).round prec

theorem entQ_sound {x : ℚ} (h0 : 0 < x) (h1 : x < 1) (n prec : ℕ) :
    (entQ x n prec).Contains (Real.binEntropy x) := by
  have hx1 : (0 : ℚ) < 1 - x := by linarith
  have hA := QI.smul_sound (-x) (lnQ_sound h0 n prec)
  have hB := QI.smul_sound (-(1 - x)) (lnQ_sound hx1 n prec)
  have hsum := QI.add_sound hA hB
  have e : Real.binEntropy (x : ℝ) = ((-x : ℚ) : ℝ) * Real.log (x : ℝ)
      + ((-(1 - x) : ℚ) : ℝ) * Real.log ((1 - x : ℚ) : ℝ) := by
    rw [Real.binEntropy_eq_negMulLog_add_negMulLog_one_sub]
    simp only [Real.negMulLog]
    push_cast
    ring
  unfold entQ
  rw [e]
  exact QI.round_sound hsum prec

theorem H2Q_sound {x : ℚ} (h0 : 0 < x) (h1 : x < 1) (n prec : ℕ) :
    (H2Q x n prec).Contains (MLS.H2 x) := by
  have hE := entQ_sound h0 h1 n prec
  have hL := ln2Pos_sound' n prec
  have hD := QI.div_sound hE hL.1 hL.2
  unfold H2Q
  unfold MLS.H2
  exact QI.round_sound hD prec

end MaxLeafFormal.Enclose
Back to top