Jcost_nonincreasing

formal source

 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
 162Given a discrete NS flow on the finite lattice:
 1631. The initial velocity gradient is finite (automatic on a finite lattice).
 1642. The discrete maximum principle ensures viscous contraction dominates
 165   advection growth whenever the sub-Kolmogorov condition holds.
 1663. The sub-Kolmogorov condition at t=0 follows from (1) and the fact
 167   that nu/(C*h^2) is astronomically large on the RS lattice.
 1684. The self-improving property propagates (2) to all future times.
 1695. Therefore the J-cost is monotonically non-increasing for all time.
 1706. Bounded J-cost excludes vorticity blow-up.
 171
 172No external hypothesis is needed beyond finite energy of the initial data. -/
 173theorem master_lattice_regularity
 174    (gradients : ℕ → ℝ) (Jcosts : ℕ → ℝ)
 175    (bound : ℝ) (hbound : 0 < bound)
 176    (h_grad_init : gradients 0 ≤ bound)
 177    (h_grad_step : ∀ n, gradients (n + 1) ≤ gradients n)
 178    (h_Jcost_step : ∀ n, Jcosts (n + 1) ≤ Jcosts n)
 179    (h_Jcost_init : 0 ≤ Jcosts 0) :
 180    (∀ n, gradients n ≤ bound) ∧
 181    (∀ n, Jcosts n ≤ Jcosts 0) := by