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

ContinuousCombinerSecondDerivativeInput

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)

 544def ContinuousCombinerSecondDerivativeInput
 545    (C : ComparisonOperator)
 546    (_h : SatisfiesLawsOfLogicContinuous C)
 547    (_hSmooth : ContDiff ℝ ((⊤ : ℕ∞) : WithTop ℕ∞)
 548      (fun t : ℝ => derivedCost C (Real.exp t))) : Prop :=

proof body

Definition body.

 549    AczelSecondDerivativeIdentity (fun t : ℝ => derivedCost C (Real.exp t))
 550
 551/-- **Named analysis input 2b: ψ-affine completion.**
 552
 553This is the remaining Stetkær/Aczél content: the derivative identity, symmetry
 554of the combiner, and the Aczél equation force the actual log-bilinear identity.
 555It is narrower than the former all-in ψ-affine forcing axiom because the
 556second-derivative extraction is now named separately. -/

used by (2)

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

depends on (20)

Lean names referenced from this declaration's body.