Theorem: SciLean.Rand.harmonicRec'_CDifferentiable (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 : ℕ
⊢ CDifferentiable Float fun w => harmonicRec' n w.1 w.2.1 w.2.2
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
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
Tactic:
simp[harmonicRec']
State after:
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')

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