Commit 2026-02-18 03:15 d6f48e47

View on Github →

refactor(Analysis/Calculus): redefine HasFDerivAtFilter (#34965) Make HasFDerivAtFilter and HasDerivAtFilter to take a filter in the Cartesian square of the domain, so that it works for HasStrictFDerivAt and HasStrictDerivAt. Other changes:

  • golf proofs about hasDerivAt_pi etc, dropping [Finite ι] assumption;
  • move proofs about HasFDerivAtFilter before HasStrictFDerivAt, use them;
  • add lemmas like hasFDerivAt_iff_isLittleO, since the old idiom rw [HasFDerivAt, hasFDerivAtFilter_iff_isLittleO] no longer gives the desired result. See Zulip discussion

Estimated changes

added theorem HasDerivAt.add
added theorem HasDerivAtFilter.add
modified theorem HasDerivAtFilter.const_sub
modified theorem HasDerivAtFilter.fun_sum
modified theorem HasDerivAtFilter.neg
modified theorem HasDerivAtFilter.sub
modified theorem HasDerivAtFilter.sum
added theorem HasDerivWithinAt.add
added theorem HasStrictDerivAt.add
modified theorem HasStrictDerivAt.neg
modified theorem hasDerivAtFilter_neg
modified theorem AffineMap.hasDerivAtFilter
modified theorem AffineMap.hasStrictDerivAt
modified theorem HasDerivAt.hasDerivAtFilter
added theorem HasDerivAt.isBigO_sub
modified theorem HasDerivAtFilter.isBigO_sub
modified theorem HasDerivAtFilter.mono
modified def HasDerivAtFilter
deleted theorem HasFDerivAt.hasDerivAt
modified theorem hasDerivAtFilter_const
modified theorem hasDerivAtFilter_id
modified theorem hasDerivAtFilter_intCast
modified theorem hasDerivAtFilter_natCast
modified theorem hasDerivAtFilter_ofNat
modified theorem hasDerivAtFilter_one
modified theorem hasDerivAtFilter_zero
added theorem HasDerivAt.comp
added theorem HasDerivAt.scomp
modified theorem HasDerivAtFilter.comp
modified theorem HasDerivAtFilter.comp_of_eq
modified theorem HasDerivAtFilter.scomp
added theorem HasDerivWithinAt.scomp
modified theorem HasDerivAtFilter.const_smul
added theorem HasDerivWithinAt.pow'
added theorem HasDerivWithinAt.pow
added theorem HasStrictDerivAt.pow'
added theorem HasStrictDerivAt.pow
added theorem HasDerivAt.prodMk
modified theorem HasDerivAtFilter.finCons
modified theorem hasDerivAtFilter_finCons'
modified theorem hasDerivAtFilter_finCons
added theorem HasFDerivAt.const_sub
modified theorem HasFDerivAtFilter.add
modified theorem HasFDerivAtFilter.const_sub
modified theorem HasFDerivAtFilter.fun_sum
modified theorem HasFDerivAtFilter.neg
modified theorem HasFDerivAtFilter.sub
modified theorem HasFDerivAtFilter.sum
modified theorem HasFDerivAt.isBigOTVS_sub
modified theorem hasFDerivAtFilter_id
modified theorem HasFDerivAtFilter.comp
modified theorem hasFDerivAtFilter_const
modified theorem hasFDerivAtFilter_intCast
modified theorem hasFDerivAtFilter_natCast
modified theorem hasFDerivAtFilter_ofNat
modified theorem hasFDerivAtFilter_one
modified theorem hasFDerivAtFilter_zero
modified structure HasFDerivAtFilter
deleted structure HasStrictFDerivAt
modified theorem HasFDerivAtFilter.prodMk
modified theorem hasFDerivAtFilter_fst
modified theorem hasFDerivAtFilter_snd