Scalar alpha-ReLU Lower Bounds

Soundness of the scalar lower relaxation used by alpha-CROWN. Keeping this elementary fact in one module lets graph transfer proofs and alpha/beta phase proofs share the same argument.

theorem NN.MLTheory.CROWN.Proofs.scaledInput_le_relu (alpha input : ℝ) (alphaNonnegative : 0 ≤ alpha) (alphaAtMostOne : alpha ≤ 1) : alpha * input ≤ Activation.Math.reluSpec input

Scaling an input by a coefficient in [0, 1] never exceeds its ReLU.

theorem NN.MLTheory.CROWN.Proofs.alphaRelaxLowerScalar_sound (lower upper alpha input : ℝ) (lowerBound : lower ≤ input) (upperBound : input ≤ upper) (alphaNonnegative : 0 ≤ alpha) (alphaAtMostOne : alpha ≤ 1) : have relaxation := Cert.alphaRelaxLowerScalar lower upper alpha; relaxation.slope * input + relaxation.bias ≤ Activation.Math.reluSpec input

The alpha-CROWN scalar lower relaxation under-approximates ReLU throughout [lower, upper].