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