Theorem: SciLean.Rand.harmonicRec.arg_x.CDifferentiable_rule (SciLean/Core/Rand/Distributions/WalkOnSpheres.lean)

State before:
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
Tactic:
induction n <;> (simp[harmonicRec]; fun_prop)
State after:
no goals

State before:
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
Tactic:
simp[harmonicRec]
State after:
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')

State before:
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')
Tactic:
fun_prop
State after:
no goals