LeanPool.RlTheoryInLean.StochasticApproximation.DiscreteGronwall

theorem StochasticApproximation.discrete_gronwall_aux {u b c : ℕ → ℝ} {n₀ : ℕ} (hu : ∀ n ≥ n₀, u (n + 1) ≤ (1 + c n) * u n + b n) (hc : ∀ n ≥ n₀, c n ≥ 0) (n : ℕ) : n₀ ≤ n → u n ≤ u n₀ * ∏ i ∈ Finset.Ico n₀ n, (1 + c i) + ∑ k ∈ Finset.Ico n₀ n, b k * ∏ i ∈ Finset.Ico (k + 1) n, (1 + c i)

theorem StochasticApproximation.discrete_gronwall {u b c : ℕ → ℝ} {n₀ : ℕ} (hun₀ : 0 ≤ u n₀) (hu : ∀ n ≥ n₀, u (n + 1) ≤ (1 + c n) * u n + b n) (hc : ∀ n ≥ n₀, c n ≥ 0) (hb : ∀ n ≥ n₀, b n ≥ 0) (n : ℕ) : n₀ ≤ n → u n ≤ (u n₀ + ∑ k ∈ Finset.Ico n₀ n, b k) * Real.exp (∑ i ∈ Finset.Ico n₀ n, c i)

theorem StochasticApproximation.discrete_gronwall_Ico {u b c : ℕ → ℝ} {n₀ n₁ : ℕ} (hun₀ : 0 ≤ u n₀) (hu : ∀ n ≥ n₀, u (n + 1) ≤ (1 + c n) * u n + b n) (hc : ∀ n ≥ n₀, c n ≥ 0) (hb : ∀ n ≥ n₀, b n ≥ 0) (n : ℕ) : n ∈ Finset.Ico n₀ n₁ → u n ≤ (u n₀ + ∑ k ∈ Finset.Ico n₀ n₁, b k) * Real.exp (∑ i ∈ Finset.Ico n₀ n₁, c i)