feat(*): prove some *.iterate theorems (#2647)

src/analysis/calculus/deriv.lean

@@ -954,6 +954,38 @@ begin
   exact has_deriv_at.comp x hh₁.has_deriv_at hh₂.has_deriv_at
 end
 
+protected lemma has_deriv_at_filter.iterate {f : 𝕜 → 𝕜} {f' : 𝕜}
+  (hf : has_deriv_at_filter f f' x L) (hL : tendsto f L L) (hx : f x = x) (n : ℕ) :
+  has_deriv_at_filter (f^[n]) (f'^n) x L :=
+begin
+  have := hf.iterate hL hx n,
+  rwa [continuous_linear_map.smul_right_one_pow] at this
+end
+
+protected lemma has_deriv_at.iterate {f : 𝕜 → 𝕜} {f' : 𝕜}
+  (hf : has_deriv_at f f' x) (hx : f x = x) (n : ℕ) :
+  has_deriv_at (f^[n]) (f'^n) x :=
+begin
+  have := has_fderiv_at.iterate hf hx n,
+  rwa [continuous_linear_map.smul_right_one_pow] at this
+end
+
+protected lemma has_deriv_within_at.iterate {f : 𝕜 → 𝕜} {f' : 𝕜}
+  (hf : has_deriv_within_at f f' s x) (hx : f x = x) (hs : maps_to f s s) (n : ℕ) :
+  has_deriv_within_at (f^[n]) (f'^n) s x :=
+begin
+  have := has_fderiv_within_at.iterate hf hx hs n,
+  rwa [continuous_linear_map.smul_right_one_pow] at this
+end
+
+protected lemma has_strict_deriv_at.iterate {f : 𝕜 → 𝕜} {f' : 𝕜}
+  (hf : has_strict_deriv_at f f' x) (hx : f x = x) (n : ℕ) :
+  has_strict_deriv_at (f^[n]) (f'^n) x :=
+begin
+  have := hf.iterate hx n,
+  rwa [continuous_linear_map.smul_right_one_pow] at this
+end
+
 end composition
 
 section composition_vector

src/analysis/calculus/fderiv.lean

@@ -998,6 +998,70 @@ protected lemma has_strict_fderiv_at.comp {g : F → G} {g' : F →L[𝕜] G}
 ((hg.comp_tendsto (hf.continuous_at.prod_map' hf.continuous_at)).trans_is_O hf.is_O_sub).triangle $
   by simpa only [g'.map_sub, f'.coe_comp'] using (g'.is_O_comp _ _).trans_is_o hf
 
+protected lemma differentiable.iterate {f : E → E} (hf : differentiable 𝕜 f) (n : ℕ) :
+  differentiable 𝕜 (f^[n]) :=
+nat.rec_on n differentiable_id (λ n ihn, ihn.comp hf)
+
+protected lemma differentiable_on.iterate {f : E → E} (hf : differentiable_on 𝕜 f s)
+  (hs : maps_to f s s) (n : ℕ) :
+  differentiable_on 𝕜 (f^[n]) s :=
+nat.rec_on n differentiable_on_id (λ n ihn, ihn.comp hf hs)
+
+variable {x}
+
+protected lemma has_fderiv_at_filter.iterate {f : E → E} {f' : E →L[𝕜] E}
+  (hf : has_fderiv_at_filter f f' x L) (hL : tendsto f L L) (hx : f x = x) (n : ℕ) :
+  has_fderiv_at_filter (f^[n]) (f'^n) x L :=
+begin
+  induction n with n ihn,
+  { exact has_fderiv_at_filter_id x L },
+  { change has_fderiv_at_filter (f^[n] ∘ f) (f'^(n+1)) x L,
+    rw [pow_succ'],
+    refine has_fderiv_at_filter.comp x _ hf,
+    rw hx,
+    exact ihn.mono hL }
+end
+
+protected lemma has_fderiv_at.iterate {f : E → E} {f' : E →L[𝕜] E}
+  (hf : has_fderiv_at f f' x) (hx : f x = x) (n : ℕ) :
+  has_fderiv_at (f^[n]) (f'^n) x :=
+begin
+  refine hf.iterate _ hx n,
+  convert hf.continuous_at,
+  exact hx.symm
+end
+
+protected lemma has_fderiv_within_at.iterate {f : E → E} {f' : E →L[𝕜] E}
+  (hf : has_fderiv_within_at f f' s x) (hx : f x = x) (hs : maps_to f s s) (n : ℕ) :
+  has_fderiv_within_at (f^[n]) (f'^n) s x :=
+begin
+  refine hf.iterate _ hx n,
+  convert tendsto_inf.2 ⟨hf.continuous_within_at, _⟩,
+  exacts [hx.symm, tendsto_le_left inf_le_right (tendsto_principal_principal.2 hs)]
+end
+
+protected lemma has_strict_fderiv_at.iterate {f : E → E} {f' : E →L[𝕜] E}
+  (hf : has_strict_fderiv_at f f' x) (hx : f x = x) (n : ℕ) :
+  has_strict_fderiv_at (f^[n]) (f'^n) x :=
+begin
+  induction n with n ihn,
+  { exact has_strict_fderiv_at_id x },
+  { change has_strict_fderiv_at (f^[n] ∘ f) (f'^(n+1)) x,
+    rw [pow_succ'],
+    refine has_strict_fderiv_at.comp x _ hf,
+    rwa hx }
+end
+
+protected lemma differentiable_at.iterate {f : E → E} (hf : differentiable_at 𝕜 f x)
+  (hx : f x = x) (n : ℕ) :
+  differentiable_at 𝕜 (f^[n]) x :=
+exists.elim hf $ λ f' hf, (hf.iterate hx n).differentiable_at
+
+protected lemma differentiable_within_at.iterate {f : E → E} (hf : differentiable_within_at 𝕜 f s x)
+  (hx : f x = x) (hs : maps_to f s s) (n : ℕ) :
+  differentiable_within_at 𝕜 (f^[n]) s x :=
+exists.elim hf $ λ f' hf, (hf.iterate hx hs n).differentiable_within_at
+
 end composition
 
 section cartesian_product

src/order/basic.lean

@@ -160,6 +160,9 @@ protected theorem monotone.comp {g : β → γ} {f : α → β} (m_g : monotone
   monotone (g ∘ f) :=
 assume a b h, m_g (m_f h)
 
+protected theorem monotone.iterate {f : α → α} (hf : monotone f) (n : ℕ) : monotone (f^[n]) :=
+nat.rec_on n monotone_id (λ n ihn, ihn.comp hf)
+
 lemma monotone_of_monotone_nat {f : ℕ → α} (hf : ∀n, f n ≤ f (n + 1)) :
   monotone f | n m h :=
 begin
@@ -178,6 +181,8 @@ end monotone
 def strict_mono [has_lt α] [has_lt β] (f : α → β) : Prop :=
 ∀ ⦃a b⦄, a < b → f a < f b
 
+lemma strict_mono_id [has_lt α] : strict_mono (id : α → α) := λ a b, id
+
 namespace strict_mono
 open ordering function
 
@@ -186,6 +191,10 @@ lemma comp [has_lt α] [has_lt β] [has_lt γ] {g : β → γ} {f : α → β}
   strict_mono (g ∘ f) :=
 λ a b h, hg (hf h)
 
+protected theorem iterate [has_lt α] {f : α → α} (hf : strict_mono f) (n : ℕ) :
+  strict_mono (f^[n]) :=
+nat.rec_on n strict_mono_id (λ n ihn, ihn.comp hf)
+
 section
 variables [linear_order α] [preorder β] {f : α → β}
 

src/topology/algebra/module.lean

@@ -315,7 +315,11 @@ rfl
 
 instance : has_mul (M →L[R] M) := ⟨comp⟩
 
-@[simp] lemma mul_apply (f g : M →L[R] M) (x : M) : (f * g) x = f (g x) := rfl
+lemma mul_def (f g : M →L[R] M) : f * g = f.comp g := rfl
+
+@[simp] lemma coe_mul (f g : M →L[R] M) : ⇑(f * g) = f ∘ g := rfl
+
+lemma mul_apply (f g : M →L[R] M) (x : M) : (f * g) x = f (g x) := rfl
 
 instance [topological_add_group M] : ring (M →L[R] M) :=
 { mul := (*),
@@ -481,6 +485,14 @@ lemma smul_right_comp [topological_module R R] {x : M₂} {c : R} :
   (smul_right 1 x : R →L[R] M₂).comp (smul_right 1 c : R →L[R] R) = smul_right 1 (c • x) :=
 by { ext, simp [mul_smul] }
 
+lemma smul_right_one_pow [topological_add_group R] [topological_module R R] (c : R) (n : ℕ) :
+  (smul_right 1 c : R →L[R] R)^n = smul_right 1 (c^n) :=
+begin
+  induction n with n ihn,
+  { ext, simp },
+  { rw [pow_succ, ihn, mul_def, smul_right_comp, smul_eq_mul, pow_succ'] }
+end
+
 end general_ring
 
 section comm_ring

src/topology/basic.lean

@@ -674,6 +674,9 @@ lemma continuous.comp {g : β → γ} {f : α → β} (hg : continuous g) (hf :
   continuous (g ∘ f) :=
 assume s h, hf _ (hg s h)
 
+lemma continuous.iterate {f : α → α} (h : continuous f) (n : ℕ) : continuous (f^[n]) :=
+nat.rec_on n continuous_id (λ n ihn, ihn.comp h)
+
 lemma continuous_at.comp {g : β → γ} {f : α → β} {x : α}
   (hg : continuous_at g (f x)) (hf : continuous_at f x) :
   continuous_at (g ∘ f) x :=
@@ -706,6 +709,12 @@ continuous_const.continuous_at
 lemma continuous_at_id {x : α} : continuous_at id x :=
 continuous_id.continuous_at
 
+lemma continuous_at.iterate {f : α → α} {x : α} (hf : continuous_at f x) (hx : f x = x) (n : ℕ) :
+  continuous_at (f^[n]) x :=
+nat.rec_on n continuous_at_id $ λ n ihn,
+show continuous_at (f^[n] ∘ f) x,
+from continuous_at.comp (hx.symm ▸ ihn) hf
+
 lemma continuous_iff_is_closed {f : α → β} :
   continuous f ↔ (∀s, is_closed s → is_closed (f ⁻¹' s)) :=
 ⟨assume hf s hs, hf (-s) hs,