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
proof body
Term-mode proof.
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. -/
used by (1)
From the project-wide theorem graph. These declarations reference this one in their body.