def
definition
boundaryTerm
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.NavierStokes.RM2U.Core on GitHub at line 50.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
47namespace RM2URadialProfile
48
49/-- The boundary term associated to a profile. -/
50noncomputable def boundaryTerm (P : RM2URadialProfile) : ℝ → ℝ :=
51 fun r => tailFlux P.A P.A' r
52
53/-- Convenience: `TailFluxVanish` for a profile. -/
54def tailFluxVanish (P : RM2URadialProfile) : Prop :=
55 TailFluxVanish P.A P.A'
56
57end RM2URadialProfile
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