pith. machine review for the scientific record. sign in
def definition def or abbrev

OperatorPairingIntegrable

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)

 193def OperatorPairingIntegrable (P : RM2URadialProfile) : Prop :=

proof body

Definition body.

 194  IntegrableOn (fun x : ℝ => (rm2uOp P x) * (P.A x) * (x ^ 2))
 195    (Set.Ioi (1 : ℝ)) volume
 196
 197/-- `AncientEnergyDecayFull` implies `OperatorPairingIntegrable`:
 198    `rm2uOp·A·r² = -A''Ar² - 2A'Ar + 6A²`, where each term decays
 199    like `C²r^{-3}`, integrable since `-3 < -1`. -/

used by (6)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (7)

Lean names referenced from this declaration's body.