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

rs_implies_global_regularity_2d_divFreeCoeffBound

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

  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)
  91        ∧ IsDivergenceFreeTraj u := by

proof body

Term-mode proof.

  92  refine ⟨Hconv.u, ?_, ?_, ?_⟩
  93  · simpa using Hconv.converges
  94  · intro t ht k
  95    simpa using (ConvergenceHypothesis.coeff_bound_of_uniformBounds (HC := Hconv) t ht k)
  96  · exact ConvergenceHypothesis.divFree_of_forall (HC := Hconv) hDF
  97
  98/-- Variant of the top-level theorem where the derived “identification” is:
  99
 100- the **proved** coefficient bound (from uniform bounds + convergence), and
 101- the **proved** linear Stokes/heat mild identity (passed to the limit under modewise convergence),
 102  assuming each approximant satisfies the same identity modewise for `t ≥ 0`.
 103
 104This avoids providing a separate `IdentificationHypothesis`. -/

depends on (25)

Lean names referenced from this declaration's body.