MaxLeafFormal.RSCheck

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

import MaxLeafFormal.EncloseH

/-!
# RS closed-form rate: the function and the interval checker

`F*(σ) = H(σ) + (1 - σ) log(1 - 2^{-1/σ})` (`eq:rs-F`), and the checker used by the
generated covers `RSCover*.lean`. On `[a, b] ⊆ (0, 1)` the three summands are bounded by
monotonicity, in natural logarithms:
`-σ ln σ ≤ b (-ln a)`, `-(1-σ) ln(1-σ) ≤ (1-a)(-ln(1-b))`,
`(1-σ) ln(1 - 2^{-1/σ}) ≤ (1-b) ln(1 - 2^{-1/a})`, with the rational enclosures of
`MaxLeafFormal.Enclose` at the endpoints. The sum is compared with `T · ln 2`.
The main theorems are in `RSRate.lean`.
-/

namespace MaxLeafFormal.RSRate

open Enclose

/-- The rational `a / b`. -/
def q (a b : ℕ) : ℚ := (a : ℚ) / b

/-- `F*`, the second expression of `eq:rs-F`, for every real `σ`. -/
noncomputable def rsF (σ : ℝ) : ℝ := MLS.H2 σ + (1 - σ) * Real.logb 2 (1 - (2:ℝ) ^ (-1 / σ))

/-- Series terms of the logarithms and of the exponential, and the rounding precision. -/
def nL : ℕ := 32

def nE : ℕ := 12

def pr : ℕ := 40

/-- One interval `[a, b]` with target `T`: the monotone bound of `F* · ln 2` on `[a, b]` lies below
`T` times a lower bound of `ln 2`. -/
def cellOK (T a b : ℚ) : Bool :=
  let L2 := ln2Q nL pr
  let LA := (lnQ a nL pr).lo
  let LB := (lnQ (1 - b) nL pr).lo
  let PL := (expQ (-L2.hi / a) nE pr).lo
  let U := (lnQ (1 - PL) nL pr).hi
  decide (0 ≤ T) && decide (0 < a) && decide (a < b) && decide (b < 1) && decide (PL < 1) &&
    decide (U ≤ 0) && decide (b * (-LA) + (1 - a) * (-LB) + (1 - b) * U < T * L2.lo)

/-- A chain of consecutive intervals `[a, b₁], [b₁, b₂], …, [b_{k-1}, e]`, given by their right
ends `b₁, …, b_k`; the last right end must be `e`. -/
def checkCover (T e : ℚ) : ℚ → List ℚ → Bool
  | _, [] => false
  | a, [b] => cellOK T a b && decide (b = e)
  | a, b :: c :: rest => cellOK T a b && checkCover T e b (c :: rest)

/-- `rsF σ · ln 2 = binEntropy σ + (1 - σ) ln (1 - 2^{-1/σ})`. -/
theorem rsF_mul_log2 (σ : ℝ) :
    rsF σ * Real.log 2 = Real.binEntropy σ + (1 - σ) * Real.log (1 - (2:ℝ) ^ (-1 / σ)) := by
  have h2 : Real.log 2 ≠ 0 := (Real.log_pos (by norm_num : (1:ℝ) < 2)).ne'
  unfold rsF MLS.H2 Real.logb
  field_simp

theorem cellOK_sound {T a b : ℚ} (h : cellOK T a b = true) {σ : ℝ}
    (hσ : σ ∈ Set.Icc (a : ℝ) b) : rsF σ < T := by
  unfold cellOK at h
  simp only [Bool.and_eq_true, decide_eq_true_eq] at h
  obtain ⟨⟨⟨⟨⟨⟨hT, ha⟩, hab⟩, hb⟩, hPL⟩, hU0⟩, hB⟩ := h
  set L2 := ln2Q nL pr with hL2def
  set LA := (lnQ a nL pr).lo with hLAdef
  set LB := (lnQ (1 - b) nL pr).lo with hLBdef
  set PL := (expQ (-L2.hi / a) nE pr).lo with hPLdef
  set U := (lnQ (1 - PL) nL pr).hi with hUdef
  obtain ⟨hσa, hσb⟩ := hσ
  -- enclosures
  have hL2 : L2.Contains (Real.log 2) := ln2Q_sound nL pr
  have hLA : (LA : ℝ) ≤ Real.log a := (lnQ_sound ha nL pr).1
  have hb1 : (0 : ℚ) < 1 - b := by linarith
  have hLB : (LB : ℝ) ≤ Real.log ((1 - b : ℚ) : ℝ) := (lnQ_sound hb1 nL pr).1
  have hPL1 : (0 : ℚ) < 1 - PL := by linarith
  have hU : Real.log ((1 - PL : ℚ) : ℝ) ≤ U := (lnQ_sound hPL1 nL pr).2
  have hPLe : (PL : ℝ) ≤ Real.exp ((-L2.hi / a : ℚ) : ℝ) := (expQ_sound (-L2.hi / a) nE pr).1
  -- real facts
  have ha' : (0 : ℝ) < a := by exact_mod_cast ha
  have hb' : (b : ℝ) < 1 := by exact_mod_cast hb
  have hσ0 : 0 < σ := lt_of_lt_of_le ha' hσa
  have hσ1 : σ < 1 := lt_of_le_of_lt hσb hb'
  have hlog2 : 0 < Real.log 2 := Real.log_pos (by norm_num)
  -- first summand: -σ ln σ ≤ b (-LA)
  have t1 : -σ * Real.log σ ≤ (b : ℝ) * (-(LA : ℝ)) := by
    have e1 : Real.log a ≤ Real.log σ := Real.log_le_log ha' hσa
    have e2 : Real.log σ ≤ 0 := Real.log_nonpos hσ0.le hσ1.le
    have e3 : 0 ≤ -(LA : ℝ) := by linarith
    have e4 : -Real.log σ ≤ -(LA : ℝ) := by linarith
    calc -σ * Real.log σ = σ * (-Real.log σ) := by ring
      _ ≤ σ * (-(LA : ℝ)) := mul_le_mul_of_nonneg_left e4 hσ0.le
      _ ≤ (b : ℝ) * (-(LA : ℝ)) := mul_le_mul_of_nonneg_right hσb e3
  -- second summand: -(1-σ) ln(1-σ) ≤ (1-a)(-LB)
  have t2 : -(1 - σ) * Real.log (1 - σ) ≤ (1 - (a : ℝ)) * (-(LB : ℝ)) := by
    have hcb : ((1 - b : ℚ) : ℝ) = 1 - (b : ℝ) := by push_cast; ring
    rw [hcb] at hLB
    have e1 : Real.log (1 - (b : ℝ)) ≤ Real.log (1 - σ) :=
      Real.log_le_log (by linarith) (by linarith)
    have e2 : Real.log (1 - σ) ≤ 0 := Real.log_nonpos (by linarith) (by linarith)
    have e3 : 0 ≤ -(LB : ℝ) := by linarith
    have e4 : -Real.log (1 - σ) ≤ -(LB : ℝ) := by linarith
    calc -(1 - σ) * Real.log (1 - σ) = (1 - σ) * (-Real.log (1 - σ)) := by ring
      _ ≤ (1 - σ) * (-(LB : ℝ)) := mul_le_mul_of_nonneg_left e4 (by linarith)
      _ ≤ (1 - (a : ℝ)) * (-(LB : ℝ)) := mul_le_mul_of_nonneg_right (by linarith) e3
  -- third summand: (1-σ) ln(1 - 2^{-1/σ}) ≤ (1-b) U
  have t3 : (1 - σ) * Real.log (1 - (2:ℝ) ^ (-1 / σ)) ≤ (1 - (b : ℝ)) * U := by
    have hp : (2:ℝ) ^ (-1 / σ) = Real.exp (Real.log 2 * (-1 / σ)) :=
      Real.rpow_def_of_pos (by norm_num) _
    have hU0' : (U : ℝ) ≤ 0 := by exact_mod_cast hU0
    have hhi : Real.log 2 ≤ (L2.hi : ℝ) := hL2.2
    -- PL ≤ 2^{-1/σ}
    have c1 : ((-L2.hi / a : ℚ) : ℝ) ≤ Real.log 2 * (-1 / σ) := by
      push_cast
      have f1 : -(L2.hi : ℝ) / a ≤ -Real.log 2 / a :=
        div_le_div_of_nonneg_right (by linarith) ha'.le
      have f2 : -Real.log 2 / a ≤ -Real.log 2 / σ := by
        rw [div_le_div_iff₀ ha' hσ0]
        nlinarith
      have f3 : Real.log 2 * (-1 / σ) = -Real.log 2 / σ := by ring
      linarith
    have hPp : (PL : ℝ) ≤ (2:ℝ) ^ (-1 / σ) := by
      rw [hp]; exact hPLe.trans (Real.exp_le_exp.mpr c1)
    have hp1 : (2:ℝ) ^ (-1 / σ) < 1 := by
      rw [hp, Real.exp_lt_one_iff]
      have : -1 / σ < 0 := by rw [neg_div]; exact neg_neg_of_pos (by positivity)
      nlinarith
    have g1 : Real.log (1 - (2:ℝ) ^ (-1 / σ)) ≤ Real.log ((1 - PL : ℚ) : ℝ) := by
      push_cast
      exact Real.log_le_log (by linarith) (by linarith)
    have g2 : Real.log (1 - (2:ℝ) ^ (-1 / σ)) ≤ U := g1.trans hU
    calc (1 - σ) * Real.log (1 - (2:ℝ) ^ (-1 / σ)) ≤ (1 - σ) * U :=
          mul_le_mul_of_nonneg_left g2 (by linarith)
      _ ≤ (1 - (b : ℝ)) * U := mul_le_mul_of_nonpos_right (by linarith) hU0'
  -- assemble
  have hBr : (b : ℝ) * (-(LA : ℝ)) + (1 - (a : ℝ)) * (-(LB : ℝ)) + (1 - (b : ℝ)) * U
      < (T : ℝ) * L2.lo := by exact_mod_cast hB
  have hTl : (T : ℝ) * L2.lo ≤ (T : ℝ) * Real.log 2 :=
    mul_le_mul_of_nonneg_left hL2.1 (by exact_mod_cast hT)
  have hent : Real.binEntropy σ = -σ * Real.log σ + -(1 - σ) * Real.log (1 - σ) := by
    rw [Real.binEntropy_eq_negMulLog_add_negMulLog_one_sub]
    simp only [Real.negMulLog]
  have key : rsF σ * Real.log 2 < (T : ℝ) * Real.log 2 := by
    rw [rsF_mul_log2, hent]
    linarith
  exact lt_of_mul_lt_mul_right key hlog2.le

theorem checkCover_sound_aux {T e : ℚ} :
    ∀ (l : List ℚ) (a : ℚ), checkCover T e a l = true →
      ∀ σ ∈ Set.Icc (a : ℝ) e, rsF σ ≤ T := by
  intro l
  induction l with
  | nil => intro a h; simp [checkCover] at h
  | cons b rest ih =>
    intro a h σ hσ
    cases rest with
    | nil =>
      simp only [checkCover, Bool.and_eq_true, decide_eq_true_eq] at h
      obtain ⟨hc, rfl⟩ := h
      exact (cellOK_sound hc hσ).le
    | cons c rest' =>
      simp only [checkCover, Bool.and_eq_true] at h
      obtain ⟨hc, hr⟩ := h
      rcases le_total σ b with hσb | hσb
      · exact (cellOK_sound hc ⟨hσ.1, hσb⟩).le
      · exact ih b hr σ ⟨hσb, hσ.2⟩

/-- A checked cover proves the bound on the whole range. -/
theorem checkCover_sound {T e a : ℚ} {l : List ℚ} (h : checkCover T e a l = true) :
    ∀ σ ∈ Set.Icc (a : ℝ) e, rsF σ ≤ T :=
  checkCover_sound_aux l a h

end MaxLeafFormal.RSRate