simp[harmonicRec']
case succ
Y : Type
inst✝³ : SemiHilbert Float Y
inst✝² : Module ℝ Y
inst✝¹ : IsScalarTower ℝ Float Y
inst✝ : MeasurableSpace Y
n✝ : ℕ
n_ih✝ : CDifferentiable Float fun w => harmonicRec' n✝ w.1 w.2.1 w.2.2
⊢ CDifferentiable Float fun w => harmonicRec' (Nat.succ n✝) w.1 w.2.1 w.2.2
case succ
Y : Type
inst✝³ : SemiHilbert Float Y
inst✝² : Module ℝ Y
inst✝¹ : IsScalarTower ℝ Float Y
inst✝ : MeasurableSpace Y
n✝ : ℕ
n_ih✝ : CDifferentiable Float fun w => harmonicRec' n✝ w.1 w.2.1 w.2.2
⊢ CDifferentiable Float fun w => (pi'⁻¹ * 4⁻¹) • ∫' x', harmonicRec' n✝ w.1 w.2.1 (w.2.2 + w.1 w.2.2 • ↑x')