APSP in $O(n^{2.99791})$: definitions, part 4 of 5

/-
Copyright (c) 2026 Anthropic, PBC. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
SPDX-License-Identifier: Apache-2.0
-/
-- Generated by skeleton subtraction from the ThreeSumApsp library at commit 27a2fa4bab32.

import Definitions.Def_APSP299791_Defs3

set_option autoImplicit false
set_option relaxedAutoImplicit false

section
-- Source module: ThreeSumApsp.AllEdges.MidClaim
/-!
# Theorem 17 for the all-edges host with the true middle dimension

The all-edges host of `AllEdges/MidHost.lean` declares the inner dimension `midDim D g = ⌈s/g⌉ s`
(with `s = ⌊√D⌋`) for the instances that it hands to the solver of Lop-AE-SparseTri.  So the claim
of Theorem 17 holds with the time of the solver at that dimension (`Claim.Theorem_17_mid`), here
with the parameters `D = ⌊n^{a/b}⌋` and `g = ⌈D^{c/e}⌉` (`claim_ae_theorem_17_mid`).
-/

@[expose] public section

namespace ThreeSumApsp

namespace Claim

/-- **Theorem 17 with the true middle dimension**: as `Claim.Theorem_17`, but the instances of
Lop-AE-SparseTri have the inner dimension `midDim D g = ⌈s/g⌉ s ≤ D` (the middle part `C_k × ℤ_p`
of an instance has `⌈s/g⌉ p ≤ ⌈s/g⌉ s` vertices). -/
def Theorem_17_mid (M : DetTimeModel) (MM : ℕ → ℝ) (D g : ℕ → ℕ) : Prop :=
  ∃ C : ℝ, 0 ≤ C ∧ ∀ T : ℕ → ℕ → ℕ → ℝ, M.lopDetect T →
    ∃ T' : ℕ → ℝ → ℝ, M.exactTriangle T' ∧
      ∀ (n : ℕ) (κ u : ℝ), 16 ≤ D n → D n ≤ n → 1 ≤ g n → (g n : ℝ) ≤ Real.sqrt (D n) → 1 ≤ κ →
        u ≤ (n : ℝ) ^ κ →
        T' n u ≤ 4 * (n : ℝ) * (g n : ℝ) *
            (T n (midDim (D n) (g n)) (queryCap n (D n)) + C * ((n : ℝ) ^ 2 / Real.sqrt (D n))) +
          C * (termScans n (g n) κ + termPrime MM n (D n) + termBuild n (D n) (g n))

end Claim

end ThreeSumApsp

namespace Light.Sec3

open ThreeSumApsp ThreeSumApsp.Spec

/-! ## From a host to the claim -/

/-- The right-hand side of `Claim.Theorem_17_mid`. -/
noncomputable def bound17mid (MM : ℕ → ℝ) (D g : ℕ → ℕ) (C : ℝ) (T : ℕ → ℕ → ℕ → ℝ) (n : ℕ)
    (κ : ℝ) : ℝ :=
  4 * (n : ℝ) * (g n : ℝ) *
      (T n (midDim (D n) (g n)) (queryCap n (D n)) + C * ((n : ℝ) ^ 2 / Real.sqrt (D n))) +
    C * (termScans n (g n) κ + termPrime MM n (D n) + termBuild n (D n) (g n))

/-- The time of a host obeys the bound of `Claim.Theorem_17_mid` with some constant. -/
def ObeysBound17Mid (MM : ℕ → ℝ) (D g : ℕ → ℕ) (time : (List ℕ → ℕ) → ℕ → ℕ → ℕ) : Prop :=
  ∃ C : ℝ, 0 ≤ C ∧ ∀ (Tn : List ℕ → ℕ) (T : ℕ → ℕ → ℕ → ℝ),
    (∀ m d w w' : ℕ, 1 ≤ m → 1 ≤ d → w ≤ w' → (Tn [m, d, w] : ℝ) ≤ T m d w') →
    ∀ (n U : ℕ) (κ : ℝ), 16 ≤ D n → D n ≤ n → 1 ≤ g n → (g n : ℝ) ≤ Real.sqrt (D n) → 1 ≤ κ →
      (U : ℝ) ≤ (n : ℝ) ^ κ → (time Tn n U : ℝ) ≤ bound17mid MM D g C T n κ

/-! ## The need -/

/-! ## The time -/

/-- The time of the all-edges host without the calls of the solver. -/
noncomputable def midRest (tD tG : ℕ → ℕ) (θ : CostParams) : ℕ :=
  fillTime (θ.n * θ.n) + 40 + hostSetup tD tG θ.n θ.D + midHostMain (fun _ => 0) θ.n θ.U θ.D θ.g

noncomputable def restBound_b299791 (θ : CostParams) : ℝ :=
  (θ.n : ℝ) * θ.g * ((θ.n : ℝ) ^ 2 / Real.sqrt θ.D) + budget θ

/-! ## The parameter routines `D = ⌊n^{a/b}⌋`, `g = ⌈D^{c/e}⌉` -/

section params

variable (a b c e : ℕ)

/-- The routines powLt, rootCeil, dr and gr, placed behind a program of length `o`. -/
def ratParamProcs (o : ℕ) : Program :=
  [powLtBody, rootCeilBody o, drBody a b (o + 1), grBody c e (o + 1)]

variable {a b c e}

end params

end Light.Sec3
end
end

section
-- Source module: ThreeSumApsp.AllEdges.Uniform
/-!
# All-edges Exact Triangle in time `n^{3−0.00175}`, for all sizes

Theorem 19 with Corollary 16 for the all-edges host, and brute force below a threshold:
`claim_aeUniform : Claim.ExactTriangleUniform aeModel 0.00175 1`.
-/

@[expose] public section

namespace Light.Sec3

open ThreeSumApsp ThreeSumApsp.Spec

variable {lim : Limits} {d : ℕ}

/-- chooseAE(n, U, ab, bc, ac, out, fr): calls p₁ if n < n₀, and p₂ if not. -/
def aeBySizeBody (n₀ p₁ p₂ : ℕ) : Stmt :=
  .ite (Light.v 0 <' k n₀) (.call p₁ [Light.v 0, Light.v 1, Light.v 2, Light.v 3, Light.v 4, Light.v 5, Light.v 6] 0)
    (.call p₂ [Light.v 0, Light.v 1, Light.v 2, Light.v 3, Light.v 4, Light.v 5, Light.v 6] 0)

end Light.Sec3
end
end

section
-- Source module: ThreeSumApsp.AllEdges.Theorem19Mid
/-!
# Theorem 19 with the true middle dimension and a pruned Lop detection

The computation of the proof of Theorem 19 for another choice of the parameters: Theorem 17 with the
true middle dimension (`Claim.Theorem_17_mid`), with `D = ⌊n^{13/228}⌋` and `g = ⌈D^{11/300}⌉`, and
a detection algorithm for Lop-AE-SparseTri with the saving `D^{0.07618}` in the regime
`D ≤ n^{5/91}` (`Claim.LopDetectP`).  The middle dimension is about `D^{289/300}`, so about
`n^{0.054927}`, below `n^{5/91}`.

1. `Claim.Theorem_19_explicitAt` is `Claim.Theorem_19_explicit` from a threshold `n₀` on, and
   `exactTriangleUniform_of_explicitAt` the bound for all sizes from it.
2. `Theorem19Mid.total_le`: every term of the time is `O(κ n³ D^{-11/300} log² n)`.  The two
   exponent inequalities are `11/300 - (289/300) 0.07618 ≤ -11/300` (the instances, preprocessing
   part) and `11/300 + (289/300) 0.44274 ≤ 1/2 - 11/300` (the instances, query part).
3. `theorem19_mid`: with `D ≥ n^{13/228}/2`, the time is `O(κ n^{3-143/68400} log² n)`, where
   `143/68400 = (11/300)(13/228)`.
4. `claim_aeUniform_mid`: the bound for all sizes for the all-edges host.
-/

@[expose] public section

namespace ThreeSumApsp

/-! ## The claims -/

/-- Lop detection from the pruned thin product with `c = 22`, `θ = 29/250`, in the regime
`D ≤ n^{5/91}`. -/
def Claim.LopDetectP (M : DetTimeModel) : Prop :=
  ∃ (C : ℝ) (Td : ℕ → ℕ → ℕ → ℝ), 0 ≤ C ∧ M.lopDetect Td ∧
    ∀ n D w : ℕ, 2 ≤ D → D ^ 91 ≤ n ^ 5 →
      Td n D w ≤ C * ((n : ℝ) ^ 2 * Real.log D ^ 2 / (D : ℝ) ^ (0.07618 : ℝ)
        + (w : ℝ) * (D : ℝ) ^ (0.44274 : ℝ) * Real.log D + (n : ℝ) * D + w + 1)

/-- `Claim.Theorem_19_explicit` from the size `n₀` on: one algorithm for Exact Triangle that, for
every `n ≥ n₀` and every `κ ≥ 1`, takes time at most `K κ n^{3−δ} (log n)^e` on weights of absolute
value at most `n^κ`. -/
def Claim.Theorem_19_explicitAt (M : DetTimeModel) (δ : ℝ) (e n₀ : ℕ) : Prop :=
  ∃ (K : ℝ) (T : ℕ → ℝ → ℝ), M.exactTriangle T ∧
    ∀ (n : ℕ) (κ u : ℝ), n₀ ≤ n → 1 ≤ κ → u ≤ (n : ℝ) ^ κ →
      T n u ≤ K * (κ * ((n : ℝ) ^ (3 - δ) * Real.log n ^ e))

/-! ## A bound for all sizes from a threshold

As `exactTriangleUniform_of_explicit`, with the threshold `max n₀ 3` in place of `16^18`. -/

namespace Theorem19Mid

/-- The time `uniformTime` without its constant. -/
noncomputable abbrev shape (δ : ℝ) (e : ℕ) (p : SizeBound) : ℝ :=
  (p.s : ℝ) ^ (3 - δ) * (Real.log p.s + 1) ^ e * (1 + logU p.u) ^ 2

end Theorem19Mid

/-! ## The costs added up -/

namespace Theorem19Mid

end Theorem19Mid

end ThreeSumApsp

namespace Light.Sec3

open ThreeSumApsp

end Light.Sec3
end
end

section
-- Source module: ThreeSumApsp.Pruned.CostsAux
/-!
# Helpers for the sharper analysis of Corollary 31

Elementary facts on `φ(y) = y ln y` (tangent-line bounds), the exponent function
`F(u, m, s) = s ln 9 + φ(m) + φ(u-m) - φ(m-s) - φ(u-m+s)` (the logarithm of the proxy for
`β_s / M` with `L = u`), its monotonicity in `s` and in `u`, the binomial ratio bound
`binom(L, k) · k · e^{φ(k) + φ(L-k)}` increasing in `k`, and the upper bound
`binom(n, k) ≤ e^{φ(n) - φ(k) - φ(n-k)}`.
-/

@[expose] public section

open Finset

namespace ThreeSumApsp

namespace PrunedAux

/-- `φ(y) = y ln y`. -/
noncomputable def xlogx (y : ℝ) : ℝ := y * Real.log y

/-- The tangent-line inequality for the convex `φ`: `φ(y) ≥ φ(x) + (y - x)(ln x + 1)`, written as
`y ln y ≥ y ln x + y - x`. -/
theorem tangent {x y : ℝ} (hx : 0 < x) (hy : 0 ≤ y) :
    y * Real.log x + y - x ≤ xlogx y := by
  unfold xlogx
  rcases hy.eq_or_lt with rfl | hy'
  · simp; linarith
  have h := Real.one_sub_inv_le_log_of_pos (div_pos hy' hx)
  rw [Real.log_div hy'.ne' hx.ne', inv_div] at h
  have h2 : y * (1 - x / y) ≤ y * (Real.log y - Real.log x) := mul_le_mul_of_nonneg_left h hy
  have h3 : y * (1 - x / y) = y - x := by field_simp
  nlinarith

/-- `φ(b) - φ(a) ≤ (b - a)(ln b + 1)` for `0 ≤ a`, `0 < b`. -/
theorem sub_le_right {a b : ℝ} (ha : 0 ≤ a) (hb : 0 < b) :
    xlogx b - xlogx a ≤ (b - a) * (Real.log b + 1) := by
  have := tangent hb ha
  unfold xlogx at *
  nlinarith

/-- `φ(b) - φ(a) ≥ (b - a)(ln a + 1)` for `0 < a`, `0 ≤ b`. -/
theorem le_sub_left {a b : ℝ} (ha : 0 < a) (hb : 0 ≤ b) :
    (b - a) * (Real.log a + 1) ≤ xlogx b - xlogx a := by
  have := tangent ha hb
  unfold xlogx at *
  nlinarith

/-- `n^n = e^{φ(n)}` for natural `n` (with `0^0 = 1`). -/
theorem pow_self_eq_exp (n : ℕ) : ((n : ℝ)) ^ n = Real.exp (xlogx n) := by
  unfold xlogx
  rcases Nat.eq_zero_or_pos n with rfl | hn
  · simp
  · rw [Real.exp_nat_mul, Real.exp_log (by exact_mod_cast hn)]

/-- The exponent `F(u, m, s) = s ln 9 + φ(m) + φ(u-m) - φ(m-s) - φ(u-m+s)`. -/
noncomputable def Fexp (u m s : ℝ) : ℝ :=
  s * Real.log 9 + xlogx m + xlogx (u - m) - xlogx (m - s) - xlogx (u - m + s)

/-- `F(u, m, 0) = 0`. -/
theorem Fexp_zero (u m : ℝ) : Fexp u m 0 = 0 := by
  unfold Fexp
  simp

/-- `F` decreases in `s` as long as `9(m - s) ≤ u - m + s`: an explicit bound on the increment. -/
theorem Fexp_sub_le {u m s₁ s₂ : ℝ} (h12 : s₁ ≤ s₂) (h2 : s₂ ≤ m) (h1 : s₁ < m)
    (hpos : 0 < u - m + s₁) :
    Fexp u m s₂ - Fexp u m s₁
      ≤ (s₂ - s₁) * (Real.log 9 + Real.log (m - s₁) - Real.log (u - m + s₁)) := by
  have hA := sub_le_right (a := m - s₂) (b := m - s₁) (by linarith) (by linarith)
  have hB := le_sub_left (a := u - m + s₁) (b := u - m + s₂) hpos (by linarith)
  unfold Fexp
  have e1 : m - s₁ - (m - s₂) = s₂ - s₁ := by ring
  have e2 : u - m + s₂ - (u - m + s₁) = s₂ - s₁ := by ring
  rw [e1] at hA
  rw [e2] at hB
  nlinarith

/-- `F` decreases in `s` where `9(m - s) ≤ u - m + s`. -/
theorem Fexp_anti_s {u m s₁ s₂ : ℝ} (h12 : s₁ ≤ s₂) (h2 : s₂ ≤ m) (h1 : s₁ < m)
    (hpos : 0 < u - m + s₁) (h9 : 9 * (m - s₁) ≤ u - m + s₁) :
    Fexp u m s₂ ≤ Fexp u m s₁ := by
  have h := Fexp_sub_le h12 h2 h1 hpos
  have hlog : Real.log 9 + Real.log (m - s₁) - Real.log (u - m + s₁) ≤ 0 := by
    rw [← Real.log_mul (by norm_num) (by linarith), sub_nonpos]
    exact Real.log_le_log (by nlinarith) h9
  nlinarith [mul_nonpos_of_nonneg_of_nonpos (sub_nonneg.2 h12) hlog]

/-- `F` decreases in `u` on `[u₁, u₁ + s]`. -/
theorem Fexp_anti_u {u₁ u₂ m s : ℝ} (h12 : u₁ ≤ u₂) (h2 : u₂ ≤ u₁ + s) (hpos : 0 < u₁ - m) :
    Fexp u₂ m s ≤ Fexp u₁ m s := by
  have hs : 0 ≤ s := by linarith
  have hA := sub_le_right (a := u₁ - m) (b := u₂ - m) (by linarith) (by linarith)
  have hB := le_sub_left (a := u₁ - m + s) (b := u₂ - m + s) (by linarith) (by linarith)
  have hlog : Real.log (u₂ - m) ≤ Real.log (u₁ - m + s) :=
    Real.log_le_log (by linarith) (by linarith)
  have e1 : u₂ - m - (u₁ - m) = u₂ - u₁ := by ring
  have e2 : u₂ - m + s - (u₁ - m + s) = u₂ - u₁ := by ring
  rw [e1] at hA
  rw [e2] at hB
  unfold Fexp
  nlinarith [mul_le_mul_of_nonneg_left hlog (sub_nonneg.2 h12)]

/-- The explicit value: `F(cx, x, θx) = x ((c-1) ln(c-1) - (1-θ) ln(1-θ) - (c-1+θ) ln(c-1+θ) +
θ ln 9)`. -/
theorem Fexp_scale {c θ x : ℝ} (hc : 1 < c) (hθ1 : θ < 1) (hθ0 : 0 ≤ θ) (hx : 0 < x) :
    Fexp (c * x) x (θ * x)
      = x * ((c - 1) * Real.log (c - 1) - (1 - θ) * Real.log (1 - θ)
          - (c - 1 + θ) * Real.log (c - 1 + θ) + θ * Real.log 9) := by
  unfold Fexp xlogx
  have h1 : Real.log (c * x - x) = Real.log (c - 1) + Real.log x := by
    rw [show c * x - x = (c - 1) * x by ring, Real.log_mul (by linarith) hx.ne']
  have h2 : Real.log (x - θ * x) = Real.log (1 - θ) + Real.log x := by
    rw [show x - θ * x = (1 - θ) * x by ring, Real.log_mul (by linarith) hx.ne']
  have h3 : Real.log (c * x - x + θ * x) = Real.log (c - 1 + θ) + Real.log x := by
    rw [show c * x - x + θ * x = (c - 1 + θ) * x by ring, Real.log_mul (by linarith) hx.ne']
  rw [h1, h2, h3]
  ring

/-- `φ(cx) - φ(x) - φ(cx - x) = x (c ln c - (c-1) ln(c-1))`. -/
theorem xlogx_scale {c x : ℝ} (hc : 1 < c) (hx : 0 < x) :
    xlogx (c * x) - xlogx x - xlogx (c * x - x)
      = x * (c * Real.log c - (c - 1) * Real.log (c - 1)) := by
  unfold xlogx
  rw [show c * x - x = (c - 1) * x by ring, Real.log_mul (by linarith) hx.ne',
    Real.log_mul (by linarith) hx.ne']
  ring

/-- `c H(1/c) = c ln c - (c-1) ln(c-1)`. -/
theorem mul_entropy_inv {c : ℝ} (hc : 1 < c) :
    c * entropy (1 / c) = c * Real.log c - (c - 1) * Real.log (c - 1) := by
  have hc0 : c ≠ 0 := by positivity
  unfold entropy
  rw [show (1 : ℝ) - 1 / c = (c - 1) / c by field_simp,
    Real.log_div (show c - 1 ≠ 0 by linarith) hc0, one_div, Real.log_inv]
  field_simp
  ring

/-- `c H(a/c) = c ln c - a ln a - (c-a) ln(c-a)` for `0 < a < c`. -/
theorem mul_entropy_div {c a : ℝ} (ha : 0 < a) (hac : a < c) :
    c * entropy (a / c) = c * Real.log c - a * Real.log a - (c - a) * Real.log (c - a) := by
  have hc0 : c ≠ 0 := by linarith
  unfold entropy
  rw [show (1 : ℝ) - a / c = (c - a) / c by field_simp,
    Real.log_div (show c - a ≠ 0 by linarith) hc0, Real.log_div ha.ne' hc0]
  field_simp
  ring

/-- The binomial coefficient bounded above by the entropy: `binom(n, k) ≤ e^{φ(n) - φ(k) - φ(n-k)}`.
-/
theorem choose_le_exp (n k : ℕ) (hkn : k ≤ n) :
    (n.choose k : ℝ) ≤ Real.exp (xlogx n - xlogx k - xlogx ((n : ℝ) - k)) := by
  have h := Nat.choose_mul_pow_mul_pow_le k (n - k) n k
  rw [Nat.add_sub_cancel' hkn] at h
  have h' : (n.choose k : ℝ) * (k : ℝ) ^ k * ((n - k : ℕ) : ℝ) ^ (n - k) ≤ (n : ℝ) ^ n := by
    exact_mod_cast h
  rw [pow_self_eq_exp, pow_self_eq_exp, pow_self_eq_exp, Nat.cast_sub hkn] at h'
  rw [sub_sub, Real.exp_sub, le_div_iff₀ (Real.exp_pos _), Real.exp_add]
  linarith [h']

/-- The proxy `binom(L, k) · k · e^{φ(k) + φ(L-k)}` increases with `k` by one step. -/
theorem ratio_step (L k : ℕ) (hk : k < L) :
    (L.choose k : ℝ) * k * Real.exp (xlogx k + xlogx ((L : ℝ) - k))
      ≤ (L.choose (k + 1) : ℝ) * ((k + 1 : ℕ) : ℝ)
          * Real.exp (xlogx ((k + 1 : ℕ) : ℝ) + xlogx ((L : ℝ) - ((k + 1 : ℕ) : ℝ))) := by
  rcases Nat.eq_zero_or_pos k with rfl | hk0
  · simp only [Nat.cast_zero, mul_zero, zero_mul]
    positivity
  have hrec : (L.choose (k + 1) : ℝ) * ((k + 1 : ℕ) : ℝ) = (L.choose k : ℝ) * ((L : ℝ) - k) := by
    have := Nat.choose_succ_right_eq L k
    rw [← Nat.cast_sub hk.le]
    exact_mod_cast this
  rw [hrec]
  have hk' : (0 : ℝ) < k := by exact_mod_cast hk0
  have hkL : (k : ℝ) + 1 ≤ L := by exact_mod_cast hk
  push_cast
  -- `φ(k+1) - φ(k) ≥ ln k + 1` and `φ(L-k) - φ(L-k-1) ≤ ln(L-k) + 1`
  have hA := le_sub_left (a := (k : ℝ)) (b := (k : ℝ) + 1) hk' (by linarith)
  have hB := sub_le_right (a := (L : ℝ) - (k + 1)) (b := (L : ℝ) - k) (by linarith) (by linarith)
  have e1 : (k : ℝ) + 1 - k = 1 := by ring
  have e2 : (L : ℝ) - k - ((L : ℝ) - (k + 1)) = 1 := by ring
  rw [e1, one_mul] at hA
  rw [e2, one_mul] at hB
  have hexp : Real.exp (xlogx k + xlogx ((L : ℝ) - k))
      ≤ Real.exp (xlogx ((k : ℝ) + 1) + xlogx ((L : ℝ) - (k + 1)))
          * Real.exp (Real.log ((L : ℝ) - k) - Real.log k) := by
    rw [← Real.exp_add]
    exact Real.exp_le_exp.2 (by linarith)
  rw [Real.exp_sub, Real.exp_log (by linarith), Real.exp_log hk'] at hexp
  have hC : (0 : ℝ) ≤ L.choose k := Nat.cast_nonneg _
  calc (L.choose k : ℝ) * k * Real.exp (xlogx k + xlogx ((L : ℝ) - k))
      ≤ (L.choose k : ℝ) * k * (Real.exp (xlogx ((k : ℝ) + 1) + xlogx ((L : ℝ) - (k + 1)))
          * (((L : ℝ) - k) / k)) := by gcongr
    _ = (L.choose k : ℝ) * ((L : ℝ) - k)
          * Real.exp (xlogx ((k : ℝ) + 1) + xlogx ((L : ℝ) - (k + 1))) := by
        field_simp

/-- The proxy `binom(L, k) · k · e^{φ(k) + φ(L-k)}` is monotone in `k ≤ L`. -/
theorem ratio_mono (L : ℕ) {k₁ k₂ : ℕ} (h12 : k₁ ≤ k₂) (h2 : k₂ ≤ L) :
    (L.choose k₁ : ℝ) * k₁ * Real.exp (xlogx k₁ + xlogx ((L : ℝ) - k₁))
      ≤ (L.choose k₂ : ℝ) * k₂ * Real.exp (xlogx k₂ + xlogx ((L : ℝ) - k₂)) := by
  induction k₂, h12 using Nat.le_induction with
  | base => exact le_rfl
  | succ n hn ih => exact (ih (by omega)).trans (ratio_step L n (by omega))

end PrunedAux

end ThreeSumApsp
end
end

section
-- Source module: ThreeSumApsp.Pruned.Costs
/-!
# A sharper analysis of Corollary 31: binomial tails and pruned encodings

Two refinements of `Corollary31.costs`, for `L = ⌈cm⌉`, `t = ⌈θm⌉`, `D = 4^m`:

* The number of boxes is bounded by the binomial tail `∑_{d=t}^{m} β_d` (`tailBeta`) itself,
  instead of the geometric bound `M ρ^t/(1-ρ)`. The tail is at most `β_t/(1-ρ)`, and
  `β_t/M = 9^t binom(L, m-t)/binom(L, m) = O(D^{-Γ})` with
  `Γ(c, θ) = (c H(1/c) - c H((1-θ)/c) - θ ln 9)/ln 4` (`GammaOf`).
* The encodings are pruned: their cost is `L N ∑_{d ≤ m} β_d / √M` (`retained`), which is
  `O(L N √M)`, and `√M = O(D^{A_pruned})` with `A_pruned(c) = ((1/2) c H(1/c) + (c-1) ln 3)/ln 4`
  (`Apruned`).

The main result is `CorollaryP.costs`; the numbers for `c = 22`, `θ = 29/250` are
`GammaOf_22`, `Apruned_22`, `qOf_29_250` and `admissibleP_22`.
-/

@[expose] public section

open Finset

namespace ThreeSumApsp

open PrunedAux

/-- The exponent of the binomial tail: `Γ(c, θ) = (c H(1/c) - c H((1-θ)/c) - θ ln 9)/ln 4`. -/
noncomputable def GammaOf (c θ : ℝ) : ℝ :=
  (c * entropy (1 / c) - c * entropy ((1 - θ) / c) - θ * Real.log 9) / Real.log 4

/-- The exponent of `√M`: `A_pruned(c) = ((1/2) c H(1/c) + (c-1) ln 3)/ln 4`. -/
noncomputable def Apruned (c : ℝ) : ℝ :=
  ((1 / 2) * c * entropy (1 / c) + (c - 1) * Real.log 3) / Real.log 4

/-- The number of retained entries of the pruned encodings: `∑_{d=0}^{m} β_d`. -/
def retained (L m : ℕ) : ℕ := ∑ d ∈ Finset.range (m + 1), beta L m d

/-- The binomial tail `∑_{d=t}^{m} β_d`. -/
noncomputable def tailBeta (L m t : ℕ) : ℝ := ∑ d ∈ Finset.Icc t m, (beta L m d : ℝ)

/-- the preprocessing cost of the pruned data structure: boxes + encodings -/
noncomputable def cost8p (L m t N : ℕ) : ℝ :=
  (L : ℝ) * ((m : ℝ) + 1) * (tailBeta L m t / (ThreeSumApsp.M L m : ℝ)) * (N : ℝ) ^ 2
    + (L : ℝ) * (N : ℝ) * (retained L m : ℝ) / Real.sqrt (ThreeSumApsp.M L m : ℝ)

/-- The hypotheses of the sharper corollary on its parameters. -/
structure AdmissibleP (c θ ε : ℝ) : Prop where
  c_gt : 10 < c
  θ_pos : 0 < θ
  θ_lt : θ < 0.9
  thin : ε * (Apruned c + GammaOf c θ) < 1

/-! ### The exponents -/

/-- `Γ ln 4 = (1-θ) ln(1-θ) + (c-1+θ) ln(c-1+θ) - (c-1) ln(c-1) - θ ln 9`. -/
theorem GammaOf_mul_log_four {c θ : ℝ} (hc : 1 < c) (hθ0 : 0 < θ) (hθ1 : θ < 1) :
    GammaOf c θ * Real.log 4
      = (1 - θ) * Real.log (1 - θ) + (c - 1 + θ) * Real.log (c - 1 + θ)
        - (c - 1) * Real.log (c - 1) - θ * Real.log 9 := by
  rw [GammaOf, div_mul_cancel₀ _ log_four_pos.ne', mul_entropy_inv hc,
    mul_entropy_div (a := 1 - θ) (by linarith) (by linarith),
    show c - (1 - θ) = c - 1 + θ by ring]
  ring

/-- `A_pruned ln 4 = (1/2)(c ln c - (c-1) ln(c-1)) + (c-1) ln 3`. -/
theorem Apruned_mul_log_four {c : ℝ} (hc : 1 < c) :
    Apruned c * Real.log 4
      = (1 / 2) * (c * Real.log c - (c - 1) * Real.log (c - 1)) + (c - 1) * Real.log 3 := by
  rw [Apruned, div_mul_cancel₀ _ log_four_pos.ne', mul_assoc, mul_entropy_inv hc]

/-- `F(cx, x, θx) = -Γ x ln 4`. -/
theorem Fexp_scale_eq {c θ x : ℝ} (hc : 1 < c) (hθ0 : 0 < θ) (hθ1 : θ < 1) (hx : 0 < x) :
    Fexp (c * x) x (θ * x) = -(GammaOf c θ * (x * Real.log 4)) := by
  rw [Fexp_scale hc hθ1 hθ0.le hx, ← mul_assoc, mul_comm (GammaOf c θ) x, mul_assoc,
    GammaOf_mul_log_four hc hθ0 hθ1]
  ring

/-- The sharper exponent is at least the exponent `γ` of Corollary 31. -/
theorem gammaOf_le_GammaOf {c θ : ℝ} (hc : 10 < c) (hθ0 : 0 < θ) (hθ1 : θ < 0.9) :
    gammaOf c θ ≤ GammaOf c θ := by
  have h := Fexp_sub_le (u := c) (m := 1) (s₁ := 0) (s₂ := θ) hθ0.le (by linarith)
    (by norm_num) (by linarith)
  rw [Fexp_zero, sub_zero, sub_zero, sub_zero, Real.log_one] at h
  simp only [add_zero] at h
  have h2 := Fexp_scale_eq (x := 1) (by linarith : (1 : ℝ) < c) hθ0 (by linarith) one_pos
  rw [mul_one, mul_one, one_mul] at h2
  rw [h2] at h
  have hγ : gammaOf c θ * Real.log 4 = θ * (Real.log (c - 1) - Real.log 9) := by
    rw [gammaOf, div_mul_cancel₀ _ log_four_pos.ne', one_div_rhoC,
      Real.log_div (by linarith) (by norm_num)]
  have : gammaOf c θ * Real.log 4 ≤ GammaOf c θ * Real.log 4 := by
    rw [hγ]
    linarith
  exact le_of_mul_le_mul_right this log_four_pos

/-- `Γ > 0` for admissible `c` and `θ`. -/
theorem GammaOf_pos {c θ : ℝ} (hc : 10 < c) (hθ0 : 0 < θ) (hθ1 : θ < 0.9) : 0 < GammaOf c θ :=
  (corollary_31_gamma_pos c θ hc hθ0).trans_le (gammaOf_le_GammaOf hc hθ0 hθ1)

/-! ### The binomial tail -/

/-- `β_d ≤ ρ^{d-t} β_t` for `t ≤ d ≤ m`. -/
theorem beta_le_rho_pow {L m t : ℕ} (hL : 10 * m ≤ L) {d : ℕ} (htd : t ≤ d) (hdm : d ≤ m) :
    (beta L m d : ℝ) ≤ ThreeSumApsp.rho L m ^ (d - t) * (beta L m t : ℝ) := by
  induction d, htd using Nat.le_induction with
  | base => simp
  | succ d hd ih =>
    obtain ⟨hratio, hle⟩ := eq_7_ratio_b299791 L m (d + 1) hL (by omega) hdm
    have hpos : (0 : ℝ) < (beta L m d : ℝ) := by
      exact_mod_cast beta_pos (L := L) (m := m) (by omega) d
    rw [← hratio, Nat.add_sub_cancel, div_le_iff₀ hpos] at hle
    calc (beta L m (d + 1) : ℝ) ≤ ThreeSumApsp.rho L m * (beta L m d : ℝ) := hle
      _ ≤ ThreeSumApsp.rho L m * (ThreeSumApsp.rho L m ^ (d - t) * (beta L m t : ℝ)) :=
          mul_le_mul_of_nonneg_left (ih (by omega)) (rho_nonneg hL)
      _ = ThreeSumApsp.rho L m ^ (d + 1 - t) * (beta L m t : ℝ) := by
          rw [show d + 1 - t = (d - t) + 1 by omega, pow_succ]
          ring

/-- The tail is at most `β_t/(1-ρ)`. -/
theorem tailBeta_le {L m t : ℕ} (hL : 10 * m ≤ L) :
    tailBeta L m t ≤ (beta L m t : ℝ) / (1 - ThreeSumApsp.rho L m) := by
  have hρ0 := rho_nonneg hL
  have hρ1 := sec4_rho_lt_one L m hL
  have hβ : (0 : ℝ) ≤ beta L m t := Nat.cast_nonneg _
  calc tailBeta L m t ≤ ∑ d ∈ Icc t m, ThreeSumApsp.rho L m ^ (d - t) * (beta L m t : ℝ) :=
        sum_le_sum fun d hd => beta_le_rho_pow hL (mem_Icc.1 hd).1 (mem_Icc.1 hd).2
    _ = (∑ i ∈ range (m + 1 - t), ThreeSumApsp.rho L m ^ i) * (beta L m t : ℝ) := by
        rw [← Finset.Ico_add_one_right_eq_Icc, Finset.sum_Ico_eq_sum_range, sum_mul]
        refine sum_congr rfl fun i _ => ?_
        rw [Nat.add_sub_cancel_left]
    _ ≤ (1 / (1 - ThreeSumApsp.rho L m)) * (beta L m t : ℝ) := by
        refine mul_le_mul_of_nonneg_right ?_ hβ
        have := geom_sum_Ico_le_of_lt_one (m := 0) (n := m + 1 - t) hρ0 hρ1
        rwa [pow_zero, ← Finset.range_eq_Ico] at this
    _ = (beta L m t : ℝ) / (1 - ThreeSumApsp.rho L m) := by ring

/-- The retained entries number at most `M/(1-ρ)`. -/
theorem retained_le {L m : ℕ} (hL : 10 * m ≤ L) :
    (retained L m : ℝ) ≤ (ThreeSumApsp.M L m : ℝ) / (1 - ThreeSumApsp.rho L m) := by
  have hρ0 := rho_nonneg hL
  have hρ1 := sec4_rho_lt_one L m hL
  rw [retained, Nat.cast_sum]
  calc ∑ d ∈ range (m + 1), (beta L m d : ℝ) ≤ ∑ d ∈ range (m + 1), ThreeSumApsp.rho L m ^ d * (ThreeSumApsp.M L m : ℝ) :=
        sum_le_sum fun d hd => ThreeSumApsp.eq_7 L m d hL (by rw [mem_range] at hd; omega)
    _ = (∑ d ∈ range (m + 1), ThreeSumApsp.rho L m ^ d) * (ThreeSumApsp.M L m : ℝ) := by rw [sum_mul]
    _ ≤ (1 / (1 - ThreeSumApsp.rho L m)) * (ThreeSumApsp.M L m : ℝ) := by
        refine mul_le_mul_of_nonneg_right ?_ (Nat.cast_nonneg _)
        have := geom_sum_Ico_le_of_lt_one (m := 0) (n := m + 1) hρ0 hρ1
        rwa [pow_zero, ← Finset.range_eq_Ico] at this
    _ = (ThreeSumApsp.M L m : ℝ) / (1 - ThreeSumApsp.rho L m) := by ring

/-- `β_t ≤ M · m/(m-t) · e^{F(L, m, t)}` for `t < m ≤ L`. -/
theorem beta_le_exp {L m t : ℕ} (htm : t < m) (hmL : m ≤ L) :
    (beta L m t : ℝ)
      ≤ (ThreeSumApsp.M L m : ℝ) * ((m : ℝ) / ((m : ℝ) - t)) * Real.exp (Fexp L m t) := by
  have hr := ratio_mono L (k₁ := m - t) (k₂ := m) (by omega) hmL
  rw [Nat.cast_sub htm.le] at hr
  have hmt : (0 : ℝ) < (m : ℝ) - t := by
    have : (t : ℝ) < m := by exact_mod_cast htm
    linarith
  have hK : (L.choose (m - t) : ℝ)
      ≤ (L.choose m : ℝ) * ((m : ℝ) / ((m : ℝ) - t))
        * Real.exp (xlogx m + xlogx ((L : ℝ) - m) - xlogx ((m : ℝ) - t)
            - xlogx ((L : ℝ) - m + t)) := by
    rw [show (L : ℝ) - ((m : ℝ) - t) = (L : ℝ) - m + t by ring] at hr
    rw [sub_sub, Real.exp_sub, mul_div_assoc', le_div_iff₀ (Real.exp_pos _),
      show (L.choose m : ℝ) * ((m : ℝ) / ((m : ℝ) - t)) * Real.exp (xlogx m + xlogx ((L : ℝ) - m))
        = (L.choose m : ℝ) * m * Real.exp (xlogx m + xlogx ((L : ℝ) - m)) / ((m : ℝ) - t) by ring,
      le_div_iff₀ hmt]
    linarith
  have hbeta : (beta L m t : ℝ) = (L.choose (m - t) : ℝ) * 9 ^ (L - m) * 9 ^ t := by
    rw [beta]
    push_cast
    ring
  have hM : (ThreeSumApsp.M L m : ℝ) = (L.choose m : ℝ) * 9 ^ (L - m) := by
    rw [ThreeSumApsp.M, ThreeSumApsp.K, ThreeSumApsp.N0]
    push_cast
    rw [← pow_mul, mul_comm (L - m) 2, pow_mul]
    norm_num
  have h9 : (9 : ℝ) ^ t = Real.exp (t * Real.log 9) := by
    rw [Real.exp_nat_mul, Real.exp_log (by norm_num)]
  rw [hbeta, hM, h9, Fexp, add_sub_assoc, add_sub_assoc, add_assoc, Real.exp_add]
  have h9L : (0 : ℝ) ≤ 9 ^ (L - m) := by positivity
  calc (L.choose (m - t) : ℝ) * 9 ^ (L - m) * Real.exp (t * Real.log 9)
      ≤ (L.choose m : ℝ) * ((m : ℝ) / ((m : ℝ) - t))
          * Real.exp (xlogx m + xlogx ((L : ℝ) - m) - xlogx ((m : ℝ) - t)
            - xlogx ((L : ℝ) - m + t)) * 9 ^ (L - m) * Real.exp (t * Real.log 9) := by gcongr
    _ = _ := by
        rw [show xlogx (m : ℝ) + xlogx ((L : ℝ) - m) - xlogx ((m : ℝ) - t)
            - xlogx ((L : ℝ) - m + t) = xlogx (m : ℝ) + (xlogx ((L : ℝ) - m)
              - xlogx ((m : ℝ) - t) - xlogx ((L : ℝ) - m + t)) by ring]
        ring

/-! ### The parameters `L = ⌈cm⌉` and `t = ⌈θm⌉` -/

/-- `L = ⌈cm⌉ ≤ (c + 1) m` for `m ≥ 1`. -/
theorem levelsOf_le_mul {c : ℝ} (hc : 10 < c) {m : ℕ} (hm : 1 ≤ m) :
    (levelsOf c m : ℝ) ≤ (c + 1) * m := by
  have hm' : (1 : ℝ) ≤ m := by exact_mod_cast hm
  have hL : (levelsOf c m : ℝ) < c * m + 1 := Nat.ceil_lt_add_one (by positivity)
  linarith

/-- The rounding of `L` and `t` only helps: `F(L, m, t) ≤ F(cm, m, θm) = -Γ m ln 4`. -/
theorem Fexp_levels_le {c θ : ℝ} (hc : 10 < c) (hθ0 : 0 < θ) (hθ1 : θ < 0.9) {m : ℕ}
    (hm : 1 ≤ m) :
    Fexp (levelsOf c m) m (switchOf θ m) ≤ -(GammaOf c θ * ((m : ℝ) * Real.log 4)) := by
  have hm' : (1 : ℝ) ≤ m := by exact_mod_cast hm
  have hcL : c * m ≤ (levelsOf c m : ℝ) := Nat.le_ceil _
  have hLc : (levelsOf c m : ℝ) < c * m + 1 := Nat.ceil_lt_add_one (by positivity)
  have hθt : θ * m ≤ (switchOf θ m : ℝ) := Nat.le_ceil _
  have ht1 : (1 : ℝ) ≤ (switchOf θ m : ℝ) := by
    have : 0 < switchOf θ m := Nat.ceil_pos.2 (by positivity)
    exact_mod_cast this
  have htm : (switchOf θ m : ℝ) ≤ m := by exact_mod_cast switchOf_le (by linarith) m
  have h9 : 9 * (m : ℝ) ≤ (c - 1) * m := by nlinarith
  calc Fexp (levelsOf c m) m (switchOf θ m)
      ≤ Fexp (c * m) m (switchOf θ m) := Fexp_anti_u hcL (by linarith) (by nlinarith)
    _ ≤ Fexp (c * m) m (θ * m) :=
        Fexp_anti_s hθt htm (by nlinarith) (by nlinarith) (by nlinarith)
    _ = -(GammaOf c θ * ((m : ℝ) * Real.log 4)) :=
        Fexp_scale_eq (by linarith) hθ0 (by linarith) (by linarith)

/-- `M > 0` for `m ≤ L`. -/
theorem cast_M_pos {L m : ℕ} (hmL : m ≤ L) : (0 : ℝ) < (ThreeSumApsp.M L m : ℝ) := by
  rw [← beta_zero_eq_M]
  exact_mod_cast beta_pos hmL 0

/-- The step on the boxes: `tailBeta/M ≤ 1/(1-ρ_c) · 2/(1-θ) · D^{-Γ}` once `(1-θ) m ≥ 2`. -/
theorem tail_div_M_le {c θ : ℝ} (hc : 10 < c) (hθ0 : 0 < θ) (hθ1 : θ < 0.9) {m : ℕ}
    (hm : 1 ≤ m) (hm2 : 2 ≤ (1 - θ) * m) :
    tailBeta (levelsOf c m) m (switchOf θ m) / (ThreeSumApsp.M (levelsOf c m) m : ℝ)
      ≤ 1 / (1 - rhoC c) * (2 / (1 - θ)) * (ThreeSumApsp.D m : ℝ) ^ (-GammaOf c θ) := by
  set L := levelsOf c m
  set t := switchOf θ m
  have hL10 : 10 * m ≤ L := ten_mul_le_levelsOf hc m
  have hmL : m ≤ L := by omega
  have hM := cast_M_pos hmL
  have hgap : 0 < 1 - rhoC c := sub_pos.2 (rhoC_lt_one hc)
  have hgap_le : 1 - rhoC c ≤ 1 - ThreeSumApsp.rho L m := by linarith [Corollary31.rho_lt hc m]
  have htlt : (t : ℝ) < θ * m + 1 := Nat.ceil_lt_add_one (by positivity)
  have hmt : (1 - θ) * m / 2 ≤ (m : ℝ) - t := by linarith
  have htm : t < m := by
    have : (t : ℝ) < m := by linarith
    exact_mod_cast this
  have hmt0 : 0 < (m : ℝ) - t := by linarith
  have hratio : (m : ℝ) / ((m : ℝ) - t) ≤ 2 / (1 - θ) := by
    rw [div_le_div_iff₀ hmt0 (by linarith)]
    nlinarith
  have hexp : Real.exp (Fexp L m t) ≤ (ThreeSumApsp.D m : ℝ) ^ (-GammaOf c θ) := by
    rw [cast_D_rpow, neg_mul]
    exact Real.exp_le_exp.2 (Fexp_levels_le hc hθ0 hθ1 hm)
  have hβ := beta_le_exp htm hmL
  have hβ0 : (0 : ℝ) ≤ beta L m t := Nat.cast_nonneg _
  rw [div_le_iff₀ hM]
  calc tailBeta L m t ≤ (beta L m t : ℝ) / (1 - ThreeSumApsp.rho L m) := tailBeta_le hL10
    _ ≤ (beta L m t : ℝ) / (1 - rhoC c) := div_le_div_of_nonneg_left hβ0 hgap hgap_le
    _ ≤ (ThreeSumApsp.M L m : ℝ) * ((m : ℝ) / ((m : ℝ) - t)) * Real.exp (Fexp L m t) / (1 - rhoC c) :=
        div_le_div_of_nonneg_right hβ hgap.le
    _ ≤ (ThreeSumApsp.M L m : ℝ) * (2 / (1 - θ)) * (ThreeSumApsp.D m : ℝ) ^ (-GammaOf c θ) / (1 - rhoC c) := by
        gcongr
        exact mul_nonneg hM.le (div_nonneg (by norm_num) (by linarith))
    _ = 1 / (1 - rhoC c) * (2 / (1 - θ)) * (ThreeSumApsp.D m : ℝ) ^ (-GammaOf c θ) * (ThreeSumApsp.M L m : ℝ) := by
        field_simp

/-! ### The encodings: `√M = O(D^{A_pruned})` -/

/-- `K = binom(L, m) ≤ 2 e^{m (c ln c - (c-1) ln(c-1))}`. -/
theorem K_le_exp {c : ℝ} (hc : 10 < c) {m : ℕ} (hm : 1 ≤ m) :
    (ThreeSumApsp.K (levelsOf c m) m : ℝ)
      ≤ 2 * Real.exp (m * (c * Real.log c - (c - 1) * Real.log (c - 1))) := by
  set L := levelsOf c m
  have hm' : (1 : ℝ) ≤ m := by exact_mod_cast hm
  have hcL : c * m ≤ (L : ℝ) := Nat.le_ceil _
  have hLc : (L : ℝ) < c * m + 1 := Nat.ceil_lt_add_one (by positivity)
  have hmL : m ≤ L := by have := ten_mul_le_levelsOf hc m; omega
  have hcm : 0 < c * m - m := by nlinarith
  have hA := sub_le_right (a := c * m) (b := (L : ℝ)) (by positivity) (by linarith)
  have hB := le_sub_left (a := c * m - m) (b := (L : ℝ) - m) hcm (by linarith)
  have hlog0 : 0 ≤ Real.log L - Real.log (c * m - m) := by
    rw [sub_nonneg]
    exact Real.log_le_log hcm (by linarith)
  have hlog2 : Real.log L - Real.log (c * m - m) ≤ Real.log 2 := by
    rw [← Real.log_div (by linarith) hcm.ne']
    refine Real.log_le_log (div_pos (by linarith) hcm) ?_
    rw [div_le_iff₀ hcm]
    nlinarith
  have hΔ : (L : ℝ) - c * m ≤ 1 := by linarith
  have hprod : ((L : ℝ) - c * m) * (Real.log L - Real.log (c * m - m)) ≤ Real.log 2 :=
    (mul_le_of_le_one_left hlog0 hΔ).trans hlog2
  have hscale := xlogx_scale (c := c) (x := m) (by linarith) (by linarith)
  have hexp : xlogx L - xlogx m - xlogx ((L : ℝ) - m)
      ≤ Real.log 2 + m * (c * Real.log c - (c - 1) * Real.log (c - 1)) := by
    rw [show (L : ℝ) - m - (c * m - m) = L - c * m by ring] at hB
    nlinarith
  calc (ThreeSumApsp.K L m : ℝ) ≤ Real.exp (xlogx L - xlogx m - xlogx ((L : ℝ) - m)) := choose_le_exp L m hmL
    _ ≤ Real.exp (Real.log 2 + m * (c * Real.log c - (c - 1) * Real.log (c - 1))) :=
        Real.exp_le_exp.2 hexp
    _ = 2 * Real.exp (m * (c * Real.log c - (c - 1) * Real.log (c - 1))) := by
        rw [Real.exp_add, Real.exp_log (by norm_num)]

/-- `√M = √K N₀ ≤ 3 √2 D^{A_pruned}`, with `D^{A_pruned}` written as `e^{A_pruned m ln 4}`. -/
theorem sqrtKN0_le_exp {c : ℝ} (hc : 10 < c) {m : ℕ} (hm : 1 ≤ m) :
    sqrtKN0 (levelsOf c m) m ≤ 3 * Real.sqrt 2 * Real.exp (Apruned c * ((m : ℝ) * Real.log 4)) := by
  set L := levelsOf c m
  set E := c * Real.log c - (c - 1) * Real.log (c - 1)
  have hm' : (1 : ℝ) ≤ m := by exact_mod_cast hm
  have hLc : (L : ℝ) < c * m + 1 := Nat.ceil_lt_add_one (by positivity)
  have hmL : m ≤ L := by have := ten_mul_le_levelsOf hc m; omega
  have hK := K_le_exp hc hm
  have hsqrtK : Real.sqrt (ThreeSumApsp.K L m : ℝ) ≤ Real.sqrt 2 * Real.exp (m * E / 2) := by
    calc Real.sqrt (ThreeSumApsp.K L m : ℝ) ≤ Real.sqrt (2 * Real.exp (m * E)) := Real.sqrt_le_sqrt hK
      _ = Real.sqrt 2 * Real.exp (m * E / 2) := by
          rw [Real.sqrt_mul (by norm_num)]
          congr 1
          rw [show Real.exp (m * E) = Real.exp (m * E / 2) ^ 2 by
            rw [sq, ← Real.exp_add]; ring_nf, Real.sqrt_sq (Real.exp_pos _).le]
  have hN0 : (ThreeSumApsp.N0 L m : ℝ) ≤ 3 * Real.exp ((c - 1) * m * Real.log 3) := by
    rw [ThreeSumApsp.N0, Nat.cast_pow, Nat.cast_ofNat, ← Real.exp_log (by norm_num : (0 : ℝ) < 3),
      ← Real.exp_nat_mul, Real.exp_log (by norm_num : (0 : ℝ) < 3), Nat.cast_sub hmL]
    calc Real.exp (((L : ℝ) - m) * Real.log 3) ≤ Real.exp ((c * m + 1 - m) * Real.log 3) :=
          Real.exp_le_exp.2 (mul_le_mul_of_nonneg_right (by linarith)
            (Real.log_nonneg (by norm_num)))
      _ = 3 * Real.exp ((c - 1) * m * Real.log 3) := by
          rw [show (c * m + 1 - m) * Real.log 3 = Real.log 3 + (c - 1) * m * Real.log 3 by ring,
            Real.exp_add, Real.exp_log (by norm_num)]
  have hA : Apruned c * ((m : ℝ) * Real.log 4) = m * E / 2 + (c - 1) * m * Real.log 3 := by
    rw [← mul_assoc, mul_comm (Apruned c), mul_assoc, Apruned_mul_log_four (by linarith)]
    ring
  rw [sqrtKN0, hA, Real.exp_add]
  calc Real.sqrt (ThreeSumApsp.K L m : ℝ) * (ThreeSumApsp.N0 L m : ℝ)
      ≤ (Real.sqrt 2 * Real.exp (m * E / 2)) * (3 * Real.exp ((c - 1) * m * Real.log 3)) :=
        mul_le_mul hsqrtK hN0 (Nat.cast_nonneg _) (by positivity)
    _ = 3 * Real.sqrt 2 * (Real.exp (m * E / 2) * Real.exp ((c - 1) * m * Real.log 3)) := by ring

/-- The analogue of (10): `√M · D^Γ ≤ N` once `m` exceeds a constant depending on `c`, `θ`, `ε`. -/
theorem eq_10p {c θ ε : ℝ} (h : AdmissibleP c θ ε) (hε : 0 < ε) :
    ∃ m₀ : ℕ, ∀ m : ℕ, m₀ ≤ m → ∀ D₀ N : ℕ, 4 ^ (m - 1) < D₀ → (D₀ : ℝ) ≤ (N : ℝ) ^ ε →
      sqrtKN0 (levelsOf c m) m * (ThreeSumApsp.D m : ℝ) ^ GammaOf c θ ≤ N := by
  obtain ⟨hc, hθ0, hθ1, hthin⟩ := h
  set S := Apruned c + GammaOf c θ
  set g := 1 / ε - S
  have hg : 0 < g := by
    have : ε * S < ε * (1 / ε) := by rw [mul_one_div_cancel hε.ne']; exact hthin
    have := lt_of_mul_lt_mul_left this hε.le
    simp only [g]; linarith
  refine ⟨⌈(2 + 1 / ε) / g⌉₊ + 1, fun m hm D₀ N hgt hthin' => ?_⟩
  have hm1 : 1 ≤ m := by omega
  have hmg : (2 + 1 / ε) / g ≤ m := by
    have := Nat.le_ceil ((2 + 1 / ε) / g)
    have h2 : ((⌈(2 + 1 / ε) / g⌉₊ : ℕ) : ℝ) ≤ m := by exact_mod_cast (by omega : _ ≤ m)
    linarith
  rw [div_le_iff₀ hg] at hmg
  have hX := log_four_pos
  have hsq := sqrtKN0_le_exp hc hm1
  have h32 : 3 * Real.sqrt 2 ≤ Real.exp (2 * Real.log 4) := by
    rw [show 2 * Real.log 4 = Real.log 4 + Real.log 4 by ring, Real.exp_add,
      Real.exp_log (by norm_num)]
    have : Real.sqrt 2 ≤ 2 := by
      rw [Real.sqrt_le_left (by norm_num)]; norm_num
    linarith
  have hN := Corollary31.hypothesis hm1 hε hgt hthin'
  rw [Real.rpow_def_of_pos (by norm_num)] at hN
  rw [cast_D_rpow]
  calc sqrtKN0 (levelsOf c m) m * Real.exp (GammaOf c θ * ((m : ℝ) * Real.log 4))
      ≤ 3 * Real.sqrt 2 * Real.exp (Apruned c * ((m : ℝ) * Real.log 4))
          * Real.exp (GammaOf c θ * ((m : ℝ) * Real.log 4)) :=
        mul_le_mul_of_nonneg_right hsq (Real.exp_pos _).le
    _ ≤ Real.exp (2 * Real.log 4) * Real.exp (Apruned c * ((m : ℝ) * Real.log 4))
          * Real.exp (GammaOf c θ * ((m : ℝ) * Real.log 4)) := by gcongr
    _ = Real.exp ((2 + S * m) * Real.log 4) := by
        rw [← Real.exp_add, ← Real.exp_add]
        congr 1
        ring
    _ ≤ Real.exp (Real.log 4 * (((m : ℝ) - 1) / ε)) := by
        rw [Real.exp_le_exp, mul_comm (Real.log 4)]
        refine mul_le_mul_of_nonneg_right ?_ hX.le
        have : ((m : ℝ) - 1) / ε = m * (1 / ε) - 1 / ε := by ring
        rw [this]
        simp only [g] at hmg
        nlinarith
    _ ≤ (N : ℝ) := hN

/-! ### The corollary -/

/-- The first term of `cost8p`, for `D = 4^m`. -/
theorem first_term_le {c θ : ℝ} (hc : 10 < c) (hθ0 : 0 < θ) (hθ1 : θ < 0.9) {m : ℕ}
    (hm : 1 ≤ m) (hm2 : 2 ≤ (1 - θ) * m) (N : ℕ) :
    (levelsOf c m : ℝ) * ((m : ℝ) + 1)
        * (tailBeta (levelsOf c m) m (switchOf θ m) / (ThreeSumApsp.M (levelsOf c m) m : ℝ)) * (N : ℝ) ^ 2
      ≤ 2 * (c + 1) * (1 / (1 - rhoC c) * (2 / (1 - θ)))
          * ((ThreeSumApsp.D m : ℝ) ^ (-GammaOf c θ) * Real.log (ThreeSumApsp.D m) ^ 2) * (N : ℝ) ^ 2 := by
  have hm' : (1 : ℝ) ≤ m := by exact_mod_cast hm
  have hL := levelsOf_le_mul hc hm
  have htail := tail_div_M_le hc hθ0 hθ1 hm hm2
  have hgap : 0 < 1 - rhoC c := sub_pos.2 (rhoC_lt_one hc)
  have hk : 0 ≤ 1 / (1 - rhoC c) * (2 / (1 - θ)) :=
    mul_nonneg (by positivity) (div_nonneg (by norm_num) (by linarith))
  have hlog : (m : ℝ) ^ 2 ≤ Real.log (ThreeSumApsp.D m) ^ 2 :=
    pow_le_pow_left₀ (Nat.cast_nonneg _) (cast_le_log_cast_D m) 2
  have htail0 : 0 ≤ tailBeta (levelsOf c m) m (switchOf θ m) / (ThreeSumApsp.M (levelsOf c m) m : ℝ) :=
    div_nonneg (sum_nonneg fun _ _ => Nat.cast_nonneg _) (Nat.cast_nonneg _)
  have hDΓ : 0 ≤ (ThreeSumApsp.D m : ℝ) ^ (-GammaOf c θ) := (Real.rpow_pos_of_pos (cast_D_pos m) _).le
  refine mul_le_mul_of_nonneg_right ?_ (sq_nonneg _)
  calc (levelsOf c m : ℝ) * ((m : ℝ) + 1)
        * (tailBeta (levelsOf c m) m (switchOf θ m) / (ThreeSumApsp.M (levelsOf c m) m : ℝ))
      ≤ ((c + 1) * m) * (2 * m)
          * (1 / (1 - rhoC c) * (2 / (1 - θ)) * (ThreeSumApsp.D m : ℝ) ^ (-GammaOf c θ)) := by
        gcongr
        linarith
    _ = 2 * (c + 1) * (1 / (1 - rhoC c) * (2 / (1 - θ)))
          * ((ThreeSumApsp.D m : ℝ) ^ (-GammaOf c θ) * (m : ℝ) ^ 2) := by ring
    _ ≤ 2 * (c + 1) * (1 / (1 - rhoC c) * (2 / (1 - θ)))
          * ((ThreeSumApsp.D m : ℝ) ^ (-GammaOf c θ) * Real.log (ThreeSumApsp.D m) ^ 2) := by
        gcongr

/-- The second term of `cost8p` (the pruned encodings), for `D = 4^m`, where `√M · D^Γ ≤ N`. -/
theorem second_term_le {c : ℝ} (hc : 10 < c) {Γ : ℝ} {m N : ℕ} (hm : 1 ≤ m)
    (hkey : sqrtKN0 (levelsOf c m) m * (ThreeSumApsp.D m : ℝ) ^ Γ ≤ N) :
    (levelsOf c m : ℝ) * (N : ℝ) * (retained (levelsOf c m) m : ℝ)
        / Real.sqrt (ThreeSumApsp.M (levelsOf c m) m : ℝ)
      ≤ (c + 1) / (1 - rhoC c) * ((ThreeSumApsp.D m : ℝ) ^ (-Γ) * Real.log (ThreeSumApsp.D m) ^ 2) * (N : ℝ) ^ 2 := by
  set L := levelsOf c m
  have hm' : (1 : ℝ) ≤ m := by exact_mod_cast hm
  have hL10 : 10 * m ≤ L := ten_mul_le_levelsOf hc m
  have hmL : m ≤ L := by omega
  have hLm := levelsOf_le_mul hc hm
  have hgap : 0 < 1 - rhoC c := sub_pos.2 (rhoC_lt_one hc)
  have hgap_le : 1 - rhoC c ≤ 1 - ThreeSumApsp.rho L m := by linarith [Corollary31.rho_lt hc m]
  have hpos := ThreeSumApsp.sqrtKN0_pos hmL
  have hsqrtM : Real.sqrt (ThreeSumApsp.M L m : ℝ) = sqrtKN0 L m := by
    rw [← sqrtKN0_sq, Real.sqrt_sq hpos.le]
  have hret : (retained L m : ℝ) ≤ (ThreeSumApsp.M L m : ℝ) / (1 - rhoC c) :=
    (retained_le hL10).trans (div_le_div_of_nonneg_left (Nat.cast_nonneg _) hgap hgap_le)
  have hDpos : 0 < (ThreeSumApsp.D m : ℝ) ^ Γ := Real.rpow_pos_of_pos (cast_D_pos m) Γ
  have hs : sqrtKN0 L m ≤ (N : ℝ) * (ThreeSumApsp.D m : ℝ) ^ (-Γ) := by
    rw [Real.rpow_neg (cast_D_pos m).le, ← div_eq_mul_inv, le_div_iff₀ hDpos]
    exact hkey
  have hlog : (m : ℝ) ≤ Real.log (ThreeSumApsp.D m) ^ 2 :=
    (cast_le_log_cast_D m).trans (by nlinarith [cast_le_log_cast_D m])
  have hDΓ : 0 ≤ (ThreeSumApsp.D m : ℝ) ^ (-Γ) := (Real.rpow_pos_of_pos (cast_D_pos m) _).le
  rw [hsqrtM]
  calc (L : ℝ) * (N : ℝ) * (retained L m : ℝ) / sqrtKN0 L m
      ≤ (L : ℝ) * (N : ℝ) * ((ThreeSumApsp.M L m : ℝ) / (1 - rhoC c)) / sqrtKN0 L m := by gcongr
    _ = (L : ℝ) * (N : ℝ) * sqrtKN0 L m / (1 - rhoC c) := by
        rw [← sqrtKN0_sq]
        field_simp
    _ ≤ ((c + 1) * Real.log (ThreeSumApsp.D m) ^ 2) * (N : ℝ) * ((N : ℝ) * (ThreeSumApsp.D m : ℝ) ^ (-Γ))
          / (1 - rhoC c) := by
        gcongr
        exact hLm.trans (mul_le_mul_of_nonneg_left hlog (by linarith))
    _ = (c + 1) / (1 - rhoC c) * ((ThreeSumApsp.D m : ℝ) ^ (-Γ) * Real.log (ThreeSumApsp.D m) ^ 2) * (N : ℝ) ^ 2 := by
        field_simp

/-- `4^{m-1} < D₀ ≤ N^ε` is possible only for `ε > 0`, because `D₀ ≥ 2`. -/
theorem pos_of_le_rpow' {m D₀ N : ℕ} {ε : ℝ} (hgt : 4 ^ (m - 1) < D₀)
    (hthin : (D₀ : ℝ) ≤ (N : ℝ) ^ ε) : 0 < ε := by
  have hD : (2 : ℝ) ≤ D₀ := by
    have : 1 ≤ 4 ^ (m - 1) := Nat.one_le_pow _ _ (by norm_num)
    exact_mod_cast (by omega : 2 ≤ D₀)
  have hN : 0 < N := by
    by_contra h0
    obtain rfl : N = 0 := by omega
    rw [Nat.cast_zero] at hthin
    linarith [Real.zero_rpow_le_one ε]
  refine lt_of_not_ge fun hε => ?_
  linarith [Real.rpow_le_one_of_one_le_of_nonpos (Nat.one_le_cast.2 hN) hε]

/-- The cost of a query is `O(D^q log D)`, in the given `D` (as in Corollary 31). -/
theorem CorollaryP.dominated_costQuery {c θ : ℝ} (hc : 10 < c) (hθ0 : 0 < θ) (hθ1 : θ < 0.9) :
    Dominated Sizes.SetUp (fun p => costQuery (levelsOf c p.m) p.m (switchOf θ p.m))
      fun p => (p.D₀ : ℝ) ^ qOf θ * Real.log p.D₀ :=
  ((Corollary31.query_cost hc hθ0 hθ1).comp Sizes.m fun _ hp => hp.m_pos).trans
    (by simpa only [pow_one] using padded_le (qOf θ) 1)

/-- The sharper Corollary 31, with the binomial tail and the pruned encodings. For `c > 10`,
`0 < θ < 0.9` and `ε (A_pruned(c) + Γ(c, θ)) < 1` there are `C` and `m₀` such that for all
`2 ≤ D ≤ N^ε` with `m = ⌈log_4 D⌉ ≥ m₀`, `L = ⌈cm⌉`, `t = ⌈θm⌉`: `N ≥ √K N₀`, the pruned
preprocessing cost is at most `C N² log² D / D^Γ`, and the query cost is at most `C D^q log D`. -/
theorem CorollaryP.costs {c θ ε : ℝ} (h : AdmissibleP c θ ε) :
    ∃ (C : ℝ) (m₀ : ℕ), 0 ≤ C ∧ ∀ D₀ N m : ℕ, 2 ≤ D₀ → (D₀ : ℝ) ≤ (N : ℝ) ^ ε →
      m = ⌈Real.logb 4 (D₀ : ℝ)⌉₊ → m₀ ≤ m →
      sqrtKN0 (levelsOf c m) m ≤ N ∧
      cost8p (levelsOf c m) m (switchOf θ m) N
        ≤ C * ((N : ℝ) ^ 2 * Real.log (D₀ : ℝ) ^ 2 / (D₀ : ℝ) ^ GammaOf c θ) ∧
      costQuery (levelsOf c m) m (switchOf θ m) ≤ C * ((D₀ : ℝ) ^ qOf θ * Real.log (D₀ : ℝ)) := by
  have hc := h.c_gt
  have hθ0 := h.θ_pos
  have hθ1 := h.θ_lt
  rcases le_or_gt ε 0 with hε0 | hε0
  · refine ⟨0, 0, le_rfl, fun D₀ N m hD hDN hm _ => ?_⟩
    exact absurd (pos_of_le_rpow' (Corollary26.setting_up D₀ m hD hm).2.2 hDN) hε0.not_gt
  obtain ⟨m₁, hkey⟩ := eq_10p h hε0
  obtain ⟨Cq, hCq, hq⟩ := CorollaryP.dominated_costQuery hc hθ0 hθ1
  obtain ⟨Cp, hCp, hp⟩ := padded_le (-GammaOf c θ) 2
  have hgap : 0 < 1 - rhoC c := sub_pos.2 (rhoC_lt_one hc)
  have h1θ : 0 < 1 - θ := by linarith
  set k₁ := 2 * (c + 1) * (1 / (1 - rhoC c) * (2 / (1 - θ)))
  set k₂ := (c + 1) / (1 - rhoC c)
  have hk₁ : 0 ≤ k₁ := by positivity
  have hk₂ : 0 ≤ k₂ := div_nonneg (by linarith) hgap.le
  have hΓ := GammaOf_pos hc hθ0 hθ1
  refine ⟨max (Cp * (k₁ + k₂)) Cq, max m₁ ⌈2 / (1 - θ)⌉₊, le_max_of_le_right hCq,
    fun D₀ N m hD hDN hm hm₀ => ?_⟩
  have hsetup : Sizes.SetUp ⟨D₀, N, m⟩ := ⟨hD, hm⟩
  have hm1 : 1 ≤ m := hsetup.m_pos
  have hkeym := hkey m (le_of_max_le_left hm₀) D₀ N hsetup.gt hDN
  have hm2 : 2 ≤ (1 - θ) * m := by
    have := Nat.ceil_le.1 (le_of_max_le_right hm₀)
    rwa [div_le_iff₀ h1θ, mul_comm] at this
  have hD1 : 1 ≤ (ThreeSumApsp.D m : ℝ) ^ GammaOf c θ := Real.one_le_rpow (one_le_cast_D m) hΓ.le
  have hD₀ : (2 : ℝ) ≤ D₀ := by exact_mod_cast hD
  have hlogD₀ : 0 ≤ Real.log (D₀ : ℝ) := Real.log_nonneg (by linarith)
  refine ⟨?_, ?_, ?_⟩
  · calc sqrtKN0 (levelsOf c m) m ≤ sqrtKN0 (levelsOf c m) m * (ThreeSumApsp.D m : ℝ) ^ GammaOf c θ :=
          le_mul_of_one_le_right (ThreeSumApsp.sqrtKN0_pos (by have := ten_mul_le_levelsOf hc m; omega)).le
            hD1
      _ ≤ N := hkeym
  · have hpad : (ThreeSumApsp.D m : ℝ) ^ (-GammaOf c θ) * Real.log (ThreeSumApsp.D m) ^ 2
        ≤ Cp * ((D₀ : ℝ) ^ (-GammaOf c θ) * Real.log D₀ ^ 2) := hp ⟨D₀, N, m⟩ hsetup
    have h1 := first_term_le hc hθ0 hθ1 hm1 hm2 N
    have h2 := second_term_le hc hm1 hkeym
    have hR : 0 ≤ (D₀ : ℝ) ^ (-GammaOf c θ) * Real.log D₀ ^ 2 := by positivity
    have heq : (N : ℝ) ^ 2 * Real.log (D₀ : ℝ) ^ 2 / (D₀ : ℝ) ^ GammaOf c θ
        = (D₀ : ℝ) ^ (-GammaOf c θ) * Real.log D₀ ^ 2 * (N : ℝ) ^ 2 := by
      rw [Real.rpow_neg (by linarith)]
      field_simp
    rw [heq]
    calc cost8p (levelsOf c m) m (switchOf θ m) N
        ≤ k₁ * ((ThreeSumApsp.D m : ℝ) ^ (-GammaOf c θ) * Real.log (ThreeSumApsp.D m) ^ 2) * (N : ℝ) ^ 2
          + k₂ * ((ThreeSumApsp.D m : ℝ) ^ (-GammaOf c θ) * Real.log (ThreeSumApsp.D m) ^ 2) * (N : ℝ) ^ 2 :=
          add_le_add h1 h2
      _ = (k₁ + k₂) * ((ThreeSumApsp.D m : ℝ) ^ (-GammaOf c θ) * Real.log (ThreeSumApsp.D m) ^ 2) * (N : ℝ) ^ 2 := by ring
      _ ≤ (k₁ + k₂) * (Cp * ((D₀ : ℝ) ^ (-GammaOf c θ) * Real.log D₀ ^ 2)) * (N : ℝ) ^ 2 := by
          gcongr
      _ = Cp * (k₁ + k₂) * ((D₀ : ℝ) ^ (-GammaOf c θ) * Real.log D₀ ^ 2 * (N : ℝ) ^ 2) := by
          ring
      _ ≤ max (Cp * (k₁ + k₂)) Cq
            * ((D₀ : ℝ) ^ (-GammaOf c θ) * Real.log D₀ ^ 2 * (N : ℝ) ^ 2) :=
          mul_le_mul_of_nonneg_right (le_max_left _ _) (by positivity)
  · calc costQuery (levelsOf c m) m (switchOf θ m)
        ≤ Cq * ((D₀ : ℝ) ^ qOf θ * Real.log (D₀ : ℝ)) := hq ⟨D₀, N, m⟩ hsetup
      _ ≤ max (Cp * (k₁ + k₂)) Cq * ((D₀ : ℝ) ^ qOf θ * Real.log (D₀ : ℝ)) :=
          mul_le_mul_of_nonneg_right (le_max_right _ _) (by positivity)

/-! ### The numbers for `c = 22`, `θ = 29/250` -/

lemma log_221_250 : Real.log (221 / 250) ∈ Set.Icc (-0.1232982164) (-0.1232982163) :=
  ⟨le_trans (by (norm_num [ThreeSumApsp.logApprox, ThreeSumApsp.logErr, ThreeSumApsp.seriesArg,
                   ThreeSumApsp.logTwoLo, ThreeSumApsp.logTwoHi, ThreeSumApsp.logThreeLo, ThreeSumApsp.logThreeHi,
                   ThreeSumApsp.logTenLo, ThreeSumApsp.logTenHi, Finset.sum_range_succ, ThreeSumApsp.rhoC])) (log_mem_b299791 0 6).1, (log_mem_b299791 0 6).2.trans (by (norm_num [ThreeSumApsp.logApprox, ThreeSumApsp.logErr, ThreeSumApsp.seriesArg,
                                                                                                                                                                           ThreeSumApsp.logTwoLo, ThreeSumApsp.logTwoHi, ThreeSumApsp.logThreeLo, ThreeSumApsp.logThreeHi,
                                                                                                                                                                           ThreeSumApsp.logTenLo, ThreeSumApsp.logTenHi, Finset.sum_range_succ, ThreeSumApsp.rhoC]))⟩

lemma log_5279_250 : Real.log (5279 / 250) ∈ Set.Icc 3.050031045 3.050031049 :=
  ⟨le_trans (by (norm_num [ThreeSumApsp.logApprox, ThreeSumApsp.logErr, ThreeSumApsp.seriesArg,
                   ThreeSumApsp.logTwoLo, ThreeSumApsp.logTwoHi, ThreeSumApsp.logThreeLo, ThreeSumApsp.logThreeHi,
                   ThreeSumApsp.logTenLo, ThreeSumApsp.logTenHi, Finset.sum_range_succ, ThreeSumApsp.rhoC])) (log_mem_b299791 4 8).1, (log_mem_b299791 4 8).2.trans (by (norm_num [ThreeSumApsp.logApprox, ThreeSumApsp.logErr, ThreeSumApsp.seriesArg,
                                                                                                                                                                           ThreeSumApsp.logTwoLo, ThreeSumApsp.logTwoHi, ThreeSumApsp.logThreeLo, ThreeSumApsp.logThreeHi,
                                                                                                                                                                           ThreeSumApsp.logTenLo, ThreeSumApsp.logTenHi, Finset.sum_range_succ, ThreeSumApsp.rhoC]))⟩

lemma log_21 : Real.log 21 ∈ Set.Icc 3.044522436 3.044522440 :=
  ⟨le_trans (by (norm_num [ThreeSumApsp.logApprox, ThreeSumApsp.logErr, ThreeSumApsp.seriesArg,
                   ThreeSumApsp.logTwoLo, ThreeSumApsp.logTwoHi, ThreeSumApsp.logThreeLo, ThreeSumApsp.logThreeHi,
                   ThreeSumApsp.logTenLo, ThreeSumApsp.logTenHi, Finset.sum_range_succ, ThreeSumApsp.rhoC])) (log_mem_b299791 4 8).1, (log_mem_b299791 4 8).2.trans (by (norm_num [ThreeSumApsp.logApprox, ThreeSumApsp.logErr, ThreeSumApsp.seriesArg,
                                                                                                                                                                           ThreeSumApsp.logTwoLo, ThreeSumApsp.logTwoHi, ThreeSumApsp.logThreeLo, ThreeSumApsp.logThreeHi,
                                                                                                                                                                           ThreeSumApsp.logTenLo, ThreeSumApsp.logTenHi, Finset.sum_range_succ, ThreeSumApsp.rhoC]))⟩

lemma log_9 : Real.log 9 ∈ Set.Icc 2.197224576 2.197224579 :=
  ⟨le_trans (by (norm_num [ThreeSumApsp.logApprox, ThreeSumApsp.logErr, ThreeSumApsp.seriesArg,
                   ThreeSumApsp.logTwoLo, ThreeSumApsp.logTwoHi, ThreeSumApsp.logThreeLo, ThreeSumApsp.logThreeHi,
                   ThreeSumApsp.logTenLo, ThreeSumApsp.logTenHi, Finset.sum_range_succ, ThreeSumApsp.rhoC])) (log_mem_b299791 3 6).1, (log_mem_b299791 3 6).2.trans (by (norm_num [ThreeSumApsp.logApprox, ThreeSumApsp.logErr, ThreeSumApsp.seriesArg,
                                                                                                                                                                           ThreeSumApsp.logTwoLo, ThreeSumApsp.logTwoHi, ThreeSumApsp.logThreeLo, ThreeSumApsp.logThreeHi,
                                                                                                                                                                           ThreeSumApsp.logTenLo, ThreeSumApsp.logTenHi, Finset.sum_range_succ, ThreeSumApsp.rhoC]))⟩

lemma log_22 : Real.log 22 ∈ Set.Icc 3.091042452 3.091042455 :=
  ⟨le_trans (by (norm_num [ThreeSumApsp.logApprox, ThreeSumApsp.logErr, ThreeSumApsp.seriesArg,
                   ThreeSumApsp.logTwoLo, ThreeSumApsp.logTwoHi, ThreeSumApsp.logThreeLo, ThreeSumApsp.logThreeHi,
                   ThreeSumApsp.logTenLo, ThreeSumApsp.logTenHi, Finset.sum_range_succ, ThreeSumApsp.rhoC])) (log_mem_b299791 4 8).1, (log_mem_b299791 4 8).2.trans (by (norm_num [ThreeSumApsp.logApprox, ThreeSumApsp.logErr, ThreeSumApsp.seriesArg,
                                                                                                                                                                           ThreeSumApsp.logTwoLo, ThreeSumApsp.logTwoHi, ThreeSumApsp.logThreeLo, ThreeSumApsp.logThreeHi,
                                                                                                                                                                           ThreeSumApsp.logTenLo, ThreeSumApsp.logTenHi, Finset.sum_range_succ, ThreeSumApsp.rhoC]))⟩

lemma log_3 : Real.log 3 ∈ Set.Icc 1.098612288 1.098612290 :=
  ⟨le_trans (by (norm_num [ThreeSumApsp.logApprox, ThreeSumApsp.logErr, ThreeSumApsp.seriesArg,
                   ThreeSumApsp.logTwoLo, ThreeSumApsp.logTwoHi, ThreeSumApsp.logThreeLo, ThreeSumApsp.logThreeHi,
                   ThreeSumApsp.logTenLo, ThreeSumApsp.logTenHi, Finset.sum_range_succ, ThreeSumApsp.rhoC])) (log_mem_b299791 2 8).1, (log_mem_b299791 2 8).2.trans (by (norm_num [ThreeSumApsp.logApprox, ThreeSumApsp.logErr, ThreeSumApsp.seriesArg,
                                                                                                                                                                           ThreeSumApsp.logTwoLo, ThreeSumApsp.logTwoHi, ThreeSumApsp.logThreeLo, ThreeSumApsp.logThreeHi,
                                                                                                                                                                           ThreeSumApsp.logTenLo, ThreeSumApsp.logTenHi, Finset.sum_range_succ, ThreeSumApsp.rhoC]))⟩

lemma log_4 : Real.log 4 ∈ Set.Icc 1.3862943606 1.3862943616 := by
  rw [Real.log_four]
  exact ⟨by linarith [Real.log_two_gt_d9], by linarith [Real.log_two_lt_d9]⟩

/-- `Γ ln 4` at `c = 22`, `θ = 29/250`. -/
lemma GammaOf_22_eq :
    GammaOf 22 (29 / 250) * Real.log 4
      = 221 / 250 * Real.log (221 / 250) + 5279 / 250 * Real.log (5279 / 250)
        - 21 * Real.log 21 - 29 / 250 * Real.log 9 := by
  rw [GammaOf_mul_log_four (by norm_num) (by norm_num) (by norm_num)]
  norm_num

/-- `Γ(22, 29/250) < 0.0762`. -/
theorem GammaOf_22_lt : GammaOf 22 (29 / 250) < 0.0762 := by
  refine lt_of_mul_lt_mul_right ?_ log_four_pos.le
  rw [GammaOf_22_eq]
  have h1 := log_221_250; have h2 := log_5279_250; have h3 := log_21; have h4 := log_9
  have h5 := log_4
  simp only [Set.mem_Icc] at *
  nlinarith

/-- `A_pruned(22) < 18.10932` (the value is `18.1093137…`). -/
theorem Apruned_22 : Apruned 22 < 18.10932 := by
  refine lt_of_mul_lt_mul_right ?_ log_four_pos.le
  rw [Apruned_mul_log_four (by norm_num)]
  have h1 := log_22; have h2 := log_21; have h3 := log_3; have h5 := log_4
  simp only [Set.mem_Icc] at *
  norm_num
  nlinarith

/-- The parameters `c = 22`, `θ = 29/250`, `ε = 5/91` are admissible. -/
theorem admissibleP_5_91 : AdmissibleP 22 (29 / 250) (5 / 91) where
  c_gt := by norm_num
  θ_pos := by norm_num
  θ_lt := by norm_num
  thin := by
    have h1 := Apruned_22
    have h2 := GammaOf_22_lt
    nlinarith

end ThreeSumApsp
end
end

section
-- Source module: ThreeSumApsp.Pruned.Within8p
/-!
# The preprocessing of Theorem 30 with pruned encodings, against the sharper cost `cost8p`

The shared stage of Section 4 writes the encodings only at the leaves with at most `m` nines.  Its
time is a constant times `retW L m`, `N (L + 1)` and the work for the bands
(`sharedShapeP_le_ret`); with the tiles this makes the preprocessing `O(cost8p)`, where
`cost8p L m t N = L (m+1) (∑_{d ≥ t} β_d / M) N² + L N ∑_{d ≤ m} β_d / √M`
(`exists_tPreCore_le_p`).

* `retW L m` is the number of strings of `L` digits with at most `m` nines, which is
  `∑_{d ≤ m} β_d = retained L m` (`retW_eq_retained`).
* `Within8p f`: `f` is at most a constant times `cost8p`, under the hypotheses of Theorem 30.
  Everything is compared with the second term `L N R/√M`, `R = retained L m`, via
  `√M = √K N₀ ≤ 7^L ≤ 9^L ≤ R` and `√M ≤ N`; the boxes are compared with the first term by
  Lemma 29 and the count of the tiles.
-/

@[expose] public section

namespace Light.Sec4

open ThreeSumApsp ThreeSumApsp.Spec Finset

/-! ## The retained leaves -/

/-! ## The facts about the sizes -/

section facts

variable {p : Sec2.Par} {t : ℕ}

end facts

/-! ## Within `cost8p` -/

/-- `f = O(cost8p)` under the hypotheses of Theorem 30. -/
def Within8p (f : Sec2.Par → ℕ → ℕ) : Prop :=
  ∃ C : ℝ, 0 ≤ C ∧ ∀ p t, Hyp30 p t → (f p t : ℝ) ≤ C * cost8p p.L p.m t p.N

namespace Within8p

variable {f g : Sec2.Par → ℕ → ℕ}

end Within8p

/-! ## The shared stage and the tiles -/

end Light.Sec4
end
end

section
-- Source module: ThreeSumApsp.Pruned.CostsP
/-!
# The costs of the programs with rational parameters, against the pruned cost `cost8p`

The analogue of `ChoosingParameters/Costs.lean` with `cost8p` in place of `cost8`.  The program is
the same; only the accounting is sharper, because the shared stage of Section 4 writes the pruned
encodings (`exists_tPreCore_le_p`).  `CostsWithinP` is `CostsWithin` with `cost8p` in its `above`
clause.  The query part is unchanged.  The results: `exists_tPre31_le_p`, `exists_tQuery31_le_p`,
`exists_tOffline32_le_p` and `programSolves_of_costsWithinP`.
-/

@[expose] public section

namespace Light.Sec4

open ThreeSumApsp ThreeSumApsp.Spec ThreeSumApsp.WordRam

section
variable (G : RatParams)

/-- The two bounds dominate the pruned cost of the preprocessing and the cost of a query. -/
structure CostsWithinP (C : ℝ) (N D₀ : ℕ) (tp tq : ℝ) : Prop where
  one_le_N : 1 ≤ N
  one_le_D : 1 ≤ D₀
  D_le_N : D₀ ≤ N
  one_le_pre : 1 ≤ tp
  one_le_query : 1 ≤ tq
  above : G.m₀ ≤ logFour D₀ → Hyp30 (parOf G N D₀) (switchOf31 G D₀) ∧
    cost8p (G.L (logFour D₀)) (logFour D₀) (switchOf31 G D₀) N ≤ C * tp ∧
    costQuery (G.L (logFour D₀)) (logFour D₀) (switchOf31 G D₀) ≤ C * tq

/-- The pruned cost of the preprocessing at the parameters G. -/
noncomputable abbrev RatParams.preCostP (N D₀ : ℕ) : ℝ :=
  cost8p (G.L (logFour D₀)) (logFour D₀) (switchOf31 G D₀) N

/-! ### The preprocessing -/

/-! ### A query -/

end

end Light.Sec4
end
end

section
-- Source module: ThreeSumApsp.Pruned.RegimeP
/-!
# The parameters 22 and 29/250, and the regime D^91 ≤ N^5

The program with rational parameters at `c = 22`, `θ = 29/250` and a threshold `m₀` from
`CorollaryP.costs admissibleP_5_91` (`ratParamsP`).  On the inputs with `D^91 ≤ N^5`, i.e.
`D ≤ N^{5/91}`, the bounds

    Tp = N² (log D + 1)²/D^{0.07618}     and     Tq = D^{0.44274} (log D + 1)

dominate the pruned cost of the preprocessing and the cost of a query of Theorem 30 at these
parameters (`regimeP`).
-/

@[expose] public section

open ThreeSumApsp

namespace Light.Sec4

open ThreeSumApsp.Spec

/-! ## The parameters -/

/-- The constant of the sharper corollary at `c = 22`, `θ = 29/250`, `ε = 5/91`. -/
noncomputable def costsPC : ℝ := Classical.choose (CorollaryP.costs admissibleP_5_91)

/-- The threshold of the sharper corollary at `c = 22`, `θ = 29/250`, `ε = 5/91`. -/
noncomputable def costsPm : ℕ :=
  Classical.choose (Classical.choose_spec (CorollaryP.costs admissibleP_5_91))

/-- The parameters in the program text: `L = 22 m`, `t = ⌈29 m/250⌉`, and the threshold. -/
noncomputable def ratParamsP : RatParams where
  a := 22
  b := 1
  p := 29
  q := 250
  m₀ := max costsPm 1
  hb := le_rfl
  hq := by norm_num
  hc := by norm_num
  hp := by norm_num
  hθ := by norm_num
  hm₀ := le_max_right _ _

/-! ## The bounds -/

/-- The bound on the preprocessing, `N² (log D + 1)²/D^{0.07618}`. -/
noncomputable def preBoundP (N D₀ : ℕ) : ℝ :=
  (N : ℝ) ^ 2 * (Real.log D₀ + 1) ^ 2 / (D₀ : ℝ) ^ (0.07618 : ℝ)

/-- The bound on a query, `D^{0.44274} (log D + 1)`. -/
noncomputable def queryBoundP (D₀ : ℕ) : ℝ := (D₀ : ℝ) ^ (0.44274 : ℝ) * (Real.log D₀ + 1)

section bounds

variable {N D₀ : ℕ}

end bounds

/-! ## The regime -/

end Light.Sec4
end
end

section
-- Source module: ThreeSumApsp.Pruned.RegimeTestP
/-!
# The test D^91 ≤ N^5

regimeTestP(N, D) returns 1 if `D^91 ≤ N^5` and 0 if not, and changes no cell.  It computes
`X = N^5` by three multiplications and then compares `D^91` with `X` as `regimePow` of Section 2
compares `D^18` with `N`: by at most 91 multiplications, none of which exceeds `X D` (but for the
first product, which is `D`), stopping as soon as a power of `D` exceeds `X`.
-/

@[expose] public section

namespace Light.Sec4

open ThreeSumApsp

variable {lim : Limits} {P : Program} {d : ℕ}

/-! ## The text -/

/-- One round of the comparison of `D^91` with `X` (local 0; `D` is local 1, the power local 7,
its exponent local 8, the flag local 9). -/
def regimePow91Round : Stmt :=
  .ite (Light.v 0 <' Light.v 7 *' Light.v 1)
    (.set 9 (k 0) ;; .set 8 (k 91))
    (.set 7 (Light.v 7 *' Light.v 1) ;; .set 8 (Light.v 8 +' k 1))

/-- The test `D^91 ≤ X`: the flag (local 9) ends as 1 if it holds and as 0 if not. -/
def regimePow91 : Stmt :=
  .set 7 (k 1) ;;
  .set 8 (k 0) ;;
  .set 9 (k 1) ;;
  .while (Light.v 8 <' k 91) regimePow91Round

/-- regimeTestP(N, D): `X := N^5`, then the test `D^91 ≤ X`. -/
def regimeTestPBody : Stmt :=
  .set 2 (Light.v 0 *' Light.v 0) ;;
  .set 2 (Light.v 2 *' Light.v 2) ;;
  .set 0 (Light.v 2 *' Light.v 0) ;;
  regimePow91 ;;
  .set 0 (Light.v 9)

/-! ## The comparison -/

/-- The states of the loop: as `Sec2.PowInv`, with 91 in place of 18. -/
def PowInv91 (X D : ℕ) (loc μ : ℕ → ℤ) (σ : State) : Prop :=
  σ.mem = μ ∧ (∀ x < 7, σ.loc x = loc x) ∧
    ((∃ j : ℕ, j ≤ 91 ∧ σ.loc 8 = j ∧ σ.loc 9 = 1 ∧ σ.loc 7 = ((D ^ j : ℕ) : ℤ) ∧
        (j = 0 ∨ D ^ j ≤ X)) ∨
      (σ.loc 8 = 91 ∧ σ.loc 9 = 0 ∧ X < D ^ 91))

/-! ## The test -/

end Light.Sec4
end
end

section
-- Source module: ThreeSumApsp.Pruned.AllInstancesP
/-!
# The pruned thin product on all instances

allInstancesP(N, D, w, U, x, y, wi, wj, out, fr) tests whether `D^91 ≤ N^5`, calls the offline
routine offline32 of the programs with rational parameters at `ratParamsP` (`c = 22`,
`θ = 29/250`) if so, and the brute force if not.  The program is `programP`: `program31P ratParamsP`
followed by allInstancesP (number 74) and regimeTestP (number 75).

* It solves the task `thinTask` on all instances (`allInstancesP_solves`), with a polynomial need
  (`allInstancesNeedP_poly`).  In the regime the hypotheses of Theorem 30 hold from the threshold
  on (`regimeP`), so that `below` bounds `10^L` by `(N + 1)^5` and the need covers what offline32
  asks of the limits (`lim31_of_needP`).
* In the regime its time is `O(w D^{0.44274} (log D + 1) + N² (log D + 1)²/D^{0.07618})`
  (`allInstancesTimeP_le`), by the pruned accounting (`exists_tOffline32_le_p`).
* `claim_thinProductP`: the thin product in this time for programs of the light language.
-/

@[expose] public section

namespace Light.Sec4

open ThreeSumApsp ThreeSumApsp.Spec

/-! ## The program -/

/-- The numbers of the two new procedures. -/
abbrev Proc.allInstancesP : ℕ := 74
@[inherit_doc Proc.allInstancesP] abbrev Proc.regimeTestP : ℕ := 75

/-- allInstancesP(N, D, w, U, x, y, wi, wj, out, fr). Local 10 is the result of the test. -/
def allInstancesPBody : Stmt :=
  .call Proc.regimeTestP [Light.v 0, Light.v 1] 10 ;;
  .ite (k 0 <' Light.v 10)
    (.call Proc.offline32 [Light.v 0, Light.v 1, Light.v 2, Light.v 3, Light.v 4, Light.v 5, Light.v 6, Light.v 7, Light.v 8, Light.v 9] 0)
    (.call Sec2.pThinBrute [Light.v 0, Light.v 1, Light.v 2, Light.v 3, Light.v 4, Light.v 5, Light.v 6, Light.v 7, Light.v 8, Light.v 9] 0)

/-- The program: the programs with rational parameters at `ratParamsP`, then allInstancesP and
regimeTestP. -/
noncomputable def programP : Program := program31P ratParamsP ++ [allInstancesPBody, regimeTestPBody]

/-! ## Time and need -/

/-- The time of allInstancesP, for the parameters N, D, w, U. -/
noncomputable def allInstancesTimeP (c : ℕ) : List ℕ → ℕ
  | [N, D, w, _] =>
    2000 + (if D ^ 91 ≤ N ^ 5 then tOffline32P c ratParamsP N D w else 40 * ((w + 1) * (D + 1)))
  | _ => 0

/-- The word part of the need. -/
noncomputable def wordNeedP (N D U : ℕ) : ℕ :=
  1000 + 400 * D + N * D + D * (U * U) + ((N + 1) ^ 5) ^ 3 * (U * U) + 7 * ((N + 1) ^ 5 * U)
    + 10 * (N + 1) ^ 5 + N ^ 5 * D + N ^ 5 + ratParamsP.m₀

/-- What allInstancesP needs, for the parameters N, D, w, U. -/
noncomputable def allInstancesNeedP : List ℕ → Need
  | [N, D, _, U] => ⟨wordNeedP N D U, 4 + N + 8 * (N * D) + 222 * ((N + 1) ^ 5) ^ 4, 88 * D + 12⟩
  | _ => ⟨0, 0, 0⟩

/-! ## The limits -/

section need

variable {lim : Limits} {N D₀ w U fr d : ℕ}

end need

/-! ## The routine -/

/-! ## The time in the regime -/

/-! ## The need is polynomial in the parameters -/

section summands

variable {N D U Q : ℕ}

end summands

/-! ## The claim -/

end Light.Sec4
end
end

section
-- Source module: ThreeSumApsp.AllEdges.Passes
/-!
# Two loops over arrays for all pairs from all-edges Exact Triangle

transpose(n, src, dst) writes the transposed `n × n` matrix to dst, one row at a time
(`transpose_meets`).  or(len, dst, src) sets dst[i] to the "or" of two flags (`or_meets`).
-/

@[expose] public section

open ThreeSumApsp

namespace Light.Sec3

open ThreeSumApsp.Spec

variable {lim : Limits} {P : Program} {d : ℕ}

/-! ## A row of the transposed matrix -/

/-- row(n, s, dst): for i < n, dst[i] := mem[s + i n]. -/
def rowBody : Stmt := pass 3 (Light.v 0) (Light.v 2) (M (Light.v 1 +' Light.v 3 *' Light.v 0))

/-- The row `j` of the transposed matrix: the column `j` of `L`. -/
def colOf (n : ℕ) (L : List ℤ) (j : ℕ) : List ℤ := (List.range n).map fun i => L.getD (i * n + j) 0

/-! ## The transposed matrix -/

/-- transpose(n, src, dst): for j < n, row(n, src + j, dst + j n). -/
def transBody (pRow : ℕ) : Stmt := .for 3 (Light.v 0) (.call pRow [Light.v 0, Light.v 1 +' Light.v 3, Light.v 2 +' Light.v 3 *' Light.v 0] 4)

/-- The transposed matrix. -/
def transL (n : ℕ) (L : List ℤ) : List ℤ :=
  (List.range (n * n)).map fun q => L.getD (q % n * n + q / n) 0

/-- The time of transpose. -/
def tTranspose (n : ℕ) : ℕ := 20 * (n * n) + 25 * n + 6

/-! ## Or of flags -/

/-- The flags of a predicate on the numbers below `N`. -/
noncomputable def flagsOf (N : ℕ) (A : ℕ → Prop) : List ℤ := (List.range N).map fun q => flag (A q)

/-- or(len, dst, src): for i < len, dst[i] := dst[i] + src[i] - dst[i] src[i]. -/
def orBody : Stmt :=
  pass 3 (Light.v 0) (Light.v 1) (M (Light.v 1 +' Light.v 3) +' M (Light.v 2 +' Light.v 3) -' M (Light.v 1 +' Light.v 3) *' M (Light.v 2 +' Light.v 3))

end Light.Sec3
end
end

section
-- Source module: ThreeSumApsp.AllEdges.PairsSpec
/-!
# All pairs by prefixes, pair by pair

`X[i,k] + Y[k,j] < V[i,j]` exactly if `−V[i,j] + Yᵀ[j,k] + X[i,k] < 0`, a negative triangle on the
edge `(i, j)`.  As for Negative Triangle, this holds exactly if, at one of the levels `ℓ < L` and
for `e = 2` or `e = 3`, the instance of the prefixes has a zero triangle on the edge `(i, j)`
(`pair_iff_exists_level`).
-/

@[expose] public section

namespace ThreeSumApsp.Spec

/-- The weights `−V`. -/
def negL (V : List ℤ) : List ℤ := affL (-1) 0 V

/-- The prefixes of the first matrix at the level `ℓ`. -/
def pairsQAB (U ℓ : ℕ) (V : List ℤ) : List ℤ := (affL 2 (2 * U) (negL V)).map (prefQ ℓ)

/-- The prefixes of the second matrix at the level `ℓ`. -/
def pairsQBC (n U ℓ : ℕ) (Y : List ℤ) : List ℤ :=
  (affL 2 (2 * U) (Light.Sec3.transL n Y)).map (prefQ ℓ)

end ThreeSumApsp.Spec
end
end