Real.bound

-- EVERY REGULAR SEQUENCE IS BOUNDED, by a natural computed from it:
--
--   |x_n|  ≤  |x_0| + |x_n − x_0|  ≤  ⌈|x_0|⌉ + 2
--
-- and ⌈|x_0|⌉ is ratCeil's qNatBound, a genuine function on ℚ. This is
-- what ℝ's product needs: the sampling depth for x·y is proportional
-- to a bound on both factors, so the bound has to be data computed
-- from the representative — and it is.
-- ===== 1/(k+1) ≤ 1, hence rBound n 0 ≤ 2 =====

import Natural (+, *, plusZeroId, zeroPlusId)
import Natural.order (≤, leZero, leSucMono)
import Rat.frac (oneMult)
import Rat (Q, +, qNeg, qZero, qAddComm, qAddAssoc, qAddNegR, qAddZeroL)
import Rat.order (≤, leQRefl, leQTrans)
import Rat.bound (Bnd, bndAdd, bndEq, bndWeaken, leQAdd)
import Rat.nat (qOfNat, qOfNatAdd, leQOfNat)
import Rat.ceil (qNatBound, bndNatBound, leQFracOfNat)
import Real (qInvNat, rBound, RSeq, Regular)
import Real.neg (seqOf, regOf, regBnd)
import Core.equality (trans, sym, cong, transport)

leQInvOne : (k : ℕ) → qInvNat k ≤ qOfNat (S Z)
  using (Core.id.Id.eq,
    Int.order.intOfNat.eq,
    Int.intOne.eq,
    Rat.nat.qOfNat.eq,
    Rat.frac.mkRat.eq,
    Rat.frac.nzOne.eq,
    Rat.frac.nzPos.eq,
    Rat.frac.ratAdd.eq,
    Rat.frac.ratNeg.eq,
    Rat.order.≤.unfold,
    Rat.order.NonNegS.unfold,
    Rat.order.Sign.eq,
    Rat.order.ratSgn.eq,
    Rat.order.sPos.eq,
    Rat.order.sZero.eq,
    Rat.order.sgnQ.eq,
    Rat.+.eq,
    Rat.qNeg.eq,
    Rat.qcls.eq,
    Real.qInvNat.eq)
leQInvOne =
  λk. leQFracOfNat (transport (λw. S Z ≤ w) (sym _ _ (oneMult (S k))) (leSucMono (leZero k)))

leQBoundTwo : (n : ℕ) → rBound n Z ≤ qOfNat 2
  using (Core.id.Id.eq,
    Natural.+.eq,
    Rat.nat.qOfNat.eq,
    Rat.order.≤.unfold,
    Rat.order.NonNegS.unfold,
    Rat.order.Sign.eq,
    Rat.order.sPos.eq,
    Rat.order.sZero.eq,
    Rat.order.sgnQ.eq,
    Rat.+.eq,
    Rat.qNeg.eq,
    Real.qInvNat.eq,
    Real.rBound.eq)
leQBoundTwo =
  λn. transport
    λw. rBound n Z ≤ w
    {qOfNat (S Z) + qOfNat (S Z)}
    {qOfNat 2}
    qOfNatAdd (S Z) (S Z)
    leQAdd _ _ _ _ (leQInvOne n) (leQInvOne Z)

-- ===== a + (b − a) ≡ b =====
qAddSubCancelL : (a b : Q) → a + (b + qNeg a) ≡ b using (Rat.Q.unfold)
qAddSubCancelL =
  λa b. a + (b + qNeg a)
    ≡⟨ cong (λw. Q) (λw. a + w) (qAddComm b (qNeg a)) ⟩ a + (qNeg a + b)
    ≡⟨ sym _ _ (qAddAssoc a (qNeg a) b) ⟩ a + qNeg a + b
    ≡⟨ cong (λw. Q) (λw. w + b) (qAddNegR a) ⟩ qZero + b
    ≡⟨ qAddZeroL b ⟩ b

-- ===== the bound =====
seqBound : RSeq → ℕ
seqBound = λp. S (S (qNatBound (seqOf p Z)))

bndSeqBound : (p : RSeq) (n : ℕ) → Bnd (qOfNat (seqBound p)) (seqOf p n)
  using (Natural.+.eq,
    Rat.bound.Bnd.unfold,
    Rat.ceil.qNatBound.eq,
    Real.RSeq.unfold,
    Real.Regular.unfold,
    Real.bound.seqBound.eq,
    Real.neg.seqOf.eq)
bndSeqBound =
  λp n. bndWeaken
    _
    _
    _
    transport
      λw. qOfNat (qNatBound (seqOf p Z)) + rBound n Z ≤ w
      {qOfNat (qNatBound (seqOf p Z)) + qOfNat 2}
      {qOfNat (seqBound p)}
      qOfNatAdd (qNatBound (seqOf p Z)) 2
      leQAdd _ _ _ _ (leQRefl (qOfNat (qNatBound (seqOf p Z)))) (leQBoundTwo n)
    bndEq
      _
      _
      qAddSubCancelL (seqOf p Z) (seqOf p n)
      bndAdd (bndNatBound (seqOf p Z)) (regBnd _ (regOf p) n Z)

-- the bound is a successor, and in fact at least 2 — which is what
-- lets the product's sampling index be written without a predecessor
seqBoundPos : {p : RSeq} → qZero ≤ qOfNat (seqBound p)
  using (Rat.nat.qOfNatZero,
    Rat.order.≤.unfold,
    Rat.order.NonNegS.unfold,
    Rat.Q.unfold,
    Real.RSeq.unfold,
    Real.Regular.unfold)
seqBoundPos =
  λp. transport (λw. w ≤ qOfNat (seqBound p)) {qOfNat Z} {qZero} ⋆ (leQOfNat (leZero (seqBound p)))