viscous_norm_bound_from_initial

formal source

 217  have : discreteEnergy (u t) ≤ discreteEnergy (u 0) := hAnti ht
 218  simpa using this
 219
 220theorem viscous_norm_bound_from_initial {N : ℕ} (ν : ℝ) (hν : 0 ≤ ν)
 221    (B : ConvectionOp N) (HB : EnergySkewHypothesis B)
 222    (u : ℝ → GalerkinState N)
 223    (hu : ∀ t : ℝ, HasDerivAt u (galerkinNSRHS ν B (u t)) t) :
 224    ∀ t ≥ 0, ‖u t‖ ≤ ‖u 0‖ := by
 225  intro t ht
 226  have hE : discreteEnergy (u t) ≤ discreteEnergy (u 0) :=
 227    viscous_energy_bound_from_initial (N := N) ν hν B HB u hu t ht
 228  have hE' : (1 / 2 : ℝ) * ‖u t‖ ^ 2 ≤ (1 / 2 : ℝ) * ‖u 0‖ ^ 2 := by
 229    simpa [discreteEnergy] using hE
 230  -- Multiply both sides by `2` to cancel the `1/2`.
 231  have hsq : ‖u t‖ ^ 2 ≤ ‖u 0‖ ^ 2 := by
 232    have hmul := mul_le_mul_of_nonneg_left hE' (by norm_num : (0 : ℝ) ≤ 2)
 233    -- `2 * (1/2) = 1`
 234    simpa [mul_assoc] using hmul
 235  -- Convert the square inequality to a norm inequality (norms are nonnegative).
 236  exact le_of_sq_le_sq hsq (norm_nonneg (u 0))
 237
 238end IndisputableMonolith.ClassicalBridge.Fluids