Commit 2023-06-01 05:37 622fd5fc

View on Github →

feat: port Analysis.Calculus.ContDiffDef (#4256)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Analysis/Calculus/ContDiffDef.lean

added theorem ContDiff.contDiffAt

added theorem ContDiff.contDiffOn

added theorem ContDiff.contDiffWithinAt

added theorem ContDiff.continuous

added theorem ContDiff.continuous_fderiv

added theorem ContDiff.continuous_fderiv_apply

added theorem ContDiff.continuous_iteratedFDeriv

added theorem ContDiff.differentiable

added theorem ContDiff.differentiable_iteratedFDeriv

added theorem ContDiff.of_le

added theorem ContDiff.of_succ

added theorem ContDiff.one_of_succ

added def ContDiff

added theorem ContDiffAt.congr_of_eventuallyEq

added theorem ContDiffAt.contDiffWithinAt

added theorem ContDiffAt.continuousAt

added theorem ContDiffAt.differentiableAt

added theorem ContDiffAt.of_le

added def ContDiffAt

added theorem ContDiffOn.congr

added theorem ContDiffOn.congr_mono

added theorem ContDiffOn.contDiffWithinAt

added theorem ContDiffOn.continuousOn

added theorem ContDiffOn.continuousOn_fderivWithin

added theorem ContDiffOn.continuousOn_fderiv_of_open

added theorem ContDiffOn.continuousOn_iteratedFDerivWithin

added theorem ContDiffOn.differentiableOn

added theorem ContDiffOn.differentiableOn_iteratedFDerivWithin

added theorem ContDiffOn.fderiv_of_open

added theorem ContDiffOn.mono

added theorem ContDiffOn.of_le

added theorem ContDiffOn.of_succ

added theorem ContDiffOn.one_of_succ

added def ContDiffOn

added theorem ContDiffWithinAt.congr'

added theorem ContDiffWithinAt.congr

added theorem ContDiffWithinAt.congr_nhds

added theorem ContDiffWithinAt.congr_of_eventuallyEq

added theorem ContDiffWithinAt.congr_of_eventuallyEq_insert

added theorem ContDiffWithinAt.congr_of_eventually_eq'

added theorem ContDiffWithinAt.contDiffAt

added theorem ContDiffWithinAt.contDiffOn'

added theorem ContDiffWithinAt.contDiffOn

added theorem ContDiffWithinAt.continuousWithinAt

added theorem ContDiffWithinAt.differentiableWithinAt

added theorem ContDiffWithinAt.differentiableWithinAt_iteratedFDerivWithin

added theorem ContDiffWithinAt.differentiable_within_at'

added theorem ContDiffWithinAt.mono

added theorem ContDiffWithinAt.mono_of_mem

added theorem ContDiffWithinAt.of_le

added def ContDiffWithinAt

added theorem Filter.EventuallyEq.contDiffWithinAt_iff

added theorem Filter.EventuallyEq.iteratedFDerivWithin_eq

added theorem Filter.EventuallyEq.iterated_fderiv_within'

added theorem HasCompactSupport.iteratedFDeriv

added theorem HasFTaylorSeriesUpTo.contDiff

added theorem HasFTaylorSeriesUpTo.continuous

added theorem HasFTaylorSeriesUpTo.differentiable

added theorem HasFTaylorSeriesUpTo.hasFDerivAt

added theorem HasFTaylorSeriesUpTo.hasFTaylorSeriesUpToOn

added theorem HasFTaylorSeriesUpTo.ofLe

added theorem HasFTaylorSeriesUpTo.zero_eq'

added structure HasFTaylorSeriesUpTo

added theorem HasFTaylorSeriesUpToOn.congr

added theorem HasFTaylorSeriesUpToOn.contDiffOn

added theorem HasFTaylorSeriesUpToOn.continuousOn

added theorem HasFTaylorSeriesUpToOn.differentiableAt

added theorem HasFTaylorSeriesUpToOn.differentiableOn

added theorem HasFTaylorSeriesUpToOn.eq_ftaylor_series_of_uniqueDiffOn

added theorem HasFTaylorSeriesUpToOn.eventually_hasFDerivAt

added theorem HasFTaylorSeriesUpToOn.hasFDerivAt

added theorem HasFTaylorSeriesUpToOn.hasFDerivWithinAt

added theorem HasFTaylorSeriesUpToOn.mono

added theorem HasFTaylorSeriesUpToOn.of_le

added theorem HasFTaylorSeriesUpToOn.shift_of_succ

added theorem HasFTaylorSeriesUpToOn.zero_eq'

added structure HasFTaylorSeriesUpToOn

added theorem contDiffAt_one_iff

added theorem contDiffAt_succ_iff_hasFDerivAt

added theorem contDiffAt_top

added theorem contDiffAt_zero

added theorem contDiffOn_all_iff_nat

added theorem contDiffOn_congr

added theorem contDiffOn_iff_continuousOn_differentiableOn

added theorem contDiffOn_iff_forall_nat_le

added theorem contDiffOn_of_continuousOn_differentiableOn

added theorem contDiffOn_of_differentiableOn

added theorem contDiffOn_of_locally_contDiffOn

added theorem contDiffOn_succ_iff_fderivWithin

added theorem contDiffOn_succ_iff_fderiv_of_open

added theorem contDiffOn_succ_iff_hasFDerivWithinAt

added theorem contDiffOn_succ_iff_has_fderiv_within

added theorem contDiffOn_succ_of_fderivWithin

added theorem contDiffOn_top

added theorem contDiffOn_top_iff_fderivWithin

added theorem contDiffOn_top_iff_fderiv_of_open

added theorem contDiffOn_univ

added theorem contDiffOn_zero

added theorem contDiffWithinAt_congr_nhds

added theorem contDiffWithinAt_iff_forall_nat_le

added theorem contDiffWithinAt_insert

added theorem contDiffWithinAt_inter'

added theorem contDiffWithinAt_inter

added theorem contDiffWithinAt_nat

added theorem contDiffWithinAt_succ_iff_hasFDerivWithinAt'

added theorem contDiffWithinAt_succ_iff_hasFDerivWithinAt

added theorem contDiffWithinAt_top

added theorem contDiffWithinAt_univ

added theorem contDiffWithinAt_zero

added theorem contDiff_all_iff_nat

added theorem contDiff_iff_contDiffAt

added theorem contDiff_iff_continuous_differentiable

added theorem contDiff_iff_forall_nat_le

added theorem contDiff_iff_ftaylorSeries

added theorem contDiff_of_differentiable_iteratedFDeriv

added theorem contDiff_one_iff_fderiv

added theorem contDiff_succ_iff_fderiv

added theorem contDiff_succ_iff_has_fderiv

added theorem contDiff_top

added theorem contDiff_top_iff_fderiv

added theorem contDiff_zero

added theorem fderiv_iteratedFDeriv

added def ftaylorSeries

added def ftaylorSeriesWithin

added theorem ftaylorSeriesWithin_univ

added theorem hasFTaylorSeriesUpToOn_succ_iff_left

added theorem hasFTaylorSeriesUpToOn_succ_iff_right

added theorem hasFTaylorSeriesUpToOn_top_iff'

added theorem hasFTaylorSeriesUpToOn_top_iff

added theorem hasFTaylorSeriesUpToOn_univ_iff

added theorem hasFTaylorSeriesUpToOn_zero_iff

added theorem hasFTaylorSeriesUpTo_succ_iff_right

added theorem hasFTaylorSeriesUpTo_top_iff'

added theorem hasFTaylorSeriesUpTo_top_iff

added theorem hasFTaylorSeriesUpTo_zero_iff

added theorem iteratedFDerivWithin_congr

added theorem iteratedFDerivWithin_congr_set

added theorem iteratedFDerivWithin_eventually_congr_set'

added theorem iteratedFDerivWithin_eventually_congr_set

added theorem iteratedFDerivWithin_inter'

added theorem iteratedFDerivWithin_inter

added theorem iteratedFDerivWithin_inter_open

added theorem iteratedFDerivWithin_of_isOpen

added theorem iteratedFDerivWithin_one_apply

added theorem iteratedFDerivWithin_succ_apply_left

added theorem iteratedFDerivWithin_succ_apply_right

added theorem iteratedFDerivWithin_succ_eq_comp_left

added theorem iteratedFDerivWithin_succ_eq_comp_right

added theorem iteratedFDerivWithin_univ

added theorem iteratedFDerivWithin_zero_apply

added theorem iteratedFDerivWithin_zero_eq_comp

added theorem iteratedFDeriv_one_apply

added theorem iteratedFDeriv_succ_apply_left

added theorem iteratedFDeriv_succ_apply_right

added theorem iteratedFDeriv_succ_eq_comp_left

added theorem iteratedFDeriv_succ_eq_comp_right

added theorem iteratedFDeriv_with_zero_eq

added theorem iteratedFDeriv_zero_apply

added theorem iteratedFDeriv_zero_eq_comp

added theorem norm_fderivWithin_iteratedFDerivWithin

added theorem norm_fderiv_iteratedFDeriv

added theorem norm_iteratedFDerivWithin_fderivWithin

added theorem norm_iteratedFDerivWithin_zero

added theorem norm_iteratedFDeriv_fderiv

added theorem norm_iteratedFDeriv_zero

Modified Mathlib/Analysis/Calculus/FormalMultilinearSeries.lean

Modified Mathlib/Analysis/NormedSpace/LinearIsometry.lean