For all L , t ∈ N \htmlData{mx=1}{L, t \in \htmlData{mx=0}{\mathbb{N}}} L , t ∈ N β 1 , β 2 , ε , η , l a m ∈ R \htmlData{mx=1}{\beta_{1}, \beta_{2}, \varepsilon, \eta, \mathit{lam} \in \htmlData{mx=0}{\mathbb{R}}} β 1 , β 2 , ε , η , lam ∈ R g , m , v , θ : N → N → R \htmlData{mx=5}{g, m, v, \theta : \htmlData{mx=0}{\mathbb{N}} \mathrel{\htmlData{mx=4}{\to}} \htmlData{mx=1}{\mathbb{N}} \mathrel{\htmlData{mx=3}{\to}} \htmlData{mx=2}{\mathbb{R}}} g , m , v , θ : N → N → R x , z : N → R \htmlData{mx=3}{x, z : \htmlData{mx=0}{\mathbb{N}} \mathrel{\htmlData{mx=2}{\to}} \htmlData{mx=1}{\mathbb{R}}} x , z : N → R 0 ≤ β 1 0 \mathrel{\htmlData{mx=1}{\leq}} \htmlData{mx=0}{\beta_{1}} 0 ≤ β 1 β 1 < 1 \htmlData{mx=0}{\beta_{1}} \mathrel{\htmlData{mx=1}{<}} 1 β 1 < 1 0 < β 2 0 \mathrel{\htmlData{mx=1}{<}} \htmlData{mx=0}{\beta_{2}} 0 < β 2 β 2 < 1 \htmlData{mx=0}{\beta_{2}} \mathrel{\htmlData{mx=1}{<}} 1 β 2 < 1 β 1 2 < β 2 \htmlData{mx=1}{\htmlData{mx=0}{\beta_{1}}^{2}} \mathrel{\htmlData{mx=3}{<}} \htmlData{mx=2}{\beta_{2}} β 1 2 < β 2 0 < ε 0 \mathrel{\htmlData{mx=1}{<}} \htmlData{mx=0}{\varepsilon} 0 < ε 0 ≤ η 0 \mathrel{\htmlData{mx=1}{\leq}} \htmlData{mx=0}{\eta} 0 ≤ η 0 < l a m 0 \mathrel{\htmlData{mx=1}{<}} \htmlData{mx=0}{\mathit{lam}} 0 < lam η ⋅ l a m ≤ 1 \htmlData{mx=2}{\htmlData{mx=0}{\eta} \cdot \htmlData{mx=1}{\mathit{lam}}} \mathrel{\htmlData{mx=3}{\leq}} 1 η ⋅ lam ≤ 1 ∀ l , m ( l , 0 ) = 0 \htmlData{mx=4}{\forall l,\ \htmlData{mx=2}{\htmlData{mx=0}{m}(\htmlData{mx=1}{l}, 0)} \mathrel{\htmlData{mx=3}{=}} 0} ∀ l , m ( l , 0 ) = 0 ∀ l , v ( l , 0 ) = 0 \htmlData{mx=4}{\forall l,\ \htmlData{mx=2}{\htmlData{mx=0}{v}(\htmlData{mx=1}{l}, 0)} \mathrel{\htmlData{mx=3}{=}} 0} ∀ l , v ( l , 0 ) = 0 ∀ l , s , m ( l , s + 1 ) = β 1 ⋅ m ( l , s ) + ( 1 − β 1 ) ⋅ g ( l , s ) \htmlData{mx=20}{\forall l, s,\ \htmlData{mx=4}{\htmlData{mx=0}{m}(\htmlData{mx=1}{l}, \htmlData{mx=3}{\htmlData{mx=2}{s} + 1})} \mathrel{\htmlData{mx=19}{=}} \htmlData{mx=18}{\htmlData{mx=10}{\htmlData{mx=5}{\beta_{1}} \cdot \htmlData{mx=9}{\htmlData{mx=6}{m}(\htmlData{mx=7}{l}, \htmlData{mx=8}{s})}} + \htmlData{mx=17}{(\htmlData{mx=12}{1 - \htmlData{mx=11}{\beta_{1}}}) \cdot \htmlData{mx=16}{\htmlData{mx=13}{g}(\htmlData{mx=14}{l}, \htmlData{mx=15}{s})}}}} ∀ l , s , m ( l , s + 1 ) = β 1 ⋅ m ( l , s ) + ( 1 − β 1 ) ⋅ g ( l , s ) ∀ l , s , v ( l , s + 1 ) = β 2 ⋅ v ( l , s ) + ( 1 − β 2 ) ⋅ g ( l , s ) 2 \htmlData{mx=21}{\forall l, s,\ \htmlData{mx=4}{\htmlData{mx=0}{v}(\htmlData{mx=1}{l}, \htmlData{mx=3}{\htmlData{mx=2}{s} + 1})} \mathrel{\htmlData{mx=20}{=}} \htmlData{mx=19}{\htmlData{mx=10}{\htmlData{mx=5}{\beta_{2}} \cdot \htmlData{mx=9}{\htmlData{mx=6}{v}(\htmlData{mx=7}{l}, \htmlData{mx=8}{s})}} + \htmlData{mx=18}{(\htmlData{mx=12}{1 - \htmlData{mx=11}{\beta_{2}}}) \cdot \htmlData{mx=17}{\htmlData{mx=16}{\htmlData{mx=13}{g}(\htmlData{mx=14}{l}, \htmlData{mx=15}{s})}^{2}}}}} ∀ l , s , v ( l , s + 1 ) = β 2 ⋅ v ( l , s ) + ( 1 − β 2 ) ⋅ g ( l , s ) 2 ∀ l , ∣ θ ( l , 0 ) ∣ ≤ 1 \htmlData{mx=5}{\forall l,\ \htmlData{mx=3}{\left\lvert \htmlData{mx=2}{\htmlData{mx=0}{\theta}(\htmlData{mx=1}{l}, 0)} \right\rvert} \mathrel{\htmlData{mx=4}{\leq}} 1} ∀ l , ∣ θ ( l , 0 ) ∣ ≤ 1 ∀ l , s , θ ( l , s + 1 ) = ( 1 − η ⋅ l a m ) ⋅ θ ( l , s ) − η ⋅ ( 1 − β 2 s + 1 1 − β 1 s + 1 ⋅ m ( l , s + 1 ) v ( l , s + 1 ) + ε ⋅ 1 − β 2 s + 1 ) \htmlData{mx=52}{\forall l, s,\ \htmlData{mx=4}{\htmlData{mx=0}{\theta}(\htmlData{mx=1}{l}, \htmlData{mx=3}{\htmlData{mx=2}{s} + 1})} \mathrel{\htmlData{mx=51}{=}} \htmlData{mx=50}{\htmlData{mx=13}{(\htmlData{mx=8}{1 - \htmlData{mx=7}{\htmlData{mx=5}{\eta} \cdot \htmlData{mx=6}{\mathit{lam}}}}) \cdot \htmlData{mx=12}{\htmlData{mx=9}{\theta}(\htmlData{mx=10}{l}, \htmlData{mx=11}{s})}} - \htmlData{mx=49}{\htmlData{mx=14}{\eta} \cdot \left(\htmlData{mx=48}{\frac{\htmlData{mx=32}{\htmlData{mx=26}{\frac{\htmlData{mx=20}{\sqrt{\htmlData{mx=19}{1 - \htmlData{mx=18}{\htmlData{mx=15}{\beta_{2}}^{\htmlData{mx=17}{\htmlData{mx=16}{s} + 1}}}}}}}{\htmlData{mx=25}{1 - \htmlData{mx=24}{\htmlData{mx=21}{\beta_{1}}^{\htmlData{mx=23}{\htmlData{mx=22}{s} + 1}}}}}} \cdot \htmlData{mx=31}{\htmlData{mx=27}{m}(\htmlData{mx=28}{l}, \htmlData{mx=30}{\htmlData{mx=29}{s} + 1})}}}{\htmlData{mx=47}{\htmlData{mx=38}{\sqrt{\htmlData{mx=37}{\htmlData{mx=33}{v}(\htmlData{mx=34}{l}, \htmlData{mx=36}{\htmlData{mx=35}{s} + 1})}}} + \htmlData{mx=46}{\htmlData{mx=39}{\varepsilon} \cdot \htmlData{mx=45}{\sqrt{\htmlData{mx=44}{1 - \htmlData{mx=43}{\htmlData{mx=40}{\beta_{2}}^{\htmlData{mx=42}{\htmlData{mx=41}{s} + 1}}}}}}}}}}\right)}}} ∀ l , s , θ ( l , s + 1 ) = ( 1 − η ⋅ lam ) ⋅ θ ( l , s ) − η ⋅ ( v ( l , s + 1 ) + ε ⋅ 1 − β 2 s + 1 1 − β 1 s + 1 1 − β 2 s + 1 ⋅ m ( l , s + 1 ) ) ∀ l , ∣ z ( l ) ∣ < 2 \htmlData{mx=5}{\forall l,\ \htmlData{mx=3}{\left\lvert \htmlData{mx=2}{\htmlData{mx=0}{z}(\htmlData{mx=1}{l})} \right\rvert} \mathrel{\htmlData{mx=4}{<}} 2} ∀ l , ∣ z ( l ) ∣ < 2 ∀ l , x ( l + 1 ) = x ( l ) + θ ( l , t ) ⋅ z ( l ) \htmlData{mx=17}{\forall l,\ \htmlData{mx=3}{\htmlData{mx=0}{x}(\htmlData{mx=2}{\htmlData{mx=1}{l} + 1})} \mathrel{\htmlData{mx=16}{=}} \htmlData{mx=15}{\htmlData{mx=6}{\htmlData{mx=4}{x}(\htmlData{mx=5}{l})} + \htmlData{mx=14}{\htmlData{mx=10}{\htmlData{mx=7}{\theta}(\htmlData{mx=8}{l}, \htmlData{mx=9}{t})} \cdot \htmlData{mx=13}{\htmlData{mx=11}{z}(\htmlData{mx=12}{l})}}}} ∀ l , x ( l + 1 ) = x ( l ) + θ ( l , t ) ⋅ z ( l )
∣ x ( L ) ∣ ≤ ∣ x ( 0 ) ∣ + L ⋅ ( 2 max ( 1 , ( 1 − β 1 ) 2 ( 1 − β 2 ) ⋅ ( 1 − β 1 2 β 2 ) 1 − β 1 l a m ) ) \begin{aligned} & \htmlData{mx=4}{\left\lvert \htmlData{mx=3}{\htmlData{mx=1}{x}(\htmlData{mx=2}{L})} \right\rvert} \\ & \quad \htmlData{mx=0}{\leq} \htmlData{mx=30}{\htmlData{mx=7}{\left\lvert \htmlData{mx=6}{\htmlData{mx=5}{x}(0)} \right\rvert} + \htmlData{mx=29}{\htmlData{mx=8}{L} \cdot \left(\htmlData{mx=28}{2\htmlData{mx=27}{\max(1, \htmlData{mx=26}{\frac{\htmlData{mx=24}{\frac{\htmlData{mx=21}{\sqrt{\htmlData{mx=20}{\frac{\htmlData{mx=11}{(\htmlData{mx=10}{1 - \htmlData{mx=9}{\beta_{1}}})^{2}}}{\htmlData{mx=19}{(\htmlData{mx=13}{1 - \htmlData{mx=12}{\beta_{2}}}) \cdot \left(\htmlData{mx=18}{1 - \htmlData{mx=17}{\frac{\htmlData{mx=15}{\htmlData{mx=14}{\beta_{1}}^{2}}}{\htmlData{mx=16}{\beta_{2}}}}}\right)}}}}}}{\htmlData{mx=23}{1 - \htmlData{mx=22}{\beta_{1}}}}}}{\htmlData{mx=25}{\mathit{lam}}}})}}\right)}} \end{aligned} ∣ x ( L ) ∣ ≤ ∣ x ( 0 ) ∣ + L ⋅ 2 max ( 1 , lam 1 − β 1 ( 1 − β 2 ) ⋅ ( 1 − β 2 β 1 2 ) ( 1 − β 1 ) 2 ) What the notation means · or point at any symbol
N Natural numbers The natural numbers 0, 1, 2, …. In Lean they start at 0. (ℕ)
x ∈ T Variables L, t range over natural numbers: the statement must hold for every choice. ((L t : ℕ))
R Real numbers The real numbers: every point on the number line. (ℝ)
≤ At most 0 is less than or equal to β₁. (0 ≤ β₁)
< Less than β₁ is strictly smaller than 1. (β₁ < 1)
aᵇ Power β₁ raised to the power 2. (β₁ ^ 2)
· Multiplication η times lam. (η * lam)
x : T Variables g, m, v, θ range over ℕ → ℕ → ℝ: the statement must hold for every choice. ((g m v θ : ℕ → ℕ → ℝ))
∀ For all The statement after the comma holds for every l. (∀ l, m l 0 = 0)
⟹ Implies If ℕ, then ℝ. (Between types, A → B is the type of functions from A to B.) (ℕ → ℝ)
f(x) Function application m applied to l, 0. Lean writes f x; papers write f(x). (m l 0)
= Equality m(l, 0) and 0 are the same. (m l 0 = 0)
|x| Absolute value The size of θ(l, 0) without its sign. (|θ l 0|)
+ Addition s plus 1. (s + 1)
max Maximum The larger of 1 and √((1 − β₁)^2/((1 − β₂) · (1 − β₁^2/β₂)))/(1 − β₁)/lam. (max 1 (Real.sqrt ((1 - β₁) ^ 2 / ((1 - …)
- Subtraction 1 minus β₁. On ℕ, Lean's subtraction stops at 0: 2 − 5 = 0. (1 - β₁)
√ Square root The non-negative number whose square is 1 − β₂^(s + 1). (Real.sqrt (1 - β₂ ^ (s + 1)))
a/b Division √(1 − β₂^(s + 1)) divided by 1 − β₁^(s + 1). In Lean, dividing by 0 gives 0. (Real.sqrt (1 - β₂ ^ (s + 1)) / (1 - β₁ …)