induction n <;> (simp[harmonicRec']; fun_prop)
Y : Type
inst✝³ : SemiHilbert Float Y
inst✝² : Module ℝ Y
inst✝¹ : IsScalarTower ℝ Float Y
inst✝ : MeasurableSpace Y
n : ℕ
⊢ CDifferentiable Float fun w => harmonicRec' n w.1 w.2.1 w.2.2
no goals