22 lines
486 B
Lean4
22 lines
486 B
Lean4
|
import Sunbeam.Model.Basic
|
||
|
|
|
||
|
|
namespace Sunbeam
|
||
|
|
|
||
|
|
/-- ReLU activation: max(0, x). -/
|
||
|
|
def relu (x : Float) : Float :=
|
||
|
|
if x > 0.0 then x else 0.0
|
||
|
|
|
||
|
|
/-- Pointwise ReLU on a vector. -/
|
||
|
|
def reluVec {n : Nat} (v : FloatVec n) : FloatVec n :=
|
||
|
|
fun i => relu (v i)
|
||
|
|
|
||
|
|
/-! ## Trust boundary: ReLU axioms -/
|
||
|
|
|
||
|
|
/-- ReLU output is non-negative. -/
|
||
|
|
axiom relu_nonneg (x : Float) : relu x ≥ 0.0
|
||
|
|
|
||
|
|
/-- ReLU is monotone. -/
|
||
|
|
axiom relu_monotone {x y : Float} (h : x ≤ y) : relu x ≤ relu y
|
||
|
|
|
||
|
|
end Sunbeam
|