`ConvergenceHypothesis`

definition

show as: view math explainer →

module: IndisputableMonolith.ClassicalBridge.Fluids.ContinuumLimit2D
domain: ClassicalBridge
line: 1133 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.ClassicalBridge.Fluids.ContinuumLimit2D on GitHub at line 1133.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

used by

formal source

1130end GalerkinForcingDominatedConvergenceHypothesis
1131
1132/-- Hypothesis: existence of a limit Fourier trajectory and convergence from the approximants. -/
1133structure ConvergenceHypothesis (H : UniformBoundsHypothesis) where
1134  /-- Candidate limit (time → full Fourier coefficients). -/
1135  u : ℝ → FourierState2D
1136  /-- Pointwise (mode-by-mode) convergence of the zero-extended Galerkin coefficients. -/
1137  converges : ∀ t : ℝ, ∀ k : Mode2,
1138    Tendsto (fun N : ℕ => (extendByZero (H.uN N t)) k) atTop (𝓝 ((u t) k))
1139
1140namespace ConvergenceHypothesis
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 :=

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.