theorem
proved
term proof
unconditional_gradient_bound
show as:
view Lean formalization →
formal statement (Lean)
131theorem unconditional_gradient_bound
132 (gradients : ℕ → ℝ) (nu h : ℝ) (hnu : 0 < nu) (hh : 0 < h)
133 (h_finite_init : gradients 0 ≤ nu / h ^ 2)
134 (h_nonincreasing : ∀ n, gradients (n + 1) ≤ gradients n) :
135 ∀ n, gradients n ≤ nu / h ^ 2 :=
proof body
Term-mode proof.
136 subK_propagation gradients (nu / h ^ 2) h_finite_init h_nonincreasing
137
138/-! ## Unconditional J-Cost Monotonicity
139
140Combining the self-improving sub-Kolmogorov condition with the
141previously proved J-cost monotonicity theorem: -/
142
143/-- The J-cost derivative is nonpositive at every time step.
144This is the unconditional lattice monotonicity theorem. -/