coeff_bound_of_uniformBounds

formal source

1141
1142/-- Derived fact: if the approximants are uniformly bounded in the Galerkin norm for `t ≥ 0`,
1143then the limit coefficients inherit the same bound (by closedness of `closedBall`). -/
1144theorem coeff_bound_of_uniformBounds {H : UniformBoundsHypothesis} (HC : ConvergenceHypothesis H) :
1145    ∀ t ≥ 0, ∀ k : Mode2, ‖(HC.u t) k‖ ≤ H.B := by
1146  intro t ht k
1147  -- Put every approximant coefficient inside the closed ball of radius `B`.
1148  have hmem :
1149      ∀ N : ℕ, (extendByZero (H.uN N t) k) ∈ Metric.closedBall (0 : VelCoeff) H.B := by
1150    intro N
1151    have h1 : ‖(extendByZero (H.uN N t)) k‖ ≤ ‖H.uN N t‖ :=
1152      norm_extendByZero_le (u := H.uN N t) (k := k)
1153    have h2 : ‖H.uN N t‖ ≤ H.B := H.bound N t ht
1154    have h3 : ‖(extendByZero (H.uN N t)) k‖ ≤ H.B := le_trans h1 h2
1155    -- `Metric.mem_closedBall` is `dist ≤ radius`, and `dist x 0 = ‖x‖`.
1156    simpa [Metric.mem_closedBall, dist_zero_right] using h3
1157
1158  have hmem_event :
1159      (∀ᶠ N : ℕ in atTop, (extendByZero (H.uN N t) k) ∈ Metric.closedBall (0 : VelCoeff) H.B) :=
1160    Filter.Eventually.of_forall hmem
1161
1162  have hlim_mem :
1163      (HC.u t) k ∈ Metric.closedBall (0 : VelCoeff) H.B :=
1164    IsClosed.mem_of_tendsto (b := atTop) Metric.isClosed_closedBall (HC.converges t k) hmem_event
1165
1166  have : dist ((HC.u t) k) (0 : VelCoeff) ≤ H.B :=
1167    (Metric.mem_closedBall).1 hlim_mem
1168
1169  simpa [dist_zero_right] using this
1170
1171/-- If the approximants satisfy the (Fourier) divergence constraint at a fixed `t,k`, then so does
1172the limit coefficient (by continuity + uniqueness of limits in `ℝ`). -/
1173theorem divConstraint_eq_zero_of_forall {H : UniformBoundsHypothesis} (HC : ConvergenceHypothesis H)
1174    (t : ℝ) (k : Mode2)