Piecewise tape nodes

Piecewise smooth min/max nodes and pointwise differentiability facts under strict branch-selection hypotheses.

noncomputable def Proofs.Autograd.TapeNodes.maxElem {Γ : List Spec.Shape} {s : Spec.Shape} (a b : Idx Γ s) : Node Γ s

Elementwise max node. Differentiable at points where a ≠ b coordinatewise.

noncomputable def Proofs.Autograd.TapeNodes.minElem {Γ : List Spec.Shape} {s : Spec.Shape} (a b : Idx Γ s) : Node Γ s

Elementwise min node. Differentiable at points where a ≠ b coordinatewise.

theorem Proofs.Autograd.TapeNodes.hasFDerivAt_max_of_lt {Γ : List Spec.Shape} {f g : CtxVec Γ → ℝ} {f' g' : CtxVec Γ →L[ℝ] ℝ} {xV : CtxVec Γ} (hf : HasFDerivAt f f' xV) (hg : HasFDerivAt g g' xV) (hfg : f xV > g xV) : HasFDerivAt (fun (x : CtxVec Γ) => max (f x) (g x)) f' xV

Derivative of max at points where the f branch strictly dominates (f xV > g xV).

theorem Proofs.Autograd.TapeNodes.hasFDerivAt_min_of_lt {Γ : List Spec.Shape} {f g : CtxVec Γ → ℝ} {f' g' : CtxVec Γ →L[ℝ] ℝ} {xV : CtxVec Γ} (hf : HasFDerivAt f f' xV) (hg : HasFDerivAt g g' xV) (hfg : f xV < g xV) : HasFDerivAt (fun (x : CtxVec Γ) => min (f x) (g x)) f' xV

Derivative of min at points where the f branch strictly dominates (f xV < g xV).

noncomputable def Proofs.Autograd.TapeNodes.maxElemFderivAt {Γ : List Spec.Shape} {s : Spec.Shape} (a b : Idx Γ s) (xV : CtxVec Γ) (hneq : ∀ (i : Fin s.size), (CtxVec.get a xV).ofLp i ≠ (CtxVec.get b xV).ofLp i) : NodeFDerivCorrectAt (maxElem a b) xV

Pointwise NodeFDerivCorrectAt for max_elem, assuming there are no ties.

noncomputable def Proofs.Autograd.TapeNodes.minElemFderivAt {Γ : List Spec.Shape} {s : Spec.Shape} (a b : Idx Γ s) (xV : CtxVec Γ) (hneq : ∀ (i : Fin s.size), (CtxVec.get a xV).ofLp i ≠ (CtxVec.get b xV).ofLp i) : NodeFDerivCorrectAt (minElem a b) xV

Pointwise NodeFDerivCorrectAt for min_elem, assuming there are no ties.