Skip to content

[Merged by Bors] - feat(ContDiff): add iteratedFDeriv_comp#20472

Closed
urkud wants to merge 2 commits intomasterfrom
YK-iterfderiv-comp
Closed

[Merged by Bors] - feat(ContDiff): add iteratedFDeriv_comp#20472
urkud wants to merge 2 commits intomasterfrom
YK-iterfderiv-comp

Conversation

@urkud
Copy link
Copy Markdown
Member

@urkud urkud commented Jan 4, 2025

Open in Gitpod

@github-actions
Copy link
Copy Markdown

github-actions bot commented Jan 4, 2025 •
edited
Loading

PR summary 3437e1578c

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference

Declarations diff

+ ContDiffWithinAt.eventually_hasFTaylorSeriesUpToOn
+ iteratedFDerivWithin_comp
+ iteratedFDerivWithin_comp_of_eventually_mem
+ iteratedFDeriv_comp

You can run this locally as follows 
## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

No changes to technical debt.

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary
  • The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
  • The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

@github-actions github-actions bot added the t-analysis Analysis (normed *, calculus) label Jan 4, 2025
@urkud urkud requested a review from sgouezel January 4, 2025 19:39
@sgouezel
Copy link
Copy Markdown
Contributor

sgouezel commented Jan 7, 2025

bors r+

@ghost ghost added the ready-to-merge This PR has been sent to bors. label Jan 7, 2025
mathlib-bors bot pushed a commit that referenced this pull request Jan 7, 2025
@urkud
feat(ContDiff): add iteratedFDeriv_comp (#20472)
f100ec8
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Jan 7, 2025

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title feat(ContDiff): add iteratedFDeriv_comp [Merged by Bors] - feat(ContDiff): add iteratedFDeriv_comp Jan 7, 2025
@mathlib-bors mathlib-bors bot closed this Jan 7, 2025
@mathlib-bors mathlib-bors bot deleted the YK-iterfderiv-comp branch January 7, 2025 20:10
Julian added a commit that referenced this pull request Jan 8, 2025
@Julian
Merge remote-tracking branch 'origin/master' into emultiplicity-of-nat
53d4c08 
* origin/master: (642 commits)
  feat: the Boolean subalgebra generated by the lattice generated by a set (#20440)
  feat: misc. lemmas about moments, tilted measures (#20150)
  chore(Algebra/Lie): make IsNilpotent and IsSolvable independent of scalars (#20556)
  feat(Combinatorics/SimpleGraph/Path): add `IsPath.getVert_injOn` (#19373)
  feat(Combinatorics/SimpleGraph): add lemmas about `spanningCoe` (#19377)
  chore: scope 'on' notation to Function (#20562)
  chore: disable docPrime linter (#20559)
  chore: deprecate MulRingNorm._ in favour of AbsoluteValue._ (#20557)
  fix(scripts/bench_summary): input jobID as a Nat, rather than a String (#20539)
  chore: move results about `DivisionMonoid` + `HasDistribNeg` (#20551)
  feat(NumberTheory/NumberField/Embeddings): definition of totally real field (#20542)
  chore(Noetherian/Artinian): generalize to Semiring (#20534)
  chore: protect `Filter.nhds_{iInf,inf}` (#20530)
  chore(AlgebraicTopology): move SplitSimplicialObject.lean (#20511)
  chore: extract 3 new files out of MeasureSpace (#20509)
  feat(RingTheory): Jacobian criterion for smoothness of local algebras (#20326)
  doc(RingTheory/Flat): add reference to Lambek's paper (#20266)
  feat(NumberTheory/AbelSummation): add more results (#19942)
  chore(Multilinear/Basic): generalize the `SMul` instance (#20536)
  feat(FDeriv/Equiv): generalize `HasFDerivAt.of_local_left_inverse` (#20516)
  feat(ContDiff): add `iteratedFDeriv_comp` (#20472)
  feat(LowerUpperTopology): add lemmas (#20465)
  feat(ContDiff): weaken some assumptions (#20368)
  fix(scripts/technical-debt-metric): avoid division by 0 (#20537)
  chore(Algebra/Ring): Clean up in SumsOfSquares and Semireal/Defs (#20528)
  feat(FTaylorSeries): add lemmas about `dist` between 0th and 1st derivs (#20089)
  feat: results on inner regularity of finite measures (#19780)
  chore: to_additive various results on groups, group actions (#20547)
  feat(Probability/Kernel): `Kernel.sectL` and `sectR` (#15466)
  chore(CategoryTheory/Limits/Fubini): relax universes constraints and weaken hypotheses (#20553)
  perf: remove `@[simp]` on `Fintype.card_of{IsEmpty,Subsingleton}` (#20524)
  fix(HashCommandLinter): remove unnecessary, broken workaround for tests (#20529)
  chore(Ideal/Basic): dependent generalization of `Ideal.pi` (#20535)
  feat(RingTheory): being unramified is a local property (#20323)
  chore(BooleanSubalgebra): use `IsSublattice` in `closure_sdiff_sup_induction` (#20439)
  feat(Order/SuccPred/CompleteLinearOrder): `⨆ a < x, succ a = x` (#19970)
  chore(*): replace `no_index (ofNat n)` with `ofNat(n)` everywhere (#20521)
  feat(CategoryTheory/Triangulated/Adjunction): the right adjoint of a triangulated functor is triangulated (#20255)
  chore(Order/SuccPred/LinearLocallyFinite): change data-creating instances to defs (#20235)
  chore: don't import algebra in `Data.Finset.Basic` (#19779)
  feat: initial segment commutes with `Iio` (#20503)
  chore(Measure/Pi): move parts to `MeasurableSpace/` (#20215)
  chore: smile more often (#20436)
  chore(Algebra/Category/MonCat/ForgetCorepresentable, Algebra/Group/Equiv/Basic): move definitions and add symmetric version (#20416)
  feat(GroupTheory/QuotientGroup): group correspondence theorem (#20007)
  doc: change "module homomorphism" to "linear map" (#20481)
  perf: improves the performance of the `Repr (Equiv.Perm α)` instance (1/4) (#20519)
  fix: do not keep only the first line of hints (#19756)
  feat(Analysis/Analytic): lemmas about `smul` for power series (#19816)
  chore: don't import algebra in `Data.Multiset.Basic` (#19775)
  ...
Julian added a commit that referenced this pull request Jan 8, 2025
@Julian
Merge remote-tracking branch 'origin/master' into bhargava-factorial
0ae6406 
* origin/master: (80 commits)
  chore(CategoryTheory): remove data produced by tactic block (#20565)
  feat: `|∫ a, f a ∂μ| ≤ ∫ a, |f a| ∂μ` (#20540)
  feat: the Boolean subalgebra generated by the lattice generated by a set (#20440)
  feat: misc. lemmas about moments, tilted measures (#20150)
  chore(Algebra/Lie): make IsNilpotent and IsSolvable independent of scalars (#20556)
  feat(Combinatorics/SimpleGraph/Path): add `IsPath.getVert_injOn` (#19373)
  feat(Combinatorics/SimpleGraph): add lemmas about `spanningCoe` (#19377)
  chore: scope 'on' notation to Function (#20562)
  chore: disable docPrime linter (#20559)
  chore: deprecate MulRingNorm._ in favour of AbsoluteValue._ (#20557)
  fix(scripts/bench_summary): input jobID as a Nat, rather than a String (#20539)
  chore: move results about `DivisionMonoid` + `HasDistribNeg` (#20551)
  feat(NumberTheory/NumberField/Embeddings): definition of totally real field (#20542)
  chore(Noetherian/Artinian): generalize to Semiring (#20534)
  chore: protect `Filter.nhds_{iInf,inf}` (#20530)
  chore(AlgebraicTopology): move SplitSimplicialObject.lean (#20511)
  chore: extract 3 new files out of MeasureSpace (#20509)
  feat(RingTheory): Jacobian criterion for smoothness of local algebras (#20326)
  doc(RingTheory/Flat): add reference to Lambek's paper (#20266)
  feat(NumberTheory/AbelSummation): add more results (#19942)
  chore(Multilinear/Basic): generalize the `SMul` instance (#20536)
  feat(FDeriv/Equiv): generalize `HasFDerivAt.of_local_left_inverse` (#20516)
  feat(ContDiff): add `iteratedFDeriv_comp` (#20472)
  feat(LowerUpperTopology): add lemmas (#20465)
  feat(ContDiff): weaken some assumptions (#20368)
  fix(scripts/technical-debt-metric): avoid division by 0 (#20537)
  chore(Algebra/Ring): Clean up in SumsOfSquares and Semireal/Defs (#20528)
  feat(FTaylorSeries): add lemmas about `dist` between 0th and 1st derivs (#20089)
  feat: results on inner regularity of finite measures (#19780)
  chore: to_additive various results on groups, group actions (#20547)
  feat(Probability/Kernel): `Kernel.sectL` and `sectR` (#15466)
  chore(CategoryTheory/Limits/Fubini): relax universes constraints and weaken hypotheses (#20553)
  perf: remove `@[simp]` on `Fintype.card_of{IsEmpty,Subsingleton}` (#20524)
  fix(HashCommandLinter): remove unnecessary, broken workaround for tests (#20529)
  chore(Ideal/Basic): dependent generalization of `Ideal.pi` (#20535)
  feat(RingTheory): being unramified is a local property (#20323)
  chore(BooleanSubalgebra): use `IsSublattice` in `closure_sdiff_sup_induction` (#20439)
  feat(Order/SuccPred/CompleteLinearOrder): `⨆ a < x, succ a = x` (#19970)
  chore(*): replace `no_index (ofNat n)` with `ofNat(n)` everywhere (#20521)
  feat(CategoryTheory/Triangulated/Adjunction): the right adjoint of a triangulated functor is triangulated (#20255)
  chore(Order/SuccPred/LinearLocallyFinite): change data-creating instances to defs (#20235)
  chore: don't import algebra in `Data.Finset.Basic` (#19779)
  feat: initial segment commutes with `Iio` (#20503)
  chore(Measure/Pi): move parts to `MeasurableSpace/` (#20215)
  chore: smile more often (#20436)
  chore(Algebra/Category/MonCat/ForgetCorepresentable, Algebra/Group/Equiv/Basic): move definitions and add symmetric version (#20416)
  feat(GroupTheory/QuotientGroup): group correspondence theorem (#20007)
  doc: change "module homomorphism" to "linear map" (#20481)
  perf: improves the performance of the `Repr (Equiv.Perm α)` instance (1/4) (#20519)
  fix: do not keep only the first line of hints (#19756)
  ...
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@sgouezel sgouezel Awaiting requested review from sgouezel

Assignees

No one assigned

Labels

ready-to-merge This PR has been sent to bors. t-analysis Analysis (normed *, calculus)

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

2 participants

@urkud @sgouezel