Skip to content

[Merged by Bors] - feat(Probability): first two derivatives of cgf#21223

Closed
RemyDegenne wants to merge 6 commits intomasterfrom
RD_cgfDeriv
Closed

[Merged by Bors] - feat(Probability): first two derivatives of cgf#21223
RemyDegenne wants to merge 6 commits intomasterfrom
RD_cgfDeriv

Conversation

@RemyDegenne
Copy link
Copy Markdown
Contributor

@RemyDegenne RemyDegenne commented Jan 29, 2025

Open in Gitpod

@RemyDegenne RemyDegenne added the t-measure-probability Measure theory / Probability theory label Jan 29, 2025
@github-actions
Copy link
Copy Markdown

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

PR summary 61c2bf4b3d

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference

Declarations diff

+ AnalyticAt.log
+ AnalyticOn.log
+ AnalyticOnNhd.log
+ AnalyticWithinAt.log
+ analyticAt_cgf
+ analyticAt_iteratedDeriv_mgf
+ analyticAt_log
+ analyticOnNhd_cgf
+ analyticOnNhd_iteratedDeriv_mgf
+ analyticOnNhd_log
+ analyticOn_cgf
+ analyticOn_iteratedDeriv_mgf
+ analyticOn_log
+ deriv_cgf
+ deriv_cgf_zero
+ differentiableAt_iteratedDeriv_mgf
+ differentiableAt_mgf
+ iteratedDeriv_two_cgf
+ iteratedDeriv_two_cgf_eq_integral

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).

@RemyDegenne RemyDegenne mentioned this pull request Jan 30, 2025
Closed
1 task
sgouezel
sgouezel reviewed Jan 31, 2025
View reviewed changes
@sgouezel sgouezel added the awaiting-author A reviewer has asked the author a question or requested changes. label Jan 31, 2025
@RemyDegenne RemyDegenne removed the awaiting-author A reviewer has asked the author a question or requested changes. label Jan 31, 2025
@RemyDegenne RemyDegenne mentioned this pull request Feb 3, 2025
Closed
1 task
sgouezel
sgouezel reviewed Feb 5, 2025
View reviewed changes
Copy link
Copy Markdown
Contributor

@sgouezel sgouezel left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

bors d+
Thanks!

@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Feb 5, 2025

✌️ RemyDegenne can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

@ghost ghost added the delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). label Feb 5, 2025
@RemyDegenne
Copy link
Copy Markdown
Contributor Author

RemyDegenne commented Feb 5, 2025

bors r+

@ghost ghost added the ready-to-merge This PR has been sent to bors. label Feb 5, 2025
mathlib-bors bot pushed a commit that referenced this pull request Feb 5, 2025
@RemyDegenne
feat(Probability): first two derivatives of cgf (#21223)
ad7930c
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Feb 5, 2025

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title feat(Probability): first two derivatives of cgf [Merged by Bors] - feat(Probability): first two derivatives of cgf Feb 5, 2025
@mathlib-bors mathlib-bors bot closed this Feb 5, 2025
@mathlib-bors mathlib-bors bot deleted the RD_cgfDeriv branch February 5, 2025 11:48
Julian added a commit that referenced this pull request Feb 5, 2025
@Julian
Merge remote-tracking branch 'origin/master' into bhargava-factorial
ae1775b 
* origin/master: (103 commits)
  chore(PresheafedSpace): remove `mk_coe` and some comments from porting  (#21382)
  refactor(CategoryTheory): `ConcreteCategory` instance for `FintypeCat` (#21466)
  refactor(Algebra/Category): clean up remaining uses of `HasForget` (#21460)
  chore(Algebra/Field/Basic): make some arguments implicit (#21453)
  chore(LinearAlgebra/TensorProduct): upgrade `TensorProduct.prodRight` (#21432)
  docs(Logic/Function/Defs): missing backticks (#21459)
  style(Logic/Embedding/Set): unindent (#21457)
  doc: document design choice of (AE)StronglyMeasurable.enorm and `edist` (#21423)
  perf(RingTheory/Artinian): reorder arguments in `IsArtinianRing.isMaximal_of_isPrime` (#21449)
  feat(Probability): first two derivatives of `cgf` (#21223)
  feat(RingTheory): `Ring.KrullDimLE` type class (#21452)
  chore(Probability/ProbabilityMassFunction/Binomial): typo "bernoulli" (#21455)
  chore: remove unused argument (#21393)
  feat(MeasureTheory/Integral/RieszMarkovKakutani) prove that the Riesz content is regular and define the Riesz measure (#20040)
  chore(Topology/Algebra/ContinuousMonoidHom): do not depend on `ContinuousLinearMap` (#21443)
  doc(CategoryTheory/Monoidal/Category): fix expression in docs (#21445)
  refactor(Order/CompleteBooleanAlgebra): a complete lattice which is a Heyting algebra is automatically a frame (#21391)
  chore: cleanup porting notes in TuringMachine (#20821)
  chore: remove @[simp] when the discr_key is a lambda (#21395)
  feat/doc: split files, add documentation (#21421)
  feat(Data/Set/Lattice): iUnion + insertion  (#21322)
  feat(Factorial): k! divides the product of any k successive integers (#21332)
  feat(CI): bench-after-CI (#21414)
  feat: primitive group actions (#12052)
  feat(Algebra/GroupWithZero/Int): add lemmas about Zm0 (#21370)
  feat(CategoryTheory): small classes of morphisms (#21411)
  feat(CategoryTheory): (co)limits of constant functors (#21412)
  chore: rename isUnit_ofPowEqOne (#21407)
  chore: split mapDomain out of MonoidAlgebra.Defs (#21398)
  chore: generalise lemmas to `ENorm` spaces, part 1 (#21380)
  chore: add `simp` to `Setoid.refl` (#21107)
  chore: tidy various files (#21406)
  chore(Geometry/Manifold/IsManifold): split out material on extended charts (#21219)
  refactor: introduce `Ideal.IsTwoSided` class for quotients of noncommutative rings (#17930)
  chore(Algebra/Category/ModuleCat): delete `ModuleCat.hasForgetModuleCat` (#21425)
  feat(RingTheory): unramified iff `κ(q)/κ(p)` is separable and `pS_q = qS_q` (#20690)
  doc(Order/Heyting/Basic): Coheyting difference is not right adjoint but left adjoint (#21418)
  chore: move ProofWidgets to v0.0.51 (#21416)
  chore: rename mem_nonZeroDivisor_of_injective and comap_nonZeroDivisor_le_of_injective (#21408)
  feat: drop ordering assumption in `RootPairing.coxeterWeight_mem_set_of_isCrystallographic` (#21122)
  feat(AlgebraicGeometry): the diagonal of an unramified morphism is an open immersion (#21386)
  feat(Data/LinearIndependent): iff versions of smul action on independent sets (#21383)
  chore(Combinatorics/SimpleGraph): Fix `hadj` naming (#21389)
  chore: rename AnalyticAt.order_neq_top_iff (#21388)
  fix: bug in daily.yml (#21401)
  chore: remove `@[simp]` from `CategoryTheory.Discrete.functor_map` (#21392)
  chore(Algebra/PUnitInstances): generalise universes (#21381)
  feat(RingTheory/PowerSeries): describe when power series map is zero (#21379)
  feat(Tactic/Linter): options to in/exclude definitions and private decls (#21374)
  feat: the prime spectrum is quasi-separated (#21362)
  ...
pfaffelh pushed a commit that referenced this pull request Feb 7, 2025
@RemyDegenne
feat(Probability): first two derivatives of cgf (#21223)
ca3a6fe
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@sgouezel sgouezel sgouezel left review comments

Assignees

No one assigned

Labels

delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). ready-to-merge This PR has been sent to bors. t-measure-probability Measure theory / Probability theory

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

2 participants

@RemyDegenne @sgouezel