RSNS2DPipelineHypothesis

formal source

  27## Master hypothesis: all ingredients of the 2D pipeline
  28-/
  29
  30structure RSNS2DPipelineHypothesis where
  31  /-- Uniform-in-`N` bounds for the Galerkin family. -/
  32  Hbounds : UniformBoundsHypothesis
  33  /-- Convergence to a limit Fourier trajectory. -/
  34  Hconv : ConvergenceHypothesis Hbounds
  35  /-- Identification: the limit satisfies a chosen solution concept. -/
  36  Hid : IdentificationHypothesis Hconv
  37
  38/-!
  39## Top-level theorem (2D)
  40-/
  41
  42/-- RS → (abstract) global regularity in 2D, via the composed bridge pipeline.
  43
  44At this stage, “regularity” is represented by the existence of a limit Fourier trajectory
  45`u : ℝ → FourierState2D` together with the packaged identification property.
  46-/
  47theorem rs_implies_global_regularity_2d
  48    (H : RSNS2DPipelineHypothesis) :
  49    ∃ u : ℝ → FourierState2D,
  50      (∀ t : ℝ, ∀ k : Mode2,
  51        Filter.Tendsto (fun N : ℕ => (extendByZero (H.Hbounds.uN N t)) k) Filter.atTop
  52          (nhds ((u t) k)))
  53        ∧ H.Hid.IsSolution u
  54        ∧ (∀ t ≥ 0, ∀ k : Mode2, ‖(u t) k‖ ≤ H.Hbounds.B) := by
  55  -- The result is exactly the continuum limit theorem from M5.
  56  simpa using (continuum_limit_exists H.Hbounds H.Hconv H.Hid)
  57
  58/-- Variant of the top-level theorem where the “identification” is the **proved** coefficient bound:
  59we do not need a separate `IdentificationHypothesis` argument for this minimal `IsSolution` notion. -/
  60theorem rs_implies_global_regularity_2d_coeffBound