Real.complete

-- COMPLETENESS: a regular sequence of reals converges, and the limit
-- is the DIAGONAL of the representatives, sampled at quarter depth:
--
--   L j = (x_{4j+3})_{4j+3}
--
-- The hypothesis is taken in its pointwise form. "The reals class(x m)
-- and class(x n) are within 1/(m+1) + 1/(n+1)" says, at every index j,
-- that the representatives are within that plus the two moduli 2/(j+1)
-- — and it is that rational statement, not the ℝ-level one, that the
-- construction consumes. (Going the other way is `leQOfArch`'s job and
-- is not needed here.)
--
-- Why the DIAGONAL and why QUARTER depth: the two estimates below each
-- spend four copies of 1/(4k+4), and four copies is exactly 1/(k+1)
-- (qInvQuarter). At half depth the regularity estimate comes out at
-- 1/(m+1) + 2/(n+1) and misses.
--
-- Note this is completeness for a sequence given WITH representatives.
-- Phrasing it for an arbitrary `X : ℕ → Real` would need a choice
-- of representative for each X n, i.e. countable choice, which is not
-- derivable here — the quotient has no section.
-- ===== four quarter-fractions make one =====

import Rat (Q, +, qNeg, qZero, qAddComm, qAddAssoc)
import Rat.order (≤, leQRefl, leQTrans, qPairSwap, leQPlusMono, leQPlusMonoL)
import Rat.bound (Bnd, bndAdd, bndVia, bndEq, bndEqB, bndWeaken, leQAdd, leQSelfAdd)
import Rat.half (dbl, qInvHalf, leQZeroInvNat, leQInvDbl)
import Rat.abs (qAbs, absLeOfBnd)
import Rat.arch (leQSubShift)
import Real (qInvNat, rBound, leQZeroBound, Regular, RSeq, REq, Real, realOfQ, constReg)
import Real.neg (seqOf, regOf, regBnd, bndReg, reqOf, realEqOfREq, rNeg)
import Real.add (rAdd, leQBoundDblDiag)
import Real.abs (rAbs)
import Real.order (RLeP, rleOf, ≤)
import Real.group (-)
import Real.metric (realDist, realDistCls, rleOfAbsSub)
import Real.eq (qtr)
import Core.equality (trans, sym, cong, transport, transportP)

qInvQuarter : {j : ℕ}
  → qInvNat (qtr j) + qInvNat (qtr j) + (qInvNat (qtr j) + qInvNat (qtr j)) ≡ qInvNat j
  using (Rat.half.dbl.eq, Rat.+.eq, Real.qInvNat.eq, Real.eq.qtr.eq)
qInvQuarter =
  λj. trans
    _
    _
    _
    cong
      λw. Q
      λw. w + w
      {qInvNat (qtr j) + qInvNat (qtr j)}
      {qInvNat (dbl j)}
      qInvHalf (dbl j)
    qInvHalf j

-- (a+b) + ((a+b) + (b+b)) ≡ (a+a) + ((b+b) + (b+b)) : both are 2a + 4b
qSum6 : (a b : Q) → a + b + (a + b + (b + b)) ≡ a + a + (b + b + (b + b)) using (Rat.Q.unfold)
qSum6 =
  λa b. a + b + (a + b + (b + b))
    ≡⟨ sym _ _ (qAddAssoc (a + b) (a + b) (b + b)) ⟩ a + b + (a + b) + (b + b)
    ≡⟨ cong (λw. Q) (λw. w + (b + b)) (qPairSwap a b a b) ⟩ a + a + (b + b) + (b + b)
    ≡⟨ qAddAssoc (a + a) (b + b) (b + b) ⟩ a + a + (b + b + (b + b))

-- 2a + 4b sits under 4a + 4b, i.e. under rBound m n
leQQuarterSum : (m n : ℕ)
  → qInvNat (qtr m) + qInvNat (qtr m)
    + (qInvNat (qtr n) + qInvNat (qtr n) + (qInvNat (qtr n) + qInvNat (qtr n)))
    ≤ rBound m n
  using (Core.id.Id.eq,
    Rat.half.dbl.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,
    Real.eq.qtr.eq)
leQQuarterSum =
  λm n. transport
    λw. qInvNat (qtr m) + qInvNat (qtr m)
      + (qInvNat (qtr n) + qInvNat (qtr n) + (qInvNat (qtr n) + qInvNat (qtr n)))
      ≤ w + qInvNat n
    {qInvNat (qtr m) + qInvNat (qtr m) + (qInvNat (qtr m) + qInvNat (qtr m))}
    {qInvNat m}
    qInvQuarter
    transport
      λw. qInvNat (qtr m) + qInvNat (qtr m)
        + (qInvNat (qtr n) + qInvNat (qtr n) + (qInvNat (qtr n) + qInvNat (qtr n)))
        ≤ qInvNat (qtr m) + qInvNat (qtr m) + (qInvNat (qtr m) + qInvNat (qtr m)) + w
      {qInvNat (qtr n) + qInvNat (qtr n) + (qInvNat (qtr n) + qInvNat (qtr n))}
      {qInvNat n}
      qInvQuarter
      leQAdd
        _
        _
        _
        _
        leQSelfAdd
          qInvNat (qtr m) + qInvNat (qtr m)
          transport
            λw. qZero ≤ w
            sym (qInvNat (qtr m) + qInvNat (qtr m)) (qInvNat (dbl m)) (qInvHalf (dbl m))
            leQZeroInvNat (dbl m)
        leQRefl (qInvNat (qtr n) + qInvNat (qtr n) + (qInvNat (qtr n) + qInvNat (qtr n)))

-- ===== the hypothesis =====
-- a regular sequence OF REALS, read off the representatives: at every
-- index j the two representatives are within the reals' separation
-- plus the two moduli
RegSeqR : (ℕ → RSeq) → 𝕌
RegSeqR = λx. (m n j : ℕ) → Bnd (rBound m n + rBound j j) (seqOf (x m) j + qNeg (seqOf (x n) j))

-- ===== the limit =====
limSeq : (ℕ → RSeq) → ℕ → Q using (Rat.Q.unfold)
limSeq = λx j. seqOf (x (qtr j)) (qtr j)

-- |L m − L n| ≤ |x_qm(qm) − x_qm(qn)| + |x_qm(qn) − x_qn(qn)|
--             ≤ (αm + αn)            + ((αm + αn) + (αn + αn))
--             = 2αm + 4αn  ≤  4αm + 4αn  =  rBound m n
limReg : {x : ℕ → RSeq} → RegSeqR x → Regular (limSeq x)
  using (Core.id.Id.eq,
    Rat.bound.Bnd.unfold,
    Rat.order.Sign.eq,
    Rat.order.sPos.eq,
    Rat.order.sZero.eq,
    Rat.order.sgnQ.eq,
    Rat.+.eq,
    Rat.qNeg.eq,
    Real.RSeq.unfold,
    Real.Regular.unfold,
    Real.qInvNat.eq,
    Real.rBound.eq,
    Real.complete.RegSeqR.unfold,
    Real.complete.limSeq.eq,
    Real.eq.qtr.eq,
    Real.neg.seqOf.eq)
limReg =
  λx h. bndReg
    λm n. bndWeaken
      _
      _
      _
      leQQuarterSum m n
      bndEqB
        rBound (qtr m) (qtr n) + (rBound (qtr m) (qtr n) + rBound (qtr n) (qtr n))
        qInvNat (qtr m) + qInvNat (qtr m)
          + (qInvNat (qtr n) + qInvNat (qtr n) + (qInvNat (qtr n) + qInvNat (qtr n)))
        limSeq x m + qNeg (limSeq x n)
        qSum6 (qInvNat (qtr m)) (qInvNat (qtr n))
        bndVia
          _
          _
          seqOf (x (qtr m)) (qtr m)
          _
          seqOf (x (qtr n)) (qtr n)
          regBnd _ (regOf (x (qtr m))) (qtr m) (qtr n)
          h (qtr m) (qtr n) (qtr n)

rLim : (x : ℕ → RSeq) → RegSeqR x → RSeq using (Real.RSeq.unfold)
rLim = λx h. limSeq x, limReg h

realLim : (x : ℕ → RSeq) → RegSeqR x → Real using (Real.Real.unfold)
realLim = λx h. class (rLim _ h)

-- ===== convergence =====
-- (b+a) + ((g+a) + (a+a)) ≡ g + (b + ((a+a)+(a+a))) : both are
-- b + g + 4a, with the four quarter-fractions collected on the right
qSum7 : (b g a : Q) → b + a + (g + a + (a + a)) ≡ g + (b + (a + a + (a + a))) using (Rat.Q.unfold)
qSum7 =
  λb g a. b + a + (g + a + (a + a))
    ≡⟨ sym _ _ (qAddAssoc (b + a) (g + a) (a + a)) ⟩ b + a + (g + a) + (a + a)
    ≡⟨ cong (λw. Q) (λw. w + (a + a)) (qPairSwap b a g a) ⟩ b + g + (a + a) + (a + a)
    ≡⟨ qAddAssoc (b + g) (a + a) (a + a) ⟩ b + g + (a + a + (a + a))
    ≡⟨ cong (λw. Q) (λw. w + (a + a + (a + a))) (qAddComm b g) ⟩ g + b + (a + a + (a + a))
    ≡⟨ qAddAssoc g b (a + a + (a + a)) ⟩ g + (b + (a + a + (a + a)))

-- |x_n(j) − L(j)| ≤ |x_n(j) − x_n(qj)| + |x_n(qj) − x_qj(qj)|
--                ≤ (β + α)            + ((γ + α) + (α + α))
--                = β + γ + 4α  =  γ + 2β  =  1/(n+1) + 2/(j+1)
-- — an equality, not a weakening: quarter depth is exactly enough
limClose : (x : ℕ → RSeq)
  (h : RegSeqR x)
  (n j : ℕ)
  → Bnd (qInvNat n + rBound j j) (seqOf (x n) j + qNeg (limSeq x j))
  using (Core.id.Id.eq,
    Rat.bound.Bnd.unfold,
    Rat.order.Sign.eq,
    Rat.order.sPos.eq,
    Rat.order.sZero.eq,
    Rat.order.sgnQ.eq,
    Rat.+.eq,
    Rat.qNeg.eq,
    Real.RSeq.unfold,
    Real.qInvNat.eq,
    Real.rBound.eq,
    Real.complete.RegSeqR.unfold,
    Real.complete.limSeq.eq,
    Real.eq.qtr.eq,
    Real.neg.seqOf.eq)
limClose =
  λx h n j. bndEqB
    _
    _
    _
    trans
      rBound j (qtr j) + (rBound n (qtr j) + rBound (qtr j) (qtr j))
      qInvNat n
        + (qInvNat j + (qInvNat (qtr j) + qInvNat (qtr j) + (qInvNat (qtr j) + qInvNat (qtr j))))
      qInvNat n + rBound j j
      qSum7 (qInvNat j) (qInvNat n) (qInvNat (qtr j))
      cong
        λw. Q
        λw. qInvNat n + (qInvNat j + w)
        {qInvNat (qtr j) + qInvNat (qtr j) + (qInvNat (qtr j) + qInvNat (qtr j))}
        {qInvNat j}
        qInvQuarter
    bndVia _ _ _ _ _ (regBnd _ (regOf (x n)) j (qtr j)) (h n (qtr j) (qtr j))

-- ===== the theorem, at the level of ℝ =====
-- d(X n, L) ≤ 1/(n+1). The pointwise estimate is taken at the doubled
-- index the distance samples at, where the modulus rBound (2j+1)(2j+1)
-- is exactly 1/(j+1) and so sits under rBound j j.
realLimClose : (x : ℕ → RSeq)
  (h : RegSeqR x)
  (n : ℕ)
  → realDist (class (x n)) (realLim _ h) ≤ realOfQ (qInvNat n)
  using (Real.Real.unfold,
    Real.RSeq.unfold,
    Real.Regular.unfold,
    Real.realOfQ.eq,
    Real.complete.realLim.eq,
    Real.complete.rLim.eq,
    Real.neg.seqOf.eq,
    Real.order.≤.eq)
realLimClose =
  λx h n. transportP
    {Real}
    λv. v ≤ realOfQ (qInvNat n)
    {class (rAbs (rAdd (x n) (rNeg (rLim _ h))))}
    sym
      realDist (class (x n)) (realLim _ h)
      class (rAbs (rAdd (x n) (rNeg (rLim _ h))))
      realDistCls (x n) (rLim _ h)
    rleOfAbsSub
      rLim _ h
      λj. absLeOfBnd
        bndWeaken
          _
          _
          seqOf (x n) (dbl j) + qNeg (seqOf (rLim _ h) (dbl j))
          leQPlusMonoL _ _ (qInvNat n) (leQBoundDblDiag j)
          limClose _ h n (dbl j)

-- ...and the hypothesis really does say what it should: a pointwise
-- RegSeqR makes the reals themselves 1/(m+1) + 1/(n+1)-close)
regSeqRSound : (x : ℕ → RSeq)
  (h : RegSeqR x)
  (m n : ℕ)
  → realDist (class (x m)) (class (x n)) ≤ realOfQ (rBound m n)
  using (Real.Real.unfold,
    Real.RSeq.unfold,
    Real.Regular.unfold,
    Real.realOfQ.eq,
    Real.order.≤.eq,
    Real.complete.RegSeqR.unfold)
regSeqRSound =
  λx h m n. transportP
    {Real}
    λv. v ≤ realOfQ (rBound m n)
    {class (rAbs (rAdd (x m) (rNeg (x n))))}
    sym _ _ (realDistCls (x m) (x n))
    rleOfAbsSub
      x n
      λj. absLeOfBnd
        bndWeaken _ _ _ (leQPlusMonoL _ _ (rBound m n) (leQBoundDblDiag j)) (h m n (dbl j))