Skip to content

[Merged by Bors] - chore: rename set_lintegral to setLIntegral throughout mathlib#14260

Closed
sgouezel wants to merge 3 commits intomasterfrom
SG_set_lintegral
Closed

[Merged by Bors] - chore: rename set_lintegral to setLIntegral throughout mathlib#14260
sgouezel wants to merge 3 commits intomasterfrom
SG_set_lintegral

Conversation

@sgouezel
Copy link
Copy Markdown
Contributor

@sgouezel sgouezel commented Jun 29, 2024

The old naming is a remnant of Lean 3. The change has already been made for the Bochner integral, from set_integral to setIntegral.

Open in Gitpod

@sgouezel sgouezel added awaiting-review t-measure-probability Measure theory / Probability theory labels Jun 29, 2024
@github-actions
Copy link
Copy Markdown

github-actions bot commented Jun 29, 2024

PR summary e4aec2e5a8

Import changes

No significant changes to the import graph

Declarations diff

+ AEMeasurable.ae_eq_of_forall_setLIntegral_eq
+ IntegrableOn.setLIntegral_lt_top
+ IsCondKernelCDF.setLIntegral
+ MeasurePreserving.setLIntegral_comp_emb
+ MeasurePreserving.setLIntegral_comp_preimage
+ MeasurePreserving.setLIntegral_comp_preimage_emb
+ _root_.Measurable.setLIntegral_kernel
+ _root_.Measurable.setLIntegral_kernel_prod_left
+ _root_.Measurable.setLIntegral_kernel_prod_right
+ ae_eq_of_forall_setLIntegral_eq_of_sigmaFinite
+ ae_eq_of_forall_setLIntegral_eq_of_sigmaFinite₀
+ ae_le_of_forall_setLIntegral_le_of_sigmaFinite
+ ae_le_of_forall_setLIntegral_le_of_sigmaFinite₀
+ exists_pos_setLIntegral_lt_of_measure_lt
+ map_eq_setLIntegral_pdf
+ setLIntegral_compProd_univ_left
+ setLIntegral_compProd_univ_right
+ setLIntegral_condCDF
+ setLIntegral_condDistrib_of_measurableSet
+ setLIntegral_congr
+ setLIntegral_congr_fun
+ setLIntegral_const_lt_top
+ setLIntegral_density
+ setLIntegral_deterministic
+ setLIntegral_deterministic'
+ setLIntegral_dirac
+ setLIntegral_dirac'
+ setLIntegral_empty
+ setLIntegral_eq
+ setLIntegral_eq_const
+ setLIntegral_eq_tsum
+ setLIntegral_eq_tsum'
+ setLIntegral_le_lintegral
+ setLIntegral_lt_top_of_bddAbove
+ setLIntegral_lt_top_of_isCompact
+ setLIntegral_map
+ setLIntegral_max
+ setLIntegral_measure_zero
+ setLIntegral_mono
+ setLIntegral_mono'
+ setLIntegral_mono_ae
+ setLIntegral_mono_ae'
+ setLIntegral_nnnorm_condexpIndSMul_le
+ setLIntegral_nnnorm_condexpL2_indicator_le
+ setLIntegral_one
+ setLIntegral_pdf_le_map
+ setLIntegral_piecewise
+ setLIntegral_preCDF_fst
+ setLIntegral_preimage_condDistrib
+ setLIntegral_restrict
+ setLIntegral_rnDeriv
+ setLIntegral_rnDeriv'
+ setLIntegral_rnDerivAux
+ setLIntegral_rnDeriv_le
+ setLIntegral_rnDeriv_mul
+ setLIntegral_smul_measure
+ setLIntegral_stieltjesOfMeasurableRat
+ setLIntegral_stieltjesOfMeasurableRat_rat
+ setLIntegral_strict_mono
+ setLIntegral_subtype
+ setLIntegral_tilted
+ setLIntegral_tilted'
+ setLIntegral_toKernel_Iic
+ setLIntegral_toKernel_prod
+ setLIntegral_toKernel_univ
+ setLIntegral_univ
+ setLIntegral_withDensity_eq_lintegral_mul₀
+ setLIntegral_withDensity_eq_lintegral_mul₀'
+ setLIntegral_withDensity_eq_setLIntegral_mul
+ setLIntegral_withDensity_eq_setLIntegral_mul_non_measurable
+ setLIntegral_withDensity_eq_setLIntegral_mul_non_measurable₀
+ setLIntegral_withDensity_eq_setLIntegral_mul_non_measurable₀'
+ tendsto_setLIntegral_zero
++ setLIntegral_compProd
++ setLIntegral_condKernel
++ setLIntegral_condKernel_eq_measure_prod
++ setLIntegral_condKernel_univ_left
++ setLIntegral_condKernel_univ_right
++ setLIntegral_const
++-- set_lintegral_compProd
++-- set_lintegral_condKernel
++-- set_lintegral_condKernel_eq_measure_prod
++-- set_lintegral_condKernel_univ_left
++-- set_lintegral_condKernel_univ_right
++-- set_lintegral_const

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

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

@sgouezel sgouezel mentioned this pull request Jun 29, 2024
Closed
2 tasks
@RemyDegenne
Copy link
Copy Markdown
Contributor

RemyDegenne commented Jun 29, 2024

Thanks!
bors r+

@github-actions github-actions bot added ready-to-merge This PR has been sent to bors. and removed awaiting-review labels Jun 29, 2024
mathlib-bors bot pushed a commit that referenced this pull request Jun 29, 2024
@sgouezel
chore: rename set_lintegral to setLIntegral throughout mathlib (#14260)
85d5f96 
The old naming is a remnant of Lean 3. The change has already been made for the Bochner integral, from `set_integral` to `setIntegral`.
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Jun 29, 2024

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title chore: rename set_lintegral to setLIntegral throughout mathlib [Merged by Bors] - chore: rename set_lintegral to setLIntegral throughout mathlib Jun 29, 2024
@mathlib-bors mathlib-bors bot closed this Jun 29, 2024
@mathlib-bors mathlib-bors bot deleted the SG_set_lintegral branch June 29, 2024 15:42
dagurtomas pushed a commit that referenced this pull request Jul 2, 2024
@sgouezel @dagurtomas
chore: rename set_lintegral to setLIntegral throughout mathlib (#14260)
2d7fb97 
The old naming is a remnant of Lean 3. The change has already been made for the Bochner integral, from `set_integral` to `setIntegral`.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

No reviews

Assignees

No one assigned

Labels

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

@sgouezel @RemyDegenne