Theorem: DifferentiableOn.iterate_dslope (RMT4/cindex.lean)

State before:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
p : FormalMultilinearSeries ℂ ℂ E
U : Set ℂ
z₀ c : ℂ
n : ℕ
hf : DifferentiableOn ℂ f U
hU : IsOpen U
hc : c ∈ U
⊢ DifferentiableOn ℂ ((swap dslope c)^[n] f) U
Tactic:
induction n generalizing f
State after:
case zero
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
p : FormalMultilinearSeries ℂ ℂ E
U : Set ℂ
z₀ c : ℂ
hU : IsOpen U
hc : c ∈ U
f : ℂ → E
hf : DifferentiableOn ℂ f U
⊢ DifferentiableOn ℂ ((swap dslope c)^[zero] f) U

case succ
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
p : FormalMultilinearSeries ℂ ℂ E
U : Set ℂ
z₀ c : ℂ
hU : IsOpen U
hc : c ∈ U
n✝ : ℕ
n_ih✝ : ∀ {f : ℂ → E}, DifferentiableOn ℂ f U → DifferentiableOn ℂ ((swap dslope c)^[n✝] f) U
f : ℂ → E
hf : DifferentiableOn ℂ f U
⊢ DifferentiableOn ℂ ((swap dslope c)^[succ n✝] f) U

State before:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
p : FormalMultilinearSeries ℂ ℂ E
U : Set ℂ
z₀ c : ℂ
hU : IsOpen U
hc : c ∈ U
f : ℂ → E
hf : DifferentiableOn ℂ f U
⊢ DifferentiableOn ℂ ((swap dslope c)^[zero] f) U
Tactic:
case zero => exact hf
State after:
no goals

State before:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
p : FormalMultilinearSeries ℂ ℂ E
U : Set ℂ
z₀ c : ℂ
hU : IsOpen U
hc : c ∈ U
n✝ : ℕ
n_ih : ∀ {f : ℂ → E}, DifferentiableOn ℂ f U → DifferentiableOn ℂ ((swap dslope c)^[n✝] f) U
f : ℂ → E
hf : DifferentiableOn ℂ f U
⊢ DifferentiableOn ℂ ((swap dslope c)^[succ n✝] f) U
Tactic:
case succ n_ih => exact n_ih ((differentiableOn_dslope (hU.mem_nhds hc)).mpr hf)
State after:
no goals

State before:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
p : FormalMultilinearSeries ℂ ℂ E
U : Set ℂ
z₀ c : ℂ
hU : IsOpen U
hc : c ∈ U
f : ℂ → E
hf : DifferentiableOn ℂ f U
⊢ DifferentiableOn ℂ ((swap dslope c)^[zero] f) U
Tactic:
exact hf
State after:
no goals

State before:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
p : FormalMultilinearSeries ℂ ℂ E
U : Set ℂ
z₀ c : ℂ
hU : IsOpen U
hc : c ∈ U
n✝ : ℕ
n_ih : ∀ {f : ℂ → E}, DifferentiableOn ℂ f U → DifferentiableOn ℂ ((swap dslope c)^[n✝] f) U
f : ℂ → E
hf : DifferentiableOn ℂ f U
⊢ DifferentiableOn ℂ ((swap dslope c)^[succ n✝] f) U
Tactic:
exact n_ih ((differentiableOn_dslope (hU.mem_nhds hc)).mpr hf)
State after:
no goals