rs_implies_global_regularity_2d_coeffBound

formal source

  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
  61    (Hbounds : UniformBoundsHypothesis)
  62    (Hconv : ConvergenceHypothesis Hbounds) :
  63    ∃ u : ℝ → FourierState2D,
  64      (∀ t : ℝ, ∀ k : Mode2,
  65        Filter.Tendsto (fun N : ℕ => (extendByZero (Hbounds.uN N t)) k) Filter.atTop
  66          (nhds ((u t) k)))
  67        ∧ (∀ t ≥ 0, ∀ k : Mode2, ‖(u t) k‖ ≤ Hbounds.B) := by
  68  -- Take the limit object from convergence, and use the derived bound lemma.
  69  refine ⟨Hconv.u, ?_, ?_⟩
  70  · simpa using Hconv.converges
  71  · intro t ht k
  72    simpa using (ConvergenceHypothesis.coeff_bound_of_uniformBounds (HC := Hconv) t ht k)
  73
  74/-- Variant of the top-level theorem where the derived “identification” is:
  75
  76- the **proved** coefficient bound (from uniform bounds + convergence), and
  77- the **proved** divergence-free constraint (passed to the limit under modewise convergence),
  78  assuming each approximant is divergence-free in Fourier variables.
  79
  80This avoids providing a separate `IdentificationHypothesis`. -/
  81theorem rs_implies_global_regularity_2d_divFreeCoeffBound
  82    (Hbounds : UniformBoundsHypothesis)
  83    (Hconv : ConvergenceHypothesis Hbounds)
  84    (hDF : ∀ N : ℕ, ∀ t : ℝ, ∀ k : Mode2,
  85      divConstraint k ((extendByZero (Hbounds.uN N t)) k) = 0) :
  86    ∃ u : ℝ → FourierState2D,
  87      (∀ t : ℝ, ∀ k : Mode2,
  88        Filter.Tendsto (fun N : ℕ => (extendByZero (Hbounds.uN N t)) k) Filter.atTop
  89          (nhds ((u t) k)))
  90        ∧ (∀ t ≥ 0, ∀ k : Mode2, ‖(u t) k‖ ≤ Hbounds.B)