Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Radon-Nikodym chain rule #1083

Merged
merged 13 commits into from
Jan 6, 2024
44 changes: 44 additions & 0 deletions CHANGELOG_UNRELEASED.md
Original file line number Diff line number Diff line change
Expand Up @@ -56,6 +56,34 @@
- in file `measure.v`
+ add lemmas `ae_eq_subset`, `measure_dominates_ae_eq`.

- in `charge.v`
+ definition `charge_of_finite_measure` (instance of `charge`)
+ lemmas `dominates_cscalel`, `dominates_cscaler`
+ definition `cpushforward` (instance of `charge`)
+ lemma `dominates_pushforward`
+ lemma `cjordan_posE`
+ lemma `jordan_posE`
+ lemma `cjordan_negE`
+ lemma `jordan_negE`
+ lemma `Radon_Nikodym_sigma_finite`
+ lemma `Radon_Nikodym_fin_num`
+ lemma `Radon_Nikodym_integral`
+ lemma `ae_eq_Radon_Nikodym_SigmaFinite`
+ lemma `Radon_Nikodym_change_of_variables`
+ lemma `Radon_Nikodym_cscale`
+ lemma `Radon_Nikodym_cadd`
+ lemma `Radon_Nikodym_chain_rule`

- in `sequences.v`:
+ lemma `minr_cvg_0_cvg_0`
+ lemma `mine_cvg_0_cvg_fin_num`
+ lemma `mine_cvg_minr_cvg`
+ lemma `mine_cvg_0_cvg_0`
+ lemma `maxr_cvg_0_cvg_0`
+ lemma `maxe_cvg_0_cvg_fin_num`
+ lemma `maxe_cvg_maxr_cvg`
+ lemma `maxe_cvg_0_cvg_0`
affeldt-aist marked this conversation as resolved.
Show resolved Hide resolved

### Changed

- in `normedtype.v`:
Expand All @@ -76,15 +104,31 @@
`ae_eq_mul1l`,
`ae_eq_abse`

- in `charge.v`
+ definition `jordan_decomp` now uses `cadd` and `cscale`
+ definition `Radon_Nikodym_SigmaFinite` now in a module `Radon_Nikodym_SigmaFinite` with
* definition `f`
* lemmas `f_ge0`, `f_fin_num`, `f_integrable`, `f_integral`
* lemma `change_of_variables`
* lemma `integralM`
* lemma `chain_rule`

- in `sequences.v`:
+ change the implicit arguments of `trivIset_seqDU`

### Renamed

- in `exp.v`:
+ `lnX` -> `lnXn`
- in `charge.v`:
+ `dominates_caddl` -> `dominates_cadd`

### Generalized

- in `lebesgue_integral.v`
+ `ge0_integral_bigsetU` generalized from `nat` to `eqType`
- in `lebesgue_measure.v`
+ an hypothesis of lemma `integral_ae_eq` is weakened
affeldt-aist marked this conversation as resolved.
Show resolved Hide resolved

### Deprecated

Expand Down
Loading
Loading