`LogCriticalMomentFinite`

definition

show as: view math explainer →

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

open explainer

Read the cached plain-language explainer.

open lean source

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

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

used by

formal source

  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.