feat(analysis/calculus): derivatives of f : E → Π i, F i (#6075)

src/analysis/asymptotics/asymptotics.lean

@@ -43,7 +43,7 @@ the Fréchet derivative.)
 -/
 
 open filter set
-open_locale topological_space big_operators classical filter
+open_locale topological_space big_operators classical filter nnreal
 
 namespace asymptotics
 
@@ -160,6 +160,15 @@ theorem is_O.exists_nonneg (h : is_O f g' l) :
   ∃ c (H : 0 ≤ c), is_O_with c f g' l :=
 let ⟨c, hc⟩ := h.is_O_with in hc.exists_nonneg
 
+/-- `f = O(g)` if and only if `is_O_with c f g` for all sufficiently large `c`. -/
+lemma is_O_iff_eventually_is_O_with : is_O f g' l ↔ ∀ᶠ c in at_top, is_O_with c f g' l :=
+is_O_iff_is_O_with.trans
+  ⟨λ ⟨c, hc⟩, mem_at_top_sets.2 ⟨c, λ c' hc', hc.weaken hc'⟩, λ h, h.exists⟩
+
+/-- `f = O(g)` if and only if `∀ᶠ x in l, ∥f x∥ ≤ c * ∥g x∥` for all sufficiently large `c`. -/
+lemma is_O_iff_eventually : is_O f g' l ↔ ∀ᶠ c in at_top, ∀ᶠ x in l, ∥f x∥ ≤ c * ∥g' x∥ :=
+is_O_iff_eventually_is_O_with.trans $ by simp only [is_O_with]
+
 /-! ### Subsingleton -/
 
 @[nontriviality] lemma is_o_of_subsingleton [subsingleton E'] : is_o f' g' l :=
@@ -176,7 +185,7 @@ theorem is_O_with_congr {c₁ c₂} {f₁ f₂ : α → E} {g₁ g₂ : α → F
 begin
   unfold is_O_with,
   subst c₂,
-  apply filter.congr_sets,
+  apply filter.eventually_congr,
   filter_upwards [hf, hg],
   assume x e₁ e₂,
   rw [e₁, e₂]
@@ -1327,6 +1336,28 @@ theorem is_O_one_nat_at_top_iff {f : ℕ → E'} :
 iff.trans (is_O_nat_at_top_iff (λ n h, (one_ne_zero h).elim)) $
   by simp only [norm_one, mul_one]
 
+theorem is_O_with_pi {ι : Type*} [fintype ι] {E' : ι → Type*} [Π i, normed_group (E' i)]
+  {f : α → Π i, E' i} {C : ℝ} (hC : 0 ≤ C) :
+  is_O_with C f g' l ↔ ∀ i, is_O_with C (λ x, f x i) g' l :=
+have ∀ x, 0 ≤ C * ∥g' x∥, from λ x, mul_nonneg hC (norm_nonneg _),
+by simp only [is_O_with_iff, pi_norm_le_iff (this _), eventually_all]
+
+@[simp] theorem is_O_pi {ι : Type*} [fintype ι] {E' : ι → Type*} [Π i, normed_group (E' i)]
+  {f : α → Π i, E' i} :
+  is_O f g' l ↔ ∀ i, is_O (λ x, f x i) g' l :=
+begin
+  simp only [is_O_iff_eventually_is_O_with, ← eventually_all],
+  exact eventually_congr (eventually_at_top.2 ⟨0, λ c, is_O_with_pi⟩)
+end
+
+@[simp] theorem is_o_pi {ι : Type*} [fintype ι] {E' : ι → Type*} [Π i, normed_group (E' i)]
+  {f : α → Π i, E' i} :
+  is_o f g' l ↔ ∀ i, is_o (λ x, f x i) g' l :=
+begin
+  simp only [is_o, is_O_with_pi, le_of_lt] { contextual := tt },
+  exact ⟨λ h i c hc, h hc i, λ h c hc i, h i hc⟩
+end
+
 end asymptotics
 
 open asymptotics

src/analysis/calculus/deriv.lean

@@ -675,6 +675,41 @@ lemma deriv_within_sum (hxs : unique_diff_within_at 𝕜 s x)
 
 end sum
 
+section pi
+
+/-! ### Derivatives of functions `f : 𝕜 → Π i, E i` -/
+
+variables {ι : Type*} [fintype ι] {E' : ι → Type*} [Π i, normed_group (E' i)]
+  [Π i, normed_space 𝕜 (E' i)] {φ : 𝕜 → Π i, E' i} {φ' : Π i, E' i}
+
+@[simp] lemma has_strict_deriv_at_pi :
+  has_strict_deriv_at φ φ' x ↔ ∀ i, has_strict_deriv_at (λ x, φ x i) (φ' i) x :=
+has_strict_fderiv_at_pi'
+
+@[simp] lemma has_deriv_at_filter_pi :
+  has_deriv_at_filter φ φ' x L ↔
+    ∀ i, has_deriv_at_filter (λ x, φ x i) (φ' i) x L :=
+has_fderiv_at_filter_pi'
+
+lemma has_deriv_at_pi :
+  has_deriv_at φ φ' x ↔ ∀ i, has_deriv_at (λ x, φ x i) (φ' i) x:=
+has_deriv_at_filter_pi
+
+lemma has_deriv_within_at_pi :
+  has_deriv_within_at φ φ' s x ↔ ∀ i, has_deriv_within_at (λ x, φ x i) (φ' i) s x:=
+has_deriv_at_filter_pi
+
+lemma deriv_within_pi (h : ∀ i, differentiable_within_at 𝕜 (λ x, φ x i) s x)
+  (hs : unique_diff_within_at 𝕜 s x) :
+  deriv_within φ s x = λ i, deriv_within (λ x, φ x i) s x :=
+(has_deriv_within_at_pi.2 (λ i, (h i).has_deriv_within_at)).deriv_within hs
+
+lemma deriv_pi (h : ∀ i, differentiable_at 𝕜 (λ x, φ x i) x) :
+  deriv φ x = λ i, deriv (λ x, φ x i) x :=
+(has_deriv_at_pi.2 (λ i, (h i).has_deriv_at)).deriv
+
+end pi
+
 section mul_vector
 /-! ### Derivative of the multiplication of a scalar function and a vector function -/
 variables {c : 𝕜 → 𝕜} {c' : 𝕜}

src/analysis/calculus/fderiv.lean

@@ -1680,6 +1680,104 @@ theorem fderiv_sum (h : ∀ i ∈ u, differentiable_at 𝕜 (A i) x) :
 
 end sum
 
+section pi
+
+/-!
+### Derivatives of functions `f : E → Π i, F' i`
+
+In this section we formulate `has_*fderiv*_pi` theorems as `iff`s, and provide two versions of each
+theorem:
+
+* the version without `'` deals with `φ : Π i, E → F' i` and `φ' : Π i, E →L[𝕜] F' i`
+  and is designed to deduce differentiability of `λ x i, φ i x` from differentiability
+  of each `φ i`;
+* the version with `'` deals with `Φ : E → Π i, F' i` and `Φ' : E →L[𝕜] Π i, F' i`
+  and is designed to deduce differentiability of the components `λ x, Φ x i` from
+  differentiability of `Φ`.
+-/
+
+variables {ι : Type*} [fintype ι] {F' : ι → Type*} [Π i, normed_group (F' i)]
+  [Π i, normed_space 𝕜 (F' i)] {φ : Π i, E → F' i} {φ' : Π i, E →L[𝕜] F' i}
+  {Φ : E → Π i, F' i} {Φ' : E →L[𝕜] Π i, F' i}
+
+@[simp] lemma has_strict_fderiv_at_pi' :
+  has_strict_fderiv_at Φ Φ' x ↔
+    ∀ i, has_strict_fderiv_at (λ x, Φ x i) ((proj i).comp Φ') x :=
+begin
+  simp only [has_strict_fderiv_at, continuous_linear_map.coe_pi],
+  exact is_o_pi
+end
+
+@[simp] lemma has_strict_fderiv_at_pi :
+  has_strict_fderiv_at (λ x i, φ i x) (continuous_linear_map.pi φ') x ↔
+    ∀ i, has_strict_fderiv_at (φ i) (φ' i) x :=
+has_strict_fderiv_at_pi'
+
+@[simp] lemma has_fderiv_at_filter_pi' :
+  has_fderiv_at_filter Φ Φ' x L ↔
+    ∀ i, has_fderiv_at_filter (λ x, Φ x i) ((proj i).comp Φ') x L :=
+begin
+  simp only [has_fderiv_at_filter, continuous_linear_map.coe_pi],
+  exact is_o_pi
+end
+
+lemma has_fderiv_at_filter_pi :
+  has_fderiv_at_filter (λ x i, φ i x) (continuous_linear_map.pi φ') x L ↔
+    ∀ i, has_fderiv_at_filter (φ i) (φ' i) x L :=
+has_fderiv_at_filter_pi'
+
+@[simp] lemma has_fderiv_at_pi' :
+  has_fderiv_at Φ Φ' x ↔
+    ∀ i, has_fderiv_at (λ x, Φ x i) ((proj i).comp Φ') x :=
+has_fderiv_at_filter_pi'
+
+lemma has_fderiv_at_pi :
+  has_fderiv_at (λ x i, φ i x) (continuous_linear_map.pi φ') x ↔
+    ∀ i, has_fderiv_at (φ i) (φ' i) x :=
+has_fderiv_at_filter_pi
+
+@[simp] lemma has_fderiv_within_at_pi' :
+  has_fderiv_within_at Φ Φ' s x ↔
+    ∀ i, has_fderiv_within_at (λ x, Φ x i) ((proj i).comp Φ') s x :=
+has_fderiv_at_filter_pi'
+
+lemma has_fderiv_within_at_pi :
+  has_fderiv_within_at (λ x i, φ i x) (continuous_linear_map.pi φ') s x ↔
+    ∀ i, has_fderiv_within_at (φ i) (φ' i) s x :=
+has_fderiv_at_filter_pi
+
+@[simp] lemma differentiable_within_at_pi :
+  differentiable_within_at 𝕜 Φ s x ↔
+   ∀ i, differentiable_within_at 𝕜 (λ x, Φ x i) s x :=
+⟨λ h i, (has_fderiv_within_at_pi'.1 h.has_fderiv_within_at i).differentiable_within_at,
+  λ h, (has_fderiv_within_at_pi.2 (λ i, (h i).has_fderiv_within_at)).differentiable_within_at⟩
+
+@[simp] lemma differentiable_at_pi :
+  differentiable_at 𝕜 Φ x ↔ ∀ i, differentiable_at 𝕜 (λ x, Φ x i) x :=
+⟨λ h i, (has_fderiv_at_pi'.1 h.has_fderiv_at i).differentiable_at,
+  λ h, (has_fderiv_at_pi.2 (λ i, (h i).has_fderiv_at)).differentiable_at⟩
+
+lemma differentiable_on_pi :
+  differentiable_on 𝕜 Φ s ↔ ∀ i, differentiable_on 𝕜 (λ x, Φ x i) s :=
+⟨λ h i x hx, differentiable_within_at_pi.1 (h x hx) i,
+  λ h x hx, differentiable_within_at_pi.2 (λ i, h i x hx)⟩
+
+lemma differentiable_pi :
+  differentiable 𝕜 Φ ↔ ∀ i, differentiable 𝕜 (λ x, Φ x i) :=
+⟨λ h i x, differentiable_at_pi.1 (h x) i, λ h x, differentiable_at_pi.2 (λ i, h i x)⟩
+
+-- TODO: find out which version (`φ` or `Φ`) works better with `rw`/`simp`
+lemma fderiv_within_pi (h : ∀ i, differentiable_within_at 𝕜 (φ i) s x)
+  (hs : unique_diff_within_at 𝕜 s x) :
+  fderiv_within 𝕜 (λ x i, φ i x) s x = pi (λ i, fderiv_within 𝕜 (φ i) s x) :=
+(has_fderiv_within_at_pi.2 (λ i, (h i).has_fderiv_within_at)).fderiv_within hs
+
+lemma fderiv_pi (h : ∀ i, differentiable_at 𝕜 (φ i) x) :
+  fderiv 𝕜 (λ x i, φ i x) x = pi (λ i, fderiv 𝕜 (φ i) x) :=
+(has_fderiv_at_pi.2 (λ i, (h i).has_fderiv_at)).fderiv
+
+end pi
+
 section neg
 /-! ### Derivative of the negative of a function -/
 

src/topology/algebra/module.lean

@@ -613,16 +613,17 @@ variables
 /-- `pi` construction for continuous linear functions. From a family of continuous linear functions
 it produces a continuous linear function into a family of topological modules. -/
 def pi (f : Πi, M →L[R] φ i) : M →L[R] (Πi, φ i) :=
-⟨linear_map.pi (λ i, (f i : M →ₗ[R] φ i)),
- continuous_pi (λ i, (f i).continuous)⟩
+⟨linear_map.pi (λ i, f i), continuous_pi (λ i, (f i).continuous)⟩
 
-@[simp] lemma pi_apply (f : Πi, M →L[R] φ i) (c : M) (i : ι) :
+@[simp] lemma coe_pi (f : Π i, M →L[R] φ i) : ⇑(pi f) = λ c i, f i c := rfl
+
+lemma pi_apply (f : Πi, M →L[R] φ i) (c : M) (i : ι) :
   pi f c i = f i c := rfl
 
 lemma pi_eq_zero (f : Πi, M →L[R] φ i) : pi f = 0 ↔ (∀i, f i = 0) :=
-by simp only [ext_iff, pi_apply, function.funext_iff]; exact ⟨λh a b, h b a, λh a b, h b a⟩
+by { simp only [ext_iff, pi_apply, function.funext_iff], exact forall_swap }
 
-lemma pi_zero : pi (λi, 0 : Πi, M →L[R] φ i) = 0 := by ext; refl
+lemma pi_zero : pi (λi, 0 : Πi, M →L[R] φ i) = 0 := ext $ λ _, rfl
 
 lemma pi_comp (f : Πi, M →L[R] φ i) (g : M₂ →L[R] M) : (pi f).comp g = pi (λi, (f i).comp g) := rfl