induction n <;> (simp[harmonicRec]; fun_prop)
Y : Type
inst✝³ : SemiHilbert Float Y
inst✝² : Module ℝ Y
inst✝¹ : IsScalarTower ℝ Float Y
inst✝ : MeasurableSpace Y
n : ℕ
φ : Vec3 → Float
g : Vec3 → Y
hφ : CDifferentiable Float φ
hg : CDifferentiable Float g
⊢ CDifferentiable Float fun x => harmonicRec n φ g x
no goals