Commit 2024-02-29 18:56 77166edf

View on Github →

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}

Estimated changes

modified theorem Finset.prod_attach_univ
added theorem HasDerivAt.finset_prod
added theorem deriv_finset_prod
added theorem HasFDerivAt.list_prod'
added theorem fderiv_finset_prod
added theorem fderiv_list_prod'
added theorem fderiv_multiset_prod
added theorem hasFDerivAt_list_prod'
added theorem List.erase_get
added theorem List.Nodup.erase_get
added theorem Sym.card_coe