TorchLean API

Docs HomeInstallationGuideExamplesGraphsTools

NN.MLTheory.CROWN.Extras.IntervalLemmas

Interval arithmetic lemmas #

Scalar facts shared by the CROWN soundness proofs: monotonicity of the real sigmoid and tanh, the real reading of BoundOps.min2/BoundOps.max2, the enclosure law for the four-corner product Graph.intervalMul, and the exact real instance of LawfulNonlinearBoundOps.

Monotone nonlinear functions #

source
noncomputable def NN.MLTheory.CROWN.IntervalLemmas.realSigmoid (x : ℝ) :
ℝ

The real sigmoid written in the form used by NonlinearBoundOps.

Instances For
    source
    theorem NN.MLTheory.CROWN.IntervalLemmas.monotone_realSigmoid :
    Monotone realSigmoid

    The real sigmoid is monotone.

    source
    theorem NN.MLTheory.CROWN.IntervalLemmas.hasDerivAt_real_tanh (x : ℝ) :
    HasDerivAt Real.tanh (1 / Real.cosh x ^ 2) x

    Derivative of real hyperbolic tangent.

    source
    theorem NN.MLTheory.CROWN.IntervalLemmas.strictMono_real_tanh :
    StrictMono Real.tanh

    The real hyperbolic tangent is strictly monotone.

    source
    theorem NN.MLTheory.CROWN.IntervalLemmas.monotone_real_tanh :
    Monotone Real.tanh

    The real hyperbolic tangent is monotone.

    Directed endpoint arithmetic #

    source
    theorem NN.MLTheory.CROWN.IntervalLemmas.value_min2 {α : Type} [TorchLean.Storage α] [Context α] [BoundOps α] [LawfulBoundOps α] (a b : α) :
    LawfulBoundOps.toReal (BoundOps.min2 a b) = min (LawfulBoundOps.toReal a) (LawfulBoundOps.toReal b)

    BoundOps.min2 selects the smaller endpoint in the mathematical interpretation.

    source
    theorem NN.MLTheory.CROWN.IntervalLemmas.value_max2 {α : Type} [TorchLean.Storage α] [Context α] [BoundOps α] [LawfulBoundOps α] (a b : α) :
    LawfulBoundOps.toReal (BoundOps.max2 a b) = max (LawfulBoundOps.toReal a) (LawfulBoundOps.toReal b)

    BoundOps.max2 selects the larger endpoint in the mathematical interpretation.

    source
    theorem NN.MLTheory.CROWN.IntervalLemmas.intervalMul_encloses {α : Type} [TorchLean.Storage α] [Context α] [BoundOps α] [LawfulBoundOps α] {al au bl bu : α} {x y : ℝ} (hal : LawfulBoundOps.toReal al ≤ x) (hau : x ≤ LawfulBoundOps.toReal au) (hbl : LawfulBoundOps.toReal bl ≤ y) (hbu : y ≤ LawfulBoundOps.toReal bu) :
    LawfulBoundOps.toReal (Graph.intervalMul al au bl bu).1 ≤ x * y ∧ x * y ≤ LawfulBoundOps.toReal (Graph.intervalMul al au bl bu).2

    The outward-rounded four-corner product Graph.intervalMul encloses every product of enclosed reals.

    It depends only on the endpoint interpretation and the directed-operation laws; it does not assume that rounded scalars form a ring or that reassociation is exact. The real four-corner bound is FloatLib's mul_bounds_Icc.

    Nonlinear transfer laws over the reals #

    source
    instance NN.MLTheory.CROWN.IntervalLemmas.instLawfulNonlinearBoundOpsReal :
    LawfulNonlinearBoundOps ℝ

    Exact real nonlinear transfers satisfy their mathematical interval contracts.