Commit 2025-05-27 02:03 856176e4

View on Github →

chore(Analysis/Calculus): split long file FDeriv/Basic.lean (#25207)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Analysis/Calculus/Conformal/NormedSpace.lean

Modified Mathlib/Analysis/Calculus/Deriv/Basic.lean

Modified Mathlib/Analysis/Calculus/FDeriv/Basic.lean

deleted def Differentiable

deleted theorem DifferentiableAt.congr_of_eventuallyEq

deleted def DifferentiableAt

deleted theorem DifferentiableOn.congr

deleted theorem DifferentiableOn.congr_mono

deleted def DifferentiableOn

deleted theorem DifferentiableWithinAt.congr

deleted theorem DifferentiableWithinAt.congr_mono

deleted theorem DifferentiableWithinAt.congr_of_eventuallyEq

deleted theorem DifferentiableWithinAt.congr_of_eventuallyEq_insert

deleted theorem DifferentiableWithinAt.congr_of_eventuallyEq_of_mem

deleted theorem DifferentiableWithinAt.fderivWithin_congr_mono

deleted def DifferentiableWithinAt

deleted theorem Filter.EventuallyEq.differentiableAt_iff

deleted theorem Filter.EventuallyEq.differentiableWithinAt_iff

deleted theorem Filter.EventuallyEq.differentiableWithinAt_iff_of_mem

deleted theorem Filter.EventuallyEq.fderivWithin'

deleted theorem Filter.EventuallyEq.fderivWithin_eq

deleted theorem Filter.EventuallyEq.fderivWithin_eq_of_insert

deleted theorem Filter.EventuallyEq.fderivWithin_eq_of_mem

deleted theorem Filter.EventuallyEq.fderivWithin_eq_of_nhds

deleted theorem Filter.EventuallyEq.fderiv_eq

deleted theorem Filter.EventuallyEq.hasFDerivAtFilter_iff

deleted theorem Filter.EventuallyEq.hasFDerivAt_iff

deleted theorem Filter.EventuallyEq.hasFDerivWithinAt_iff

deleted theorem Filter.EventuallyEq.hasFDerivWithinAt_iff_of_mem

deleted theorem Filter.EventuallyEq.hasStrictFDerivAt_iff

deleted theorem HasFDerivAt.congr_fderiv

deleted theorem HasFDerivAt.congr_of_eventuallyEq

deleted theorem HasFDerivAt.of_notMem_tsupport

deleted def HasFDerivAt

deleted theorem HasFDerivAtFilter.congr_of_eventuallyEq

deleted structure HasFDerivAtFilter

deleted theorem HasFDerivWithinAt.congr'

deleted theorem HasFDerivWithinAt.congr

deleted theorem HasFDerivWithinAt.congr_fderiv

deleted theorem HasFDerivWithinAt.congr_mono

deleted theorem HasFDerivWithinAt.congr_of_eventuallyEq

deleted theorem HasFDerivWithinAt.of_notMem_tsupport

deleted def HasFDerivWithinAt

deleted theorem HasStrictFDerivAt.congr_fderiv

deleted theorem HasStrictFDerivAt.congr_of_eventuallyEq

deleted theorem HasStrictFDerivAt.of_notMem_tsupport

deleted structure HasStrictFDerivAt

deleted theorem Set.Subsingleton.differentiableOn

deleted theorem differentiableAt_const

deleted theorem differentiableAt_intCast

deleted theorem differentiableAt_natCast

deleted theorem differentiableAt_ofNat

deleted theorem differentiableAt_of_isInvertible_fderiv

deleted theorem differentiableAt_one

deleted theorem differentiableAt_zero

deleted theorem differentiableOn_congr

deleted theorem differentiableOn_const

deleted theorem differentiableOn_empty

deleted theorem differentiableOn_intCast

deleted theorem differentiableOn_natCast

deleted theorem differentiableOn_ofNat

deleted theorem differentiableOn_one

deleted theorem differentiableOn_singleton

deleted theorem differentiableOn_zero

deleted theorem differentiableWithinAt_congr_set'

deleted theorem differentiableWithinAt_congr_set

deleted theorem differentiableWithinAt_const

deleted theorem differentiableWithinAt_intCast

deleted theorem differentiableWithinAt_natCast

deleted theorem differentiableWithinAt_ofNat

deleted theorem differentiableWithinAt_of_isInvertible_fderivWithin

deleted theorem differentiableWithinAt_one

deleted theorem differentiableWithinAt_zero

deleted theorem differentiable_const

deleted theorem differentiable_intCast

deleted theorem differentiable_natCast

deleted theorem differentiable_ofNat

deleted theorem differentiable_one

deleted theorem differentiable_zero

deleted theorem fderivWithin_congr'

deleted theorem fderivWithin_congr

deleted theorem fderivWithin_congr_set'

deleted theorem fderivWithin_congr_set

deleted theorem fderivWithin_const

deleted theorem fderivWithin_const_apply

deleted theorem fderivWithin_eventually_congr_set'

deleted theorem fderivWithin_eventually_congr_set

deleted theorem fderivWithin_fun_const

deleted theorem fderivWithin_intCast

deleted theorem fderivWithin_natCast

deleted theorem fderivWithin_ofNat

deleted theorem fderivWithin_one

deleted theorem fderivWithin_univ

deleted theorem fderivWithin_zero

deleted theorem fderivWithin_zero_of_not_differentiableWithinAt

deleted theorem fderiv_const

deleted theorem fderiv_const_apply

deleted theorem fderiv_fun_const

deleted theorem fderiv_intCast

deleted theorem fderiv_natCast

deleted theorem fderiv_ofNat

deleted theorem fderiv_of_notMem_tsupport

deleted theorem fderiv_one

deleted theorem fderiv_zero

deleted theorem hasFDerivAtFilter_const

deleted theorem hasFDerivAtFilter_iff_isLittleO

deleted theorem hasFDerivAtFilter_intCast

deleted theorem hasFDerivAtFilter_natCast

deleted theorem hasFDerivAtFilter_ofNat

deleted theorem hasFDerivAtFilter_one

deleted theorem hasFDerivAtFilter_zero

deleted theorem hasFDerivAt_const

deleted theorem hasFDerivAt_intCast

deleted theorem hasFDerivAt_natCast

deleted theorem hasFDerivAt_ofNat

deleted theorem hasFDerivAt_of_subsingleton

deleted theorem hasFDerivAt_one

deleted theorem hasFDerivAt_zero

deleted theorem hasFDerivAt_zero_of_eventually_const

deleted theorem hasFDerivWithinAt_congr_set'

deleted theorem hasFDerivWithinAt_congr_set

deleted theorem hasFDerivWithinAt_const

deleted theorem hasFDerivWithinAt_intCast

deleted theorem hasFDerivWithinAt_natCast

deleted theorem hasFDerivWithinAt_ofNat

deleted theorem hasFDerivWithinAt_one

deleted theorem hasFDerivWithinAt_singleton

deleted theorem hasFDerivWithinAt_zero

deleted theorem hasStrictFDerivAt_const

deleted theorem hasStrictFDerivAt_iff_isLittleO

deleted theorem hasStrictFDerivAt_intCast

deleted theorem hasStrictFDerivAt_natCast

deleted theorem hasStrictFDerivAt_ofNat

deleted theorem hasStrictFDerivAt_one

deleted theorem hasStrictFDerivAt_zero

deleted theorem support_fderiv_subset

deleted theorem tsupport_fderiv_subset

Created Mathlib/Analysis/Calculus/FDeriv/Congr.lean

added theorem DifferentiableAt.congr_of_eventuallyEq

added theorem DifferentiableOn.congr

added theorem DifferentiableOn.congr_mono

added theorem DifferentiableWithinAt.congr

added theorem DifferentiableWithinAt.congr_mono

added theorem DifferentiableWithinAt.congr_of_eventuallyEq

added theorem DifferentiableWithinAt.congr_of_eventuallyEq_insert

added theorem DifferentiableWithinAt.congr_of_eventuallyEq_of_mem

added theorem DifferentiableWithinAt.fderivWithin_congr_mono

added theorem Filter.EventuallyEq.differentiableAt_iff

added theorem Filter.EventuallyEq.differentiableWithinAt_iff

added theorem Filter.EventuallyEq.differentiableWithinAt_iff_of_mem

added theorem Filter.EventuallyEq.fderivWithin'

added theorem Filter.EventuallyEq.fderivWithin_eq

added theorem Filter.EventuallyEq.fderivWithin_eq_of_insert

added theorem Filter.EventuallyEq.fderivWithin_eq_of_mem

added theorem Filter.EventuallyEq.fderivWithin_eq_of_nhds

added theorem Filter.EventuallyEq.fderiv_eq

added theorem Filter.EventuallyEq.hasFDerivAtFilter_iff

added theorem Filter.EventuallyEq.hasFDerivAt_iff

added theorem Filter.EventuallyEq.hasFDerivWithinAt_iff

added theorem Filter.EventuallyEq.hasFDerivWithinAt_iff_of_mem

added theorem Filter.EventuallyEq.hasStrictFDerivAt_iff

added theorem HasFDerivAt.congr_fderiv

added theorem HasFDerivAt.congr_of_eventuallyEq

added theorem HasFDerivAtFilter.congr_of_eventuallyEq

added theorem HasFDerivWithinAt.congr'

added theorem HasFDerivWithinAt.congr

added theorem HasFDerivWithinAt.congr_fderiv

added theorem HasFDerivWithinAt.congr_mono

added theorem HasFDerivWithinAt.congr_of_eventuallyEq

added theorem HasStrictFDerivAt.congr_fderiv

added theorem HasStrictFDerivAt.congr_of_eventuallyEq

added theorem differentiableOn_congr

added theorem differentiableWithinAt_congr_set'

added theorem differentiableWithinAt_congr_set

added theorem fderivWithin_congr'

added theorem fderivWithin_congr

added theorem fderivWithin_congr_set'

added theorem fderivWithin_congr_set

added theorem fderivWithin_eventually_congr_set'

added theorem fderivWithin_eventually_congr_set

added theorem hasFDerivWithinAt_congr_set'

added theorem hasFDerivWithinAt_congr_set

Created Mathlib/Analysis/Calculus/FDeriv/Const.lean

added theorem HasFDerivAt.of_notMem_tsupport

added theorem HasFDerivWithinAt.of_notMem_tsupport

added theorem HasStrictFDerivAt.of_notMem_tsupport

added theorem Set.Subsingleton.differentiableOn

added theorem differentiableAt_const

added theorem differentiableAt_intCast

added theorem differentiableAt_natCast

added theorem differentiableAt_ofNat

added theorem differentiableAt_of_isInvertible_fderiv

added theorem differentiableAt_one

added theorem differentiableAt_zero

added theorem differentiableOn_const

added theorem differentiableOn_empty

added theorem differentiableOn_intCast

added theorem differentiableOn_natCast

added theorem differentiableOn_ofNat

added theorem differentiableOn_one

added theorem differentiableOn_singleton

added theorem differentiableOn_zero

added theorem differentiableWithinAt_const

added theorem differentiableWithinAt_intCast

added theorem differentiableWithinAt_natCast

added theorem differentiableWithinAt_ofNat

added theorem differentiableWithinAt_of_isInvertible_fderivWithin

added theorem differentiableWithinAt_one

added theorem differentiableWithinAt_zero

added theorem differentiable_const

added theorem differentiable_intCast

added theorem differentiable_natCast

added theorem differentiable_ofNat

added theorem differentiable_one

added theorem differentiable_zero

added theorem fderivWithin_const

added theorem fderivWithin_const_apply

added theorem fderivWithin_fun_const

added theorem fderivWithin_intCast

added theorem fderivWithin_natCast

added theorem fderivWithin_ofNat

added theorem fderivWithin_one

added theorem fderivWithin_zero

added theorem fderiv_const

added theorem fderiv_const_apply

added theorem fderiv_fun_const

added theorem fderiv_intCast

added theorem fderiv_natCast

added theorem fderiv_ofNat

added theorem fderiv_of_notMem_tsupport

added theorem fderiv_one

added theorem fderiv_zero

added theorem hasFDerivAtFilter_const

added theorem hasFDerivAtFilter_intCast

added theorem hasFDerivAtFilter_natCast

added theorem hasFDerivAtFilter_ofNat

added theorem hasFDerivAtFilter_one

added theorem hasFDerivAtFilter_zero

added theorem hasFDerivAt_const

added theorem hasFDerivAt_intCast

added theorem hasFDerivAt_natCast

added theorem hasFDerivAt_ofNat

added theorem hasFDerivAt_of_subsingleton

added theorem hasFDerivAt_one

added theorem hasFDerivAt_zero

added theorem hasFDerivAt_zero_of_eventually_const

added theorem hasFDerivWithinAt_const

added theorem hasFDerivWithinAt_intCast

added theorem hasFDerivWithinAt_natCast

added theorem hasFDerivWithinAt_ofNat

added theorem hasFDerivWithinAt_one

added theorem hasFDerivWithinAt_singleton

added theorem hasFDerivWithinAt_zero

added theorem hasStrictFDerivAt_const

added theorem hasStrictFDerivAt_intCast

added theorem hasStrictFDerivAt_natCast

added theorem hasStrictFDerivAt_ofNat

added theorem hasStrictFDerivAt_one

added theorem hasStrictFDerivAt_zero

added theorem support_fderiv_subset

added theorem tsupport_fderiv_subset

Created Mathlib/Analysis/Calculus/FDeriv/Defs.lean

added def Differentiable

added def DifferentiableAt

added def DifferentiableOn

added def DifferentiableWithinAt

added def HasFDerivAt

added structure HasFDerivAtFilter

added def HasFDerivWithinAt

added structure HasStrictFDerivAt

added theorem fderivWithin_univ

added theorem fderivWithin_zero_of_not_differentiableWithinAt

added theorem hasFDerivAtFilter_iff_isLittleO

added theorem hasStrictFDerivAt_iff_isLittleO

Modified Mathlib/Analysis/Calculus/FDeriv/Equiv.lean

Modified Mathlib/Analysis/Calculus/FDeriv/Pi.lean

Modified Mathlib/Analysis/Calculus/FDeriv/Prod.lean

Modified Mathlib/Analysis/Complex/Angle.lean