MaxLeafFormal.RSRateAB

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

Statements of the paper formalised here: Proposition 6.1.

import MaxLeafFormal.RSRate

/-!
# RS: parts (a) and (b) of `prop:rs-rate`

The function `f_σ` and the minimiser `τ*` of `sec:rs`, parts (a) and (b) of `prop:rs-rate`, the
minimum value of `f_σ` and the base `2^{F*(σ)}` in closed form, with the denominator of the base as in
`sec:aprime`.

The link lemmas `rsfσ_eq_fσ` and `rsTau_eq_τstar` come before `rs_rate_a`, whose proof uses them.
-/

namespace MaxLeafFormal.RSRateAB

open MaxLeafFormal.RSRate

/-- `f_σ(τ) = H(τ) - σ H(τ/σ) + 1 - τ/σ`. -/
noncomputable def rsfσ (σ τ : ℝ) : ℝ := MLS.H2 τ - σ * MLS.H2 (τ / σ) + 1 - τ / σ

/-- `τ*(σ) = (σ - 2^{-1/σ}) / (1 - 2^{-1/σ})` (`prop:rs-rate`(a)). -/
noncomputable def rsTau (σ : ℝ) : ℝ := (σ - (2:ℝ) ^ (-1 / σ)) / (1 - (2:ℝ) ^ (-1 / σ))

/-- `0 < 2^{-1/σ} < σ < 1` on `(0, 1)`. -/
theorem two_rpow_bounds {σ : ℝ} (hσ : σ ∈ Set.Ioo (0:ℝ) 1) :
    0 < (2:ℝ) ^ (-1 / σ) ∧ (2:ℝ) ^ (-1 / σ) < σ := by
  obtain ⟨h0, _⟩ := hσ
  refine ⟨Real.rpow_pos_of_pos (by norm_num) _, ?_⟩
  have hpos : (0:ℝ) < (2:ℝ) ^ σ⁻¹ := Real.rpow_pos_of_pos (by norm_num) _
  have key := lt_two_rpow (inv_pos.mpr h0).le
  rw [show -1 / σ = -σ⁻¹ by ring, Real.rpow_neg (by norm_num), inv_lt_comm₀ hpos h0]
  exact key

/-! Further lemmas, needed by the proofs of the main theorems. -/

theorem rsfσ_eq_fσ (σ : ℝ) : rsfσ σ = MLS.fσ σ 1 σ⁻¹ := by
  funext τ
  simp only [rsfσ, MLS.fσ]
  ring

theorem rsTau_eq_τstar {σ : ℝ} (hσ : σ ∈ Set.Ioo (0:ℝ) 1) : rsTau σ = MLS.τstar σ σ⁻¹ := by
  have hlt := (two_rpow_bounds hσ).2
  unfold MLS.τstar rsTau
  rw [show -1 / σ = -σ⁻¹ by ring] at hlt ⊢
  split_ifs with h
  · exact absurd h (not_le.mpr hlt)
  · rfl

/-- `prop:rs-rate`(a). -/
theorem rs_rate_a {σ : ℝ} (hσ : σ ∈ Set.Ioo (0:ℝ) 1) :
    rsF σ < MLS.H2 σ ∧ MLS.H2 σ ≤ 1 ∧
    rsTau σ ∈ Set.Ioo 0 σ ∧
    (∀ τ ∈ Set.Icc 0 σ, rsfσ σ (rsTau σ) ≤ rsfσ σ τ) ∧
    (∀ τ ∈ Set.Icc 0 σ, rsfσ σ τ = rsfσ σ (rsTau σ) → τ = rsTau σ) := by
  obtain ⟨hp0, hpσ⟩ := two_rpow_bounds hσ
  obtain ⟨h0, h1⟩ := hσ
  obtain ⟨-, hmem, hiff, hle, -⟩ :=
    MLS.one_sample_size σ 1 σ⁻¹ ⟨h0, h1⟩ zero_le_one (inv_nonneg.mpr h0.le)
  have hval : MLS.fσ σ 1 σ⁻¹ (MLS.τstar σ σ⁻¹) = MLS.Fstar σ 1 σ⁻¹ := (hiff _ hmem).mpr rfl
  refine ⟨?_, ?_, ?_, ?_, ?_⟩
  · have hl : Real.logb 2 (1 - (2:ℝ) ^ (-1 / σ)) < 0 :=
      Real.logb_neg (by norm_num) (by linarith) (by linarith)
    have : (1 - σ) * Real.logb 2 (1 - (2:ℝ) ^ (-1 / σ)) < 0 :=
      mul_neg_of_pos_of_neg (by linarith) hl
    unfold rsF
    linarith
  · unfold MLS.H2
    rw [div_le_one (Real.log_pos one_lt_two)]
    exact Real.binEntropy_le_log_two
  · unfold rsTau
    constructor
    · exact div_pos (by linarith) (by linarith)
    · rw [div_lt_iff₀ (by linarith)]
      nlinarith [mul_pos hp0 (sub_pos.mpr h1)]
  · intro τ hτ
    rw [rsfσ_eq_fσ σ, rsTau_eq_τstar ⟨h0, h1⟩, hval]
    exact hle τ hτ
  · intro τ hτ heq
    rw [rsfσ_eq_fσ σ, rsTau_eq_τstar ⟨h0, h1⟩, hval] at heq
    rw [rsTau_eq_τstar ⟨h0, h1⟩]
    exact (hiff τ hτ).mp heq

/-- The minimum of `f_σ` over `[0, σ]` is `F*(σ)` (from `rem:co-fsigma`). -/
theorem rsfσ_min_eq {σ : ℝ} (hσ : σ ∈ Set.Ioo (0:ℝ) 1) : rsfσ σ (rsTau σ) = rsF σ := by
  obtain ⟨-, hmem, hiff, -, -⟩ :=
    MLS.one_sample_size σ 1 σ⁻¹ hσ zero_le_one (inv_nonneg.mpr hσ.1.le)
  rw [rsfσ_eq_fσ σ, rsTau_eq_τstar hσ, rsF_eq_Fstar hσ]
  exact (hiff _ hmem).mpr rfl

/-- `2^{-1/(1/2)} = 1/4`. -/
theorem two_rpow_half : (2:ℝ) ^ (-1 / (1 / 2) : ℝ) = 1 / 4 := by
  rw [show (-1 / (1 / 2) : ℝ) = -2 by norm_num, Real.rpow_neg (by norm_num), Real.rpow_two]
  norm_num

/-- `H(1/2) = 1`. -/
theorem H2_half : MLS.H2 (1 / 2) = 1 := by
  unfold MLS.H2
  rw [one_div, Real.binEntropy_two_inv, div_self (Real.log_pos one_lt_two).ne']

/-- `prop:rs-rate`(b). -/
theorem rs_rate_b :
    rsTau (1 / 2) = 1 / 3 ∧ rsF (1 / 2) = Real.logb 2 3 / 2 ∧
    (2:ℝ) ^ rsF (1 / 2) = Real.sqrt 3 := by
  have hF : rsF (1 / 2) = Real.logb 2 3 / 2 := by
    have h4 : Real.logb 2 4 = 2 := by
      rw [show (4:ℝ) = (2:ℝ) ^ (2:ℝ) by rw [Real.rpow_two]; norm_num,
        Real.logb_rpow (by norm_num) (by norm_num)]
    unfold rsF
    rw [two_rpow_half, H2_half, show (1:ℝ) - 1 / 4 = 3 / 4 by norm_num,
      Real.logb_div (by norm_num) (by norm_num), h4]
    ring
  refine ⟨?_, hF, ?_⟩
  · unfold rsTau
    rw [two_rpow_half]
    norm_num
  · rw [hF, div_eq_mul_one_div, Real.rpow_mul (by norm_num),
      Real.rpow_logb (by norm_num) (by norm_num) (by norm_num), Real.sqrt_eq_rpow]

theorem rs_rate_b_argmin :
    (1 / 3 : ℝ) ∈ Set.Icc (0:ℝ) (1 / 2) ∧
    (∀ τ ∈ Set.Icc (0:ℝ) (1 / 2), rsfσ (1 / 2) (1 / 3) ≤ rsfσ (1 / 2) τ) ∧
    (∀ τ ∈ Set.Icc (0:ℝ) (1 / 2), rsfσ (1 / 2) τ = rsfσ (1 / 2) (1 / 3) → τ = 1 / 3) := by
  have h := rs_rate_a (σ := 1 / 2) ⟨by norm_num, by norm_num⟩
  rw [rs_rate_b.1] at h
  exact ⟨⟨by norm_num, by norm_num⟩, h.2.2.2.1, h.2.2.2.2⟩

/-- The denominator of the base is `2^{-H(σ)}` (as in `sec:aprime`, at `x = σ`). -/
theorem rs_base_denom {σ : ℝ} (hσ : σ ∈ Set.Ioo (0:ℝ) 1) :
    σ ^ σ * (1 - σ) ^ (1 - σ) = (2:ℝ) ^ (-MLS.H2 σ) := by
  obtain ⟨h0, h1⟩ := hσ
  have hl2 : Real.log 2 ≠ 0 := (Real.log_pos one_lt_two).ne'
  rw [Real.rpow_def_of_pos h0, Real.rpow_def_of_pos (sub_pos.mpr h1),
    Real.rpow_def_of_pos (by norm_num : (0:ℝ) < 2), ← Real.exp_add]
  congr 1
  unfold MLS.H2 Real.binEntropy
  rw [Real.log_inv, Real.log_inv]
  field_simp
  ring

/-- The base `2^{F*(σ)}` in closed form. -/
theorem rs_base {σ : ℝ} (hσ : σ ∈ Set.Ioo (0:ℝ) 1) :
    (2:ℝ) ^ rsF σ = (1 - (2:ℝ) ^ (-1 / σ)) ^ (1 - σ) / (σ ^ σ * (1 - σ) ^ (1 - σ)) := by
  have hq : 0 < 1 - (2:ℝ) ^ (-1 / σ) := by
    have := (two_rpow_bounds hσ).2
    linarith [hσ.2]
  rw [rs_base_denom hσ, Real.rpow_neg (by norm_num), div_inv_eq_mul]
  unfold rsF
  rw [Real.rpow_add (by norm_num), mul_comm (1 - σ), Real.rpow_mul (by norm_num),
    Real.rpow_logb (by norm_num) (by norm_num) hq]
  ring

end MaxLeafFormal.RSRateAB