Commit 2026-02-03 17:15 33a2f730

View on Github →

refactor(Analysis/Calculus): split long file ContDiff/Basic.lean (#34764) Split Mathlib.Analysis.Calculus.ContDiff.Basic into 3 chunks, Basic (~600 lines), Comp (~800), and Deriv (~150). Also, in making the downstream changes, I realised that Mathlib.Analysis.Convolution is ~1400 lines and imports a bunch of calculus-related stuff which is only used at the very end of the file, so I split that one up too: Mathlib.Analysis.Convolution (~1000 lines) for the purely measure-theoretic stuff and Mathlib.Analysis.Calculus.ContDiff.Convolution (~450) for differentiability of the convolution.

Estimated changes

deleted theorem ContDiff.clm_apply
deleted theorem ContDiff.clm_comp
deleted theorem ContDiff.comp
deleted theorem ContDiff.comp_contDiffAt
deleted theorem ContDiff.comp_contDiffOn
deleted theorem ContDiff.comp₂
deleted theorem ContDiff.comp₃
deleted theorem ContDiff.continuous_deriv
deleted theorem ContDiff.deriv'
deleted theorem ContDiff.fderiv_apply
deleted theorem ContDiff.fderiv_right
deleted theorem ContDiff.fst'
deleted theorem ContDiff.fst
deleted theorem ContDiff.fun_comp
deleted theorem ContDiff.iterate_deriv'
deleted theorem ContDiff.iterate_deriv
deleted theorem ContDiff.smulRight
deleted theorem ContDiff.snd'
deleted theorem ContDiff.snd
deleted theorem ContDiffAt.clm_apply
deleted theorem ContDiffAt.clm_comp
deleted theorem ContDiffAt.comp₂
deleted theorem ContDiffAt.fderiv_right
deleted theorem ContDiffAt.fst''
deleted theorem ContDiffAt.fst'
deleted theorem ContDiffAt.fst
deleted theorem ContDiffAt.fun_comp
deleted theorem ContDiffAt.smulRight
deleted theorem ContDiffAt.snd''
deleted theorem ContDiffAt.snd'
deleted theorem ContDiffAt.snd
deleted theorem ContDiffOn.clm_apply
deleted theorem ContDiffOn.clm_comp
deleted theorem ContDiffOn.comp
deleted theorem ContDiffOn.comp_contDiff
deleted theorem ContDiffOn.comp_inter
deleted theorem ContDiffOn.fst
deleted theorem ContDiffOn.smulRight
deleted theorem ContDiffOn.snd
deleted theorem ContDiffWithinAt.clm_comp
deleted theorem ContDiffWithinAt.comp
deleted theorem Continuous.fderiv
deleted theorem Continuous.fderiv_one
deleted theorem contDiffAt_fst
deleted theorem contDiffAt_snd
deleted theorem contDiffOn_fst
deleted theorem contDiffOn_snd
deleted theorem contDiffWithinAt_fst
deleted theorem contDiffWithinAt_snd
deleted theorem contDiff_fst
deleted theorem contDiff_infty_iff_deriv
deleted theorem contDiff_one_iff_deriv
deleted theorem contDiff_snd
deleted theorem contDiff_succ_iff_deriv
deleted theorem iteratedFDerivWithin_comp
deleted theorem iteratedFDeriv_comp
added theorem ContDiff.clm_apply
added theorem ContDiff.clm_comp
added theorem ContDiff.comp
added theorem ContDiff.comp₂
added theorem ContDiff.comp₃
added theorem ContDiff.fderiv_apply
added theorem ContDiff.fderiv_right
added theorem ContDiff.fst'
added theorem ContDiff.fst
added theorem ContDiff.fun_comp
added theorem ContDiff.smulRight
added theorem ContDiff.snd'
added theorem ContDiff.snd
added theorem ContDiffAt.clm_apply
added theorem ContDiffAt.clm_comp
added theorem ContDiffAt.comp₂
added theorem ContDiffAt.fst''
added theorem ContDiffAt.fst'
added theorem ContDiffAt.fst
added theorem ContDiffAt.fun_comp
added theorem ContDiffAt.smulRight
added theorem ContDiffAt.snd''
added theorem ContDiffAt.snd'
added theorem ContDiffAt.snd
added theorem ContDiffOn.clm_apply
added theorem ContDiffOn.clm_comp
added theorem ContDiffOn.comp
added theorem ContDiffOn.comp_inter
added theorem ContDiffOn.fst
added theorem ContDiffOn.smulRight
added theorem ContDiffOn.snd
added theorem ContDiffWithinAt.comp
added theorem Continuous.fderiv
added theorem Continuous.fderiv_one
added theorem contDiffAt_fst
added theorem contDiffAt_snd
added theorem contDiffOn_fst
added theorem contDiffOn_snd
added theorem contDiffWithinAt_fst
added theorem contDiffWithinAt_snd
added theorem contDiff_fst
added theorem contDiff_snd
added theorem iteratedFDeriv_comp
added theorem ContDiff.deriv'
added theorem ContDiff.iterate_deriv
added theorem contDiff_one_iff_deriv