pith. machine review for the scientific record. sign in
theorem proved tactic proof high

coeff_bound_of_uniformBounds

show as:
view Lean formalization →

If Galerkin approximants satisfy a uniform bound B in the discrete norm for all truncation levels N and times t ≥ 0, then the modewise limits of their zero-extended coefficients satisfy the same bound. Researchers constructing continuum limits from Galerkin approximations in 2D fluids would cite this result to establish the identification hypothesis. The argument proceeds by showing each approximant coefficient lies in the closed ball of radius B, passing to the limit via closedness of that ball under the given pointwise convergence.

claimLet $H$ be a uniform bounds hypothesis for a family of Galerkin trajectories $u_N$ with bound $B$, and let $HC$ be a convergence hypothesis from those approximants to a limit trajectory $u$. Then for all $t ≥ 0$ and all modes $k$, $‖(u(t))_k‖ ≤ B$.

background

In the ContinuumLimit2D module the pipeline from finite Galerkin approximations to a continuum Fourier state is formalized by packaging analytic steps as explicit hypotheses. UniformBoundsHypothesis packages a family of Galerkin trajectories uN together with a uniform bound B such that for all N and t ≥ 0 the discrete norm satisfies ‖uN N t‖ ≤ B; this would arise in a full proof from energy estimates or compactness arguments. ConvergenceHypothesis assumes a candidate limit u : ℝ → FourierState2D together with modewise convergence of the zero-extended approximants: for each t and k, the sequence (extendByZero (H.uN N t)) k tends to (u t) k as N → ∞.

proof idea

The proof fixes t ≥ 0 and mode k, then shows that for every N the extended coefficient (extendByZero (H.uN N t)) k lies in the closed ball of radius B centered at zero. This follows from norm_extendByZero_le combined with the uniform bound H.bound N t ht. The set of points in the closed ball is closed, so the limit under the assumed convergence HC.converges t k must also lie in the ball. Extracting the distance from the membership statement yields the desired norm bound.

why it matters in Recognition Science

This theorem supplies the coefficient bound component of the IdentificationHypothesis used by coeffBound, divFreeCoeffBound, nsDuhamelCoeffBound and their variants; those constructors in turn feed the existence statement continuum_limit_exists. It therefore closes one concrete step in the M5 milestone pipeline that turns Galerkin approximants into a continuum limit object. Within the Recognition Science framework the result sits inside the ClassicalBridge layer that bridges discrete algebraic structures to continuum fluid models.

scope and limits

Lean usage

example {H : UniformBoundsHypothesis} (HC : ConvergenceHypothesis H) (t : ℝ) (ht : t ≥ 0) (k : Mode2) : ‖(HC.u t) k‖ ≤ H.B := coeff_bound_of_uniformBounds HC t ht k

formal statement (Lean)

1144theorem coeff_bound_of_uniformBounds {H : UniformBoundsHypothesis} (HC : ConvergenceHypothesis H) :
1145    ∀ t ≥ 0, ∀ k : Mode2, ‖(HC.u t) k‖ ≤ H.B := by

proof body

Tactic-mode proof.

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 `ℝ`). -/

used by (15)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (22)

Lean names referenced from this declaration's body.