Provedattentionresidual-seriesexternal-review-4
Residual series: complete finite-history probability, mean and variance
For all , and , if , , , , , , and (given ), then
What the notation means · or point at any symbol
- Type
- Type: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (
Type) - Fintype
- Fintype: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (
Fintype) - f(x)Function application
- Fintype applied to J. Lean writes f x; papers write f(x). (
Fintype J) - ⟹Implies
- If J, then ℝ. (Between types, A → B is the type of functions from A to B.) (
J → ℝ) - x : TVariables
- r, h, R range over J → ℝ: the statement must hold for every choice. (
(r h R : J → ℝ)) - x ∈ TVariables
- ρ, θ, q, d, V range over real numbers: the statement must hold for every choice. (
(ρ θ q d V : ℝ)) - ∀For all
- The statement after the comma holds for every j. (
∀ j, 0 ≤ r j) - ∑Summation
- Add up r(j) for every j. (
∑ j, r j) - =Equality
- ∑ j, r(j) and 1 are the same. (
∑ j, r j = 1) - <Less than
- 0 is strictly smaller than ρ. (
0 < ρ) - a/bDivision
- ∑ j, r(j) · R(j)^2 divided by 1 − ρ. In Lean, dividing by 0 gives 0. (
(∑ j, r j * R j ^ 2) / (1 - ρ)) - RReal numbers
- The real numbers: every point on the number line. (
ℝ) - ≤At most
- 0 is less than or equal to r(j). (
0 ≤ r j) - ·Multiplication
- r(j) times h(j). (
r j * h j) - NNatural numbers
- The natural numbers 0, 1, 2, …. In Lean they start at 0. (
ℕ) - aᵇPower
- h(j) raised to the power 2. (
h j ^ 2) - Fin
- Fin: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (
Fin) - -Subtraction
- 1 minus θ. On ℕ, Lean's subtraction stops at 0: 2 − 5 = 0. (
1 - θ) - ×Product
- Pairs of an element of J and an element of Bool. (
J × Bool) - Bool
- Bool: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (
Bool) - ∏Product
- Multiply together r(f(i)).1 · ρ if f(i).2, else 1 − ρ for every i. (
∏ i, r (f i).1 * (if (f i).2 then ρ els…) - p₁Component
- Component 1 of r(f(i)) (the first). (
r (f i).1) - +Addition
- V plus d^2. (
V + d ^ 2) - { a if c; b otherwiseCases (if … then … else)
- ρ when f(i).2, and 1 − ρ otherwise. (
if (f i).2 then ρ else 1 - ρ) - ∧And
- Both hold: (∑ f, (∏ i, r(f(i)).1 · ρ if f(i).2, else 1 − ρ) · foldr(o…, and (∑ f, (∏ i, r(f(i)).1 · ρ if f(i).2, else 1 − ρ) · (foldr(…. (
(∑ f : Fin L → J × Bool, (∏ i, r (f i).…) - e.ffoldr
- foldr of ofFn(f): Lean's dot notation e.foldr means foldr applied to e. (
(List.ofFn f).foldr) - ofFn
- List.ofFn: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (
List.ofFn) - x ↦ f(x)Function (λ-abstraction)
- The function sending z, tail to h(z.1)/ρ · tail if z.2, else R(z.1)/(1 − ρ). Lean writes fun x => …; papers write x ↦ …. (
fun z tail => if z.2 then (h z.1 / ρ) *…)
theorem residual-series-finite-history {J : Type} [Fintype J] (r h R : J → ℝ) (ρ θ q d V : ℝ) (hr : ∀ j, 0 ≤ r j) (hrs : ∑ j, r j = 1) (hρ0 : 0 < ρ) (hρ1 : ρ < 1) (hθ : ∑ j, r j * h j = θ) (hR : ∑ j, r j * R j = (1 - θ) * d) (hq : ∑ j, r j * h j ^ 2 = ρ * q) (hQ : (∑ j, r j * R j ^ 2) / (1 - ρ) = (1 - q) * (V + d ^ 2)) :
∀ L : ℕ, (∀ f : Fin L → J × Bool, 0 ≤ ∏ i, r (f i).1 * (if (f i).2 then ρ else 1 - ρ)) ∧ (∑ f : Fin L → J × Bool, ∏ i, r (f i).1 * (if (f i).2 then ρ else 1 - ρ)) = 1 ∧ (∑ f : Fin L → J × Bool, (∏ i, r (f i).1 * (if (f i).2 then ρ else 1 - ρ)) * (List.ofFn f).foldr (fun z tail => if z.2 then (h z.1 / ρ) * tail else R z.1 / (1 - ρ)) d) = d ∧ (∑ f : Fin L → J × Bool, (∏ i, r (f i).1 * (if (f i).2 then ρ else 1 - ρ)) * ((List.ofFn f).foldr (fun z tail => if z.2 then (h z.1 / ρ) * tail else R z.1 / (1 - ρ)) d - d) ^ 2) = (1 - q ^ L) * VDefines actual finite independent reference-key/geometric-branch path probabilities and terminal/prefix/dense-tail fold. Proves nonnegative normalized weights, exact mean and centered second moment for every deadline. The stationary variance parameter is explicitly related to one-step raw moments; the unbounded probability space and vector variance remain paper proofs.
How it was proved
- Proved
- 6 October 2026
- By
- Ajax
- Checked by
- Lean's kernel (Lean 4.33.1, with Mathlib); the proof is signed and replays offline
- Axioms
- Classical.choice, Quot.sound, propext
- Proof
- 85 lines of Lean
Sign in to see the proofThe proof, its signed report and its history.