feat: Add norm_iteratedFDeriv_prod_le using Sym (#10022)

add (iterated) deriv for prod

* Add `HasFDerivAt` + variants for `Finset.prod` (and `ContinuousMultilinearMap.mkPiAlgebra`)
* Add missing `iteratedFDerivWithin` equivalents for zero, const (resolves a todo in `Analysis.Calculus.ContDiff.Basic`)
* Add `iteratedFDeriv[Within]_sum` for symmetry
* Add a couple of convenience lemmas for `Sym` and `Finset.{prod,sum}`

Author: jvlmdr

Mathlib/Algebra/BigOperators/Basic.lean

@@ -2322,15 +2322,21 @@ theorem prod_subtype_mul_prod_subtype {α β : Type*} [Fintype α] [CommMonoid 
 end Fintype
 
 namespace Finset
-variable [Fintype ι] [CommMonoid α]
+variable [CommMonoid α]
 
 @[to_additive (attr := simp)]
-lemma prod_attach_univ (f : {i // i ∈ @univ ι _} → α) :
+lemma prod_attach_univ [Fintype ι] (f : {i // i ∈ @univ ι _} → α) :
     ∏ i in univ.attach, f i = ∏ i, f ⟨i, mem_univ _⟩ :=
   Fintype.prod_equiv (Equiv.subtypeUnivEquiv mem_univ) _ _ $ by simp
 #align finset.prod_attach_univ Finset.prod_attach_univ
 #align finset.sum_attach_univ Finset.sum_attach_univ
 
+@[to_additive]
+theorem prod_erase_attach [DecidableEq ι] {s : Finset ι} (f : ι → α) (i : ↑s) :
+    ∏ j in s.attach.erase i, f ↑j = ∏ j in s.erase ↑i, f j := by
+  rw [← Function.Embedding.coe_subtype, ← prod_map]
+  simp [attach_map_val]
+
 end Finset
 
 namespace List

Mathlib/Analysis/Calculus/ContDiff/Bounds.lean

@@ -4,7 +4,9 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Sébastien Gouëzel, Floris van Doorn
 -/
 import Mathlib.Analysis.Calculus.ContDiff.Basic
+import Mathlib.Data.Finset.Sym
 import Mathlib.Data.Nat.Choose.Cast
+import Mathlib.Data.Nat.Choose.Multinomial
 
 #align_import analysis.calculus.cont_diff from "leanprover-community/mathlib"@"3bce8d800a6f2b8f63fe1e588fd76a9ff4adcebe"
 
@@ -290,7 +292,8 @@ end
 
 section
 
-variable {A : Type*} [NormedRing A] [NormedAlgebra 𝕜 A]
+variable {ι : Type*} {A : Type*} [NormedRing A] [NormedAlgebra 𝕜 A] {A' : Type*} [NormedCommRing A']
+  [NormedAlgebra 𝕜 A']
 
 theorem norm_iteratedFDerivWithin_mul_le {f : E → A} {g : E → A} {N : ℕ∞} (hf : ContDiffOn 𝕜 N f s)
     (hg : ContDiffOn 𝕜 N g s) (hs : UniqueDiffOn 𝕜 s) {x : E} (hx : x ∈ s) {n : ℕ}
@@ -311,6 +314,62 @@ theorem norm_iteratedFDeriv_mul_le {f : E → A} {g : E → A} {N : ℕ∞} (hf
     hf.contDiffOn hg.contDiffOn uniqueDiffOn_univ (mem_univ x) hn
 #align norm_iterated_fderiv_mul_le norm_iteratedFDeriv_mul_le
 
+-- TODO: Add `norm_iteratedFDeriv[Within]_list_prod_le` for non-commutative `NormedRing A`.
+
+theorem norm_iteratedFDerivWithin_prod_le [DecidableEq ι] [NormOneClass A'] {u : Finset ι}
+    {f : ι → E → A'} {N : ℕ∞} (hf : ∀ i ∈ u, ContDiffOn 𝕜 N (f i) s) (hs : UniqueDiffOn 𝕜 s) {x : E}
+    (hx : x ∈ s) {n : ℕ} (hn : (n : ℕ∞) ≤ N) :
+    ‖iteratedFDerivWithin 𝕜 n (∏ j in u, f j ·) s x‖ ≤
+      ∑ p in u.sym n, (p : Multiset ι).multinomial *
+        ∏ j in u, ‖iteratedFDerivWithin 𝕜 (Multiset.count j p) (f j) s x‖ := by
+  induction u using Finset.induction generalizing n with
+  | empty =>
+    cases n with
+    | zero => simp [Sym.eq_nil_of_card_zero]
+    | succ n => simp [iteratedFDerivWithin_succ_const _ _ hs hx]
+  | @insert i u hi IH =>
+    conv => lhs; simp only [Finset.prod_insert hi]
+    simp only [Finset.mem_insert, forall_eq_or_imp] at hf
+    refine le_trans (norm_iteratedFDerivWithin_mul_le hf.1 (contDiffOn_prod hf.2) hs hx hn) ?_
+    rw [← Finset.sum_coe_sort (Finset.sym _ _)]
+    rw [Finset.sum_equiv (Finset.symInsertEquiv hi) (t := Finset.univ)
+      (g := (fun v ↦ v.multinomial *
+          ∏ j in insert i u, ‖iteratedFDerivWithin 𝕜 (v.count j) (f j) s x‖) ∘
+        Sym.toMultiset ∘ Subtype.val ∘ (Finset.symInsertEquiv hi).symm)
+      (by simp) (by simp only [← comp_apply (g := Finset.symInsertEquiv hi), comp.assoc]; simp)]
+    rw [← Finset.univ_sigma_univ, Finset.sum_sigma, Finset.sum_range]
+    simp only [comp_apply, Finset.symInsertEquiv_symm_apply_coe]
+    refine Finset.sum_le_sum ?_
+    intro m _
+    specialize IH hf.2 (n := n - m) (le_trans (WithTop.coe_le_coe.mpr (n.sub_le m)) hn)
+    refine le_trans (mul_le_mul_of_nonneg_left IH (by simp [mul_nonneg])) ?_
+    rw [Finset.mul_sum, ← Finset.sum_coe_sort]
+    refine Finset.sum_le_sum ?_
+    simp only [Finset.mem_univ, forall_true_left, Subtype.forall, Finset.mem_sym_iff]
+    intro p hp
+    refine le_of_eq ?_
+    rw [Finset.prod_insert hi]
+    have hip : i ∉ p := mt (hp i) hi
+    rw [Sym.count_coe_fill_self_of_not_mem hip, Sym.multinomial_coe_fill_of_not_mem hip]
+    suffices ∏ j in u, ‖iteratedFDerivWithin 𝕜 (Multiset.count j p) (f j) s x‖ =
+        ∏ j in u, ‖iteratedFDerivWithin 𝕜 (Multiset.count j (Sym.fill i m p)) (f j) s x‖ by
+      rw [this, Nat.cast_mul]
+      ring
+    refine Finset.prod_congr rfl ?_
+    intro j hj
+    have hji : j ≠ i := mt (· ▸ hj) hi
+    rw [Sym.count_coe_fill_of_ne hji]
+
+theorem norm_iteratedFDeriv_prod_le [DecidableEq ι] [NormOneClass A'] {u : Finset ι}
+    {f : ι → E → A'} {N : ℕ∞} (hf : ∀ i ∈ u, ContDiff 𝕜 N (f i)) {x : E} {n : ℕ}
+    (hn : (n : ℕ∞) ≤ N) :
+    ‖iteratedFDeriv 𝕜 n (∏ j in u, f j ·) x‖ ≤
+      ∑ p in u.sym n, (p : Multiset ι).multinomial *
+        ∏ j in u, ‖iteratedFDeriv 𝕜 ((p : Multiset ι).count j) (f j) x‖ := by
+  simpa [iteratedFDerivWithin_univ] using
+    norm_iteratedFDerivWithin_prod_le (fun i hi ↦ (hf i hi).contDiffOn) uniqueDiffOn_univ
+      (mem_univ x) hn
+
 end
 
 /-- If the derivatives within a set of `g` at `f x` are bounded by `C`, and the `i`-th derivative

Mathlib/Analysis/Calculus/Deriv/Mul.lean

@@ -283,6 +283,38 @@ theorem deriv_const_mul_field' (u : 𝕜') : (deriv fun x => u * v x) = fun x =>
 
 end Mul
 
+section Prod
+
+variable {ι : Type*} [DecidableEq ι] {𝔸' : Type*} [NormedCommRing 𝔸'] [NormedAlgebra 𝕜 𝔸']
+  {u : Finset ι} {f : ι → 𝕜 → 𝔸'} {f' : ι → 𝔸'}
+
+theorem HasDerivAt.finset_prod (hf : ∀ i ∈ u, HasDerivAt (f i) (f' i) x) :
+    HasDerivAt (∏ i in u, f i ·) (∑ i in u, (∏ j in u.erase i, f j x) • f' i) x := by
+  simpa [ContinuousLinearMap.sum_apply, ContinuousLinearMap.smul_apply] using
+    (HasFDerivAt.finset_prod (fun i hi ↦ (hf i hi).hasFDerivAt)).hasDerivAt
+
+theorem HasDerivWithinAt.finset_prod (hf : ∀ i ∈ u, HasDerivWithinAt (f i) (f' i) s x) :
+    HasDerivWithinAt (∏ i in u, f i ·) (∑ i in u, (∏ j in u.erase i, f j x) • f' i) s x := by
+  simpa [ContinuousLinearMap.sum_apply, ContinuousLinearMap.smul_apply] using
+    (HasFDerivWithinAt.finset_prod (fun i hi ↦ (hf i hi).hasFDerivWithinAt)).hasDerivWithinAt
+
+theorem HasStrictDerivAt.finset_prod (hf : ∀ i ∈ u, HasStrictDerivAt (f i) (f' i) x) :
+    HasStrictDerivAt (∏ i in u, f i ·) (∑ i in u, (∏ j in u.erase i, f j x) • f' i) x := by
+  simpa [ContinuousLinearMap.sum_apply, ContinuousLinearMap.smul_apply] using
+    (HasStrictFDerivAt.finset_prod (fun i hi ↦ (hf i hi).hasStrictFDerivAt)).hasStrictDerivAt
+
+theorem deriv_finset_prod (hf : ∀ i ∈ u, DifferentiableAt 𝕜 (f i) x) :
+    deriv (∏ i in u, f i ·) x = ∑ i in u, (∏ j in u.erase i, f j x) • deriv (f i) x :=
+  (HasDerivAt.finset_prod fun i hi ↦ (hf i hi).hasDerivAt).deriv
+
+theorem derivWithin_finset_prod (hxs : UniqueDiffWithinAt 𝕜 s x)
+    (hf : ∀ i ∈ u, DifferentiableWithinAt 𝕜 (f i) s x) :
+    derivWithin (∏ i in u, f i ·) s x =
+      ∑ i in u, (∏ j in u.erase i, f j x) • derivWithin (f i) s x :=
+  (HasDerivWithinAt.finset_prod fun i hi ↦ (hf i hi).hasDerivWithinAt).derivWithin hxs
+
+end Prod
+
 section Div
 
 variable {𝕜' : Type*} [NontriviallyNormedField 𝕜'] [NormedAlgebra 𝕜 𝕜'] {c d : 𝕜 → 𝕜'} {c' d' : 𝕜'}