MaxLeafFormal.RSCParams

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

Statements of the paper formalised here: Lemma D.5.21, Lemma D.5.22.

import MaxLeafFormal.RSCCert

/-!
# Rational side conditions for the RSC parameters

For the parameters of `prop:rsc-cert`, proves `lem:rsc-lightpairs`, (C3), `lem:rsc-rsccredits`,
(C6), the remaining scalar hypotheses of `lem:rsc-cert`, and the tree bound conditional on the
data conditions (C1), (C2), (C4), (C5).
-/

namespace MaxLeafFormal.RSCParams

open MaxLeafFormal.RSCCert
open Pointwise
open MaxLeafFormal.Antinorm8 (RTree size PZ fin cZ initInf)

noncomputable section

/-- prop:rsc-cert. -/
def p₂ : ℝ := 7/100

def p₃ : ℝ := 77/1000

def y : ℝ := 31/100

def ϖ₂ : ℝ := 272657/250000

def ϖ₃ : ℝ := 288677/250000

def ê : ℝ := 145729958/189014575

def ν₀ : ℕ := 24

def νE : ℕ := 36

def d₃ (ν : ℕ) : ℕ := if ν = 1 then 3 else if ν = 2 ∨ ν = 3 then 2 else 1

def d₂ (ν : ℕ) : ℕ := if ν = 1 then 4 else if ν = 2 then 3 else if ν = 3 then 2 else 1

/-! ### Rational bounds for the logarithms

Truncation depths of `Real.abs_log_sub_add_sum_range_le`: 6 terms for `log 0.923` and `log 0.93`
(lightness), 10 for `log ϖ₂`, 13 for `log ϖ₃`, 9 for `log q₃` (credits); `log 2` via
`Real.log_two_gt_d9`. -/

lemma yv : y = 31/100 := by norm_num [y]

lemma p2v : p₂ = 7/100 := by norm_num [p₂]

lemma p3v : p₃ = 77/1000 := by norm_num [p₃]

lemma bconstv : bconst p₂ p₃ y = 76/31 := by
  have hm : max p₂ (p₃ - p₂) = 7/100 := by
    rw [p2v, p3v]; exact max_eq_left (by norm_num)
  unfold bconst
  rw [hm, yv]
  norm_num

/-- -log(1 - 77/1000) lies below 8013/100000, via the alternating series bound. -/
lemma log1m077 : -(8013/100000 : ℝ) ≤ Real.log (1 - 77/1000) := by
  have h := Real.abs_log_sub_add_sum_range_le (x := (77/1000 : ℝ))
    (by rw [abs_lt]; constructor <;> norm_num) 6
  rw [abs_le] at h
  obtain ⟨h1, h2⟩ := h
  norm_num [Finset.sum_range_succ, abs_of_pos] at h1 h2 ⊢
  linarith

lemma log1m007 : -(7258/100000 : ℝ) ≤ Real.log (1 - 7/100) := by
  have h := Real.abs_log_sub_add_sum_range_le (x := (7/100 : ℝ))
    (by rw [abs_lt]; constructor <;> norm_num) 6
  rw [abs_le] at h
  obtain ⟨h1, h2⟩ := h
  norm_num [Finset.sum_range_succ, abs_of_pos] at h1 h2 ⊢
  linarith

lemma eps3le : eps p₃ ≤ 8013/100000 := by
  unfold eps
  rw [p3v]
  linarith [log1m077]

lemma eps2le : eps p₂ ≤ 7258/100000 := by
  unfold eps
  rw [p2v]
  linarith [log1m007]

lemma delta3_split : delta₃ p₃ = Real.log 2 + Real.log (1 - 77/1000) := by
  unfold delta₃
  rw [p3v, Real.log_mul (x := 2) (y := 1 - 77/1000) (by norm_num) (by norm_num)]

lemma delta3ge : (6130/10000 : ℝ) ≤ delta₃ p₃ := by
  rw [delta3_split]
  have h2 : (693147/1000000 : ℝ) < Real.log 2 := lt_trans (by norm_num) Real.log_two_gt_d9
  linarith [log1m077]

lemma delta2ge : (6931/10000 : ℝ) ≤ delta₂ := by
  unfold delta₂
  exact le_of_lt (lt_of_le_of_lt (by norm_num) Real.log_two_gt_d9)

lemma thr2 : eps p₂ * y / delta₂ ≤ 325/10000 := by
  have he := eps2le
  have hd := delta2ge
  have hpos : 0 < delta₂ := by linarith
  rw [div_le_iff₀ hpos, yv]
  linarith

lemma thr3 : (1 + p₃ / y) * (eps p₃ * y / delta₃ p₃) ≤ 506/10000 := by
  have he := eps3le
  have hd := delta3ge
  have hpos : 0 < delta₃ p₃ := by linarith
  have h1 : eps p₃ * y / delta₃ p₃ ≤ 4053/100000 := by
    rw [div_le_iff₀ hpos, yv]
    linarith
  have h2 : 1 + p₃ / y = 387/310 := by
    rw [p3v, yv]; norm_num
  rw [h2]
  linarith

lemma light3_of (ν d : ℕ) (h : (506/10000 : ℝ) ≤ (1/2 : ℝ) ^ ν * ((76/31 : ℝ) ^ d)⁻¹) :
    Light₃ p₂ p₃ y ν d := by
  unfold Light₃
  rw [bconstv, ge_iff_le]
  exact le_trans thr3 h

lemma light2_of (ν d : ℕ) (h : (325/10000 : ℝ) ≤ (1/2 : ℝ) ^ ν * ((76/31 : ℝ) ^ d)⁻¹) :
    Light₂ p₂ p₃ y ν d := by
  unfold Light₂
  rw [bconstv, ge_iff_le]
  exact le_trans thr2 h

/-- Upper bound for log ϖ₂ via the alternating series for log(1 - x), x = 1 - ϖ₂. -/
theorem rsccr_log_w2_le : Real.log ϖ₂ ≤ 0.086753678 := by
  have hx : |1 - ϖ₂| < 1 := by
    rw [abs_lt]; constructor <;> norm_num [ϖ₂]
  have hb : |1 - ϖ₂| = 22657/250000 := by
    rw [abs_of_neg (by norm_num [ϖ₂])]; norm_num [ϖ₂]
  have e2 : 1 - ϖ₂ = -(22657/250000) := by norm_num [ϖ₂]
  have h := Real.abs_log_sub_add_sum_range_le hx 10
  rw [sub_sub_cancel, hb] at h
  obtain ⟨h1, h2⟩ := abs_le.mp h
  rw [e2] at h1 h2
  simp only [Finset.sum_range_succ, Finset.sum_range_zero] at h1 h2
  norm_num at h1 h2
  linarith

/-- Upper bound for log ϖ₃ via the alternating series for log(1 - x), x = 1 - ϖ₃. -/
theorem rsccr_log_w3_le : Real.log ϖ₃ ≤ 0.1438474985 := by
  have hx : |1 - ϖ₃| < 1 := by
    rw [abs_lt]; constructor <;> norm_num [ϖ₃]
  have hb : |1 - ϖ₃| = 38677/250000 := by
    rw [abs_of_neg (by norm_num [ϖ₃])]; norm_num [ϖ₃]
  have e3 : 1 - ϖ₃ = -(38677/250000) := by norm_num [ϖ₃]
  have h := Real.abs_log_sub_add_sum_range_le hx 13
  rw [sub_sub_cancel, hb] at h
  obtain ⟨h1, h2⟩ := abs_le.mp h
  rw [e3] at h1 h2
  simp only [Finset.sum_range_succ, Finset.sum_range_zero] at h1 h2
  norm_num at h1 h2
  linarith

/-- Lower bound for log(1 - p₃) = log 0.923 via the alternating series, x = p₃. -/
theorem rsccr_log_q3_ge : -0.0801260445 ≤ Real.log (1 - p₃) := by
  have hx : |p₃| < 1 := by
    rw [abs_lt]; constructor <;> norm_num [p₃]
  have hp : |p₃| = 77/1000 := by
    rw [abs_of_pos (by norm_num [p₃])]; norm_num [p₃]
  have e : 1 - p₃ = 923/1000 := by norm_num [p₃]
  have ep : p₃ = 77/1000 := by norm_num [p₃]
  have h := Real.abs_log_sub_add_sum_range_le hx 9
  rw [hp, e] at h
  rw [e]
  obtain ⟨h1, h2⟩ := abs_le.mp h
  rw [ep] at h1 h2
  simp only [Finset.sum_range_succ, Finset.sum_range_zero] at h1 h2
  norm_num at h1 h2
  linarith

theorem rsccr_credit_i : Real.log ϖ₂ ≤ (1 - rho₁ p₃ y) * delta₂ := by
  have hr : 1 - rho₁ p₃ y = 28613/228613 := by
    unfold rho₁; norm_num [p₃, y]
  rw [hr]
  unfold delta₂
  have := Real.log_two_gt_d9
  linarith [rsccr_log_w2_le]

theorem rsccr_credit_ii : Real.log ϖ₃ ≤ (1 - rho₁ p₃ y ^ 2) * delta₃ p₃ := by
  have hr : 1 - rho₁ p₃ y ^ 2 = 12263903769/52263903769 := by
    unfold rho₁; norm_num [p₃, y]
  rw [hr]
  unfold delta₃
  rw [Real.log_mul (by norm_num) (by norm_num [p₃])]
  have := Real.log_two_gt_d9
  linarith [rsccr_log_w3_le, rsccr_log_q3_ge]

/-- lem:rsc-lightpairs. -/
theorem rsc_lightpairs :
    Light₃ p₂ p₃ y 1 1 ∧ Light₃ p₂ p₃ y 1 2 ∧ Light₃ p₂ p₃ y 2 1 ∧ Light₃ p₂ p₃ y 3 1 ∧
    Light₂ p₂ p₃ y 1 3 ∧ Light₂ p₂ p₃ y 2 2 := by
  refine ⟨light3_of 1 1 (by norm_num), light3_of 1 2 (by norm_num),
    light3_of 2 1 (by norm_num), light3_of 3 1 (by norm_num),
    light2_of 1 3 (by norm_num), light2_of 2 2 (by norm_num)⟩

/-- (C3) for the RSC parameters. -/
theorem rsc_C3 : ∀ ν, 1 ≤ ν → ν ≤ νE →
    (∀ d, 1 ≤ d → d < d₃ ν → Light₃ p₂ p₃ y ν d) ∧
    (∀ d, 1 ≤ d → d < d₂ ν → Light₂ p₂ p₃ y ν d) := by
  intro ν h1 _
  obtain ⟨L1, L2, L3, L4, L5, L6⟩ := rsc_lightpairs
  by_cases hν : 4 ≤ ν
  · have hne1 : ν ≠ 1 := by omega
    have hne2 : ν ≠ 2 := by omega
    have hne3 : ν ≠ 3 := by omega
    have e3 : d₃ ν = 1 := by simp [d₃, hne1, hne2, hne3]
    have e2 : d₂ ν = 1 := by simp [d₂, hne1, hne2, hne3]
    rw [e3, e2]
    exact ⟨fun d hd1 hd2 => absurd hd2 (by omega), fun d hd1 hd2 => absurd hd2 (by omega)⟩
  · have hlt : ν < 4 := by omega
    interval_cases ν
    · have e3 : d₃ 1 = 3 := by simp [d₃]
      have e2 : d₂ 1 = 4 := by simp [d₂]
      rw [e3, e2]
      refine ⟨fun d hd1 hd2 => ?_, fun d hd1 hd2 => ?_⟩
      · interval_cases d
        · exact L1
        · exact L2
      · interval_cases d
        · exact light2_of 1 1 (by norm_num)
        · exact light2_of 1 2 (by norm_num)
        · exact L5
    · have e3 : d₃ 2 = 2 := by simp [d₃]
      have e2 : d₂ 2 = 3 := by simp [d₂]
      rw [e3, e2]
      refine ⟨fun d hd1 hd2 => ?_, fun d hd1 hd2 => ?_⟩
      · interval_cases d
        · exact L3
      · interval_cases d
        · exact light2_of 2 1 (by norm_num)
        · exact L6
    · have e3 : d₃ 3 = 2 := by simp [d₃]
      have e2 : d₂ 3 = 2 := by simp [d₂]
      rw [e3, e2]
      refine ⟨fun d hd1 hd2 => ?_, fun d hd1 hd2 => ?_⟩
      · interval_cases d
        · exact L4
      · interval_cases d
        · exact light2_of 3 1 (by norm_num)

/-- lem:rsc-rsccredits. -/
theorem rsc_rsccredits :
    (1 ≤ ϖ₂ ∧ ϖ₂ ≤ 2 * (1 - p₂) ∧ 1 ≤ ϖ₃ ∧ ϖ₃ ≤ 2 * (1 - p₃)) ∧ Credits p₃ y ϖ₂ ϖ₃ := by
  refine ⟨by norm_num [ϖ₂, ϖ₃, p₂, p₃], ?_⟩
  unfold Credits
  exact ⟨rsccr_credit_i, rsccr_credit_ii⟩

/-- (C6) for the RSC parameters: (q₃/ê)^37 ≥ ê^(−25). -/
theorem rsc_C6 : ((1 - p₃) / ê) ^ (νE + 1) ≥ ê⁻¹ ^ (ν₀ + 1) := by
  norm_num [p₃, ê, νE, ν₀]

/-- The other scalar hypotheses of lem:rsc-cert. -/
theorem rsc_side :
    (0 < p₂ ∧ p₂ ≤ p₃ ∧ p₃ < 1/2) ∧ 0 < y ∧ (0 < ê ∧ ê < 1 - p₃) ∧ 1 ≤ νE ∧
    ∀ ν, 1 ≤ ν → ν ≤ νE → 1 ≤ d₃ ν ∧ d₃ ν ≤ d₂ ν := by
  refine ⟨⟨?_, ?_, ?_⟩, ?_, ⟨?_, ?_⟩, ?_, ?_⟩
  · norm_num [p₂]
  · norm_num [p₂, p₃]
  · norm_num [p₃]
  · norm_num [y]
  · norm_num [ê]
  · norm_num [ê, p₃]
  · norm_num [νE]
  · intro ν h1 h2
    simp only [d₃, d₂]
    split_ifs <;> omega

/-- lem:rsc-cert for the RSC parameters, conditional on the data conditions. -/
theorem rsc_tree_bound_of_data (Z : Finset (Fin 8 → ℝ)) (hZ : Z.Nonempty)
    (hZ0 : ∀ z ∈ Z, 0 ≤ z)
    (C1 : ∀ z ∈ Z, ∀ z' ∈ Z, merge p₂ p₃ z z' ∈ PZ Z)
    (C2 : (∀ ν ≤ ν₀, init p₂ p₃ y ϖ₂ ϖ₃ ν 0 0 ∈ ê ^ (1 + ν) • PZ Z) ∧
          initInf p₂ y ∈ ê ^ (ν₀ + 2) • PZ Z)
    (C4 : ∀ ν, 2 ≤ ν → ν ≤ νE → d₃ ν ≤ 1 →
          (∀ c₃, 1 ≤ c₃ → c₃ ≤ ν - 1 → init p₂ p₃ y ϖ₂ ϖ₃ ν 0 c₃ ∈ ê ^ (1 + ν) • PZ Z) ∧
          (d₂ ν ≤ 1 → ∀ c₂ c₃, 1 ≤ c₂ → c₂ + c₃ ≤ ν - 1 →
             init p₂ p₃ y ϖ₂ ϖ₃ ν c₂ c₃ ∈ ê ^ (1 + ν) • PZ Z))
    (C5 : ∀ ν, 1 ≤ ν → ν ≤ νE → ∀ c₂ c₃, 1 ≤ c₂ + c₃ → c₂ + c₃ ≤ ν →
          ∀ Qs : List (Fin 8 → ℝ), Qs.length = (if c₂ = 0 then jOf d₃ ν else jOf d₂ ν) →
          (∀ Q ∈ Qs, Q ∈ PZ Z ∧ 0 ≤ Q) →
          Qs.foldl (merge p₂ p₃) ((ê ^ (1 + ν))⁻¹ • init p₂ p₃ y ϖ₂ ϖ₃ ν c₂ c₃) ∈ PZ Z)
    (t : RTree Label) (ht : Admissible p₂ p₃ y t) :
    cZ p₂ Z hZ * ê ^ (size t + nuSum t) ≤ fin p₂ (message p₂ p₃ y ϖ₂ ϖ₃ t) := by
  obtain ⟨hp, hy, hê, hνE, hd⟩ := rsc_side
  exact certificate_conditions p₂ p₃ y ϖ₂ ϖ₃ ê hp hy rsc_rsccredits.1 hê Z hZ hZ0 ν₀ νE hνE
    d₃ d₂ hd C1 C2 rsc_C3 C4 C5 rsc_C6 t ht

/-- The scalar hypotheses of the main theorem hold together. -/
example : True := by
  have := rsc_side; have := rsc_C3; have := rsc_rsccredits; have := rsc_C6; trivial

end

end MaxLeafFormal.RSCParams