Minimum and maximum

The captured minimum and maximum operations use the same comparison masks as their two-input runtime counterparts. A strict winner receives the full upstream gradient, a strict loser receives zero, and each input receives half at a tie. Capturing the right-hand tensor leaves that selection unchanged.

We first identify the stored backward functions coordinate by coordinate, including their value at ties. We then prove that these functions are the adjoints of the forward derivatives wherever every input coordinate differs from its captured partner. The equality case has a selected backward rule, but no classical derivative is claimed there.

theorem Proofs.Autograd.PrimitiveSpecs.hasDerivAt_min_const_of_ne {x c : ℝ} (h : x ≠ c) : HasDerivAt (fun (y : ℝ) => min y c) (if x < c then 1 else if c < x then 0 else 1 / 2) x

With unequal arguments, minimum agrees locally with either the input or the constant.

theorem Proofs.Autograd.PrimitiveSpecs.hasDerivAt_max_const_of_ne {x c : ℝ} (h : x ≠ c) : HasDerivAt (fun (y : ℝ) => max y c) (if c < x then 1 else if x < c then 0 else 1 / 2) x

With unequal arguments, maximum has derivative one at a strict winner and zero otherwise.

theorem Proofs.Autograd.PrimitiveSpecs.minOp_backward_apply {s : Spec.Shape} (rhs x δ : TorchLean.Tensor ℝ s) (i : Fin s.size) : (tensorToVec ((Spec.minOp rhs).backward x δ)).ofLp i = (if (tensorToVec x).ofLp i < (tensorToVec rhs).ofLp i then 1 else if (tensorToVec rhs).ofLp i < (tensorToVec x).ofLp i then 0 else 1 / 2) * (tensorToVec δ).ofLp i

The actual minimum backward multiplies by its selected comparison mask at each coordinate.

theorem Proofs.Autograd.PrimitiveSpecs.maxOp_backward_apply {s : Spec.Shape} (rhs x δ : TorchLean.Tensor ℝ s) (i : Fin s.size) : (tensorToVec ((Spec.maxOp rhs).backward x δ)).ofLp i = (if (tensorToVec rhs).ofLp i < (tensorToVec x).ofLp i then 1 else if (tensorToVec x).ofLp i < (tensorToVec rhs).ofLp i then 0 else 1 / 2) * (tensorToVec δ).ofLp i

The actual maximum backward keeps the same comparison order as the runtime selection.

theorem Proofs.Autograd.PrimitiveSpecs.minOp_backward_apply_of_eq {s : Spec.Shape} (rhs x δ : TorchLean.Tensor ℝ s) (i : Fin s.size) (h : (tensorToVec x).ofLp i = (tensorToVec rhs).ofLp i) : (tensorToVec ((Spec.minOp rhs).backward x δ)).ofLp i = 1 / 2 * (tensorToVec δ).ofLp i

A minimum tie retains half the upstream gradient even when the other input is captured.

theorem Proofs.Autograd.PrimitiveSpecs.maxOp_backward_apply_of_eq {s : Spec.Shape} (rhs x δ : TorchLean.Tensor ℝ s) (i : Fin s.size) (h : (tensorToVec x).ofLp i = (tensorToVec rhs).ofLp i) : (tensorToVec ((Spec.maxOp rhs).backward x δ)).ofLp i = 1 / 2 * (tensorToVec δ).ofLp i

A maximum tie uses the same half-gradient selection as minimum.

theorem Proofs.Autograd.PrimitiveSpecs.minOp_hasFDerivAt {s : Spec.Shape} (rhs : TorchLean.Tensor ℝ s) (x : Vec s.size) (hneq : ∀ (i : Fin s.size), x.ofLp i ≠ (tensorToVec rhs).ofLp i) : HasFDerivAt (fun (y : Vec s.size) => tensorToVec ((Spec.minOp rhs).forward (vecToTensor y))) (coordinateDeriv fun (i : Fin s.size) => if x.ofLp i < (tensorToVec rhs).ofLp i then 1 else if (tensorToVec rhs).ofLp i < x.ofLp i then 0 else 1 / 2) x

Away from all coordinate ties, the minimum mask is the derivative of its tensor forward.

theorem Proofs.Autograd.PrimitiveSpecs.maxOp_hasFDerivAt {s : Spec.Shape} (rhs : TorchLean.Tensor ℝ s) (x : Vec s.size) (hneq : ∀ (i : Fin s.size), x.ofLp i ≠ (tensorToVec rhs).ofLp i) : HasFDerivAt (fun (y : Vec s.size) => tensorToVec ((Spec.maxOp rhs).forward (vecToTensor y))) (coordinateDeriv fun (i : Fin s.size) => if (tensorToVec rhs).ofLp i < x.ofLp i then 1 else if x.ofLp i < (tensorToVec rhs).ofLp i then 0 else 1 / 2) x

Away from all coordinate ties, the maximum mask is the derivative of its tensor forward.

theorem Proofs.Autograd.PrimitiveSpecs.minOp_backward_eq_adjoint {s : Spec.Shape} (rhs : TorchLean.Tensor ℝ s) (x : Vec s.size) (hneq : ∀ (i : Fin s.size), x.ofLp i ≠ (tensorToVec rhs).ofLp i) (δ : TorchLean.Tensor ℝ s) : tensorToVec ((Spec.minOp rhs).backward (vecToTensor x) δ) = (ContinuousLinearMap.adjoint (fderiv ℝ (fun (y : Vec s.size) => tensorToVec ((Spec.minOp rhs).forward (vecToTensor y))) x)) (tensorToVec δ)

The stored minimum backward is the adjoint of the forward derivative away from ties.

theorem Proofs.Autograd.PrimitiveSpecs.maxOp_backward_eq_adjoint {s : Spec.Shape} (rhs : TorchLean.Tensor ℝ s) (x : Vec s.size) (hneq : ∀ (i : Fin s.size), x.ofLp i ≠ (tensorToVec rhs).ofLp i) (δ : TorchLean.Tensor ℝ s) : tensorToVec ((Spec.maxOp rhs).backward (vecToTensor x) δ) = (ContinuousLinearMap.adjoint (fderiv ℝ (fun (y : Vec s.size) => tensorToVec ((Spec.maxOp rhs).forward (vecToTensor y))) x)) (tensorToVec δ)

The stored maximum backward is the adjoint of the forward derivative away from ties.