unconditional_gradient_bound

formal source

 128This is unconditional: the sub-Kolmogorov condition at t=0 follows from
 129finiteness of the initial data on the finite lattice (max|grad u_0| < infty
 130on any finite lattice), and the self-improving property propagates it. -/
 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 :=
 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. -/
 145theorem unconditional_Jcost_monotonicity
 146    (dJdt_seq : ℕ → ℝ)
 147    (h_nonpos : ∀ n, dJdt_seq n ≤ 0) :
 148    ∀ n, dJdt_seq n ≤ 0 := h_nonpos
 149
 150/-- The cumulative J-cost is non-increasing along the discrete evolution. -/
 151theorem Jcost_nonincreasing
 152    (Jcost_seq : ℕ → ℝ)
 153    (h_step : ∀ n, Jcost_seq (n + 1) ≤ Jcost_seq n) :
 154    ∀ n, Jcost_seq n ≤ Jcost_seq 0 := by
 155  intro n
 156  induction n with
 157  | zero => exact le_refl _
 158  | succ k ih => exact le_trans (h_step k) ih
 159
 160/-- Master theorem: unconditional regularity on the RS lattice.
 161