`CoerciveL2Bound`

definition

show as: view math explainer →

module: IndisputableMonolith.NavierStokes.RM2U.Core
domain: NavierStokes
line: 61 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.NavierStokes.RM2U.Core on GitHub at line 61.

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

  58
  59/-- A concrete analytic target implied by UEWE and used to close RM2U in the manuscript:
  60integrability of the \(\ell=2\) coefficient and its derivative with the `r^2` weight. -/
  61def CoerciveL2Bound (P : RM2URadialProfile) : Prop :=
  62  IntegrableOn (fun r : ℝ => (P.A r) ^ 2) (Set.Ioi (1 : ℝ)) volume
  63    ∧ IntegrableOn (fun r : ℝ => (P.A' r) ^ 2 * (r ^ 2)) (Set.Ioi (1 : ℝ)) volume
  64
  65/-- The log-critical shell moment integrability (the RM2 obstruction in the manuscript):
  66`A(r)/r ∈ L¹((1,∞), dr)`. -/
  67def LogCriticalMomentFinite (A : ℝ → ℝ) : Prop :=
  68  IntegrableOn (fun r : ℝ => A r / r) (Set.Ioi (1 : ℝ)) volume
  69
  70end RM2U
  71end NavierStokes
  72end IndisputableMonolith

papers checked against this theorem

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