Skip to content

Commit

Permalink
powere_pos lemmas
Browse files Browse the repository at this point in the history
- refactoring by Cyril

Co-authored-by: Alessandro Bruni <[email protected]>
Co-authored-by: Cyril Cohen <[email protected]>
  • Loading branch information
3 people authored and proux01 committed Jul 6, 2023
1 parent 46f8489 commit a961322
Show file tree
Hide file tree
Showing 3 changed files with 280 additions and 230 deletions.
74 changes: 67 additions & 7 deletions CHANGELOG_UNRELEASED.md
Original file line number Diff line number Diff line change
Expand Up @@ -28,11 +28,11 @@
`ae_pointwise_almost_uniform`.

- in `exp.v`:
+ lemmas `power_posrM`, `gt0_ler_power_pos`,
`gt0_power_pos`, `norm_power_pos`, `lt0_norm_power_pos`,
`power_posB`
+ lemmas `powere_posrM`, `powere_posAC`, `gt0_powere_pos`,
`powere_pos_eqy`, `eqy_powere_pos`, `powere_posD`, `powere_posB`
+ lemmas `powRrM`, `gt0_ler_powR`,
`gt0_powR`, `norm_powR`, `lt0_norm_powR`,
`powRB`
+ lemmas `poweRrM`, `poweRAC`, `gt0_poweR`,
`poweR_eqy`, `eqy_poweR`, `poweRD`, `poweRB`

- in `mathcomp_extra.v`:
+ definition `min_fun`, notation `\min`
Expand All @@ -41,6 +41,14 @@
- in `lebesgue_measure.v`:
+ lemmas `measurable_fun_ltr`, `measurable_minr`

- in `exp.v`:
+ notation `` e `^?(r +? s) ``
+ lemmas `expR_eq0`, `powRN`
+ definition `poweRD_def`
+ lemmas `poweRD_defE`, `poweRB_defE`, `add_neq0_poweRD_def`,
`add_neq0_poweRB_def`, `nneg_neq0_poweRD_def`, `nneg_neq0_poweRB_def`
+ lemmas `powR_eq0`, `poweR_eq0`

### Changed

- moved from `lebesgue_measure.v` to `real_interval.v`:
Expand All @@ -49,20 +57,72 @@

- moved from `functions.v` to `classical_sets.v`: `subsetP`.

- in `exp.v`:
+ lemmas `power_posD` (now `powRD`), `power_posB` (now `powRB`)

### Renamed

- in `boolp.v`:
+ `mextentionality` -> `mextensionality`
+ `extentionality` -> `extensionality`

- in `exp.v`:
+ `expK` -> `expRK`

- in `exp.v`:
+ `power_pos_eq0` -> `powR_eq0_eq0`
+ `power_pos_inv` -> `powR_invn`
+ `powere_pos_eq0` -> `poweR_eq0_eq0`

- in `exp.v`:
+ `power_pos` -> `powR`
+ `power_pos_ge0` -> `powR_ge0`
+ `power_pos_gt0` -> `powR_gt0`
+ `gt0_power_pos` -> `gt0_powR`
+ `power_pos0` -> `powR0`
+ `power_posr1` -> `powRr1`
+ `power_posr0` -> `powRr0`
+ `power_pos1` -> `powR1`
+ `ler_power_pos` -> `ler_powR`
+ `gt0_ler_power_pos` -> `gt0_ler_powR`
+ `power_posM` -> `powRM`
+ `power_posrM` -> `powRrM`
+ `power_posAC` -> `powRAC`
+ `power_posD` -> `powRD`
+ `power_posN` -> `powRN`
+ `power_posB` -> `powRB`
+ `power_pos_mulrn` -> `powR_mulrn`
+ `power_pos_inv1` -> `powR_inv1`
+ `power_pos_intmul` -> `powR_intmul`
+ `ln_power_pos` -> `ln_powR`
+ `power12_sqrt` -> `powR12_sqrt`
+ `norm_power_pos` -> `norm_powR`
+ `lt0_norm_power_pos` -> `lt0_norm_powR`

- in `lebesgue_measure.v`:
+ `measurable_power_pos` -> `measurable_powR`

- in `exp.v`:
+ `powere_pos` -> `poweR`
+ `powere_pos_EFin` -> `poweR_EFin`
+ `powere_posyr` -> `poweRyr`
+ `powere_pose0` -> `poweRe0`
+ `powere_pose1` -> `poweRe1`
+ `powere_posNyr` -> `poweRNyr`
+ `powere_pos0r` -> `poweR0r`
+ `powere_pos1r` -> `poweR1r`
+ `fine_powere_pos` -> `fine_poweR`
+ `powere_pos_ge0` -> `poweR_ge0`
+ `powere_pos_gt0` -> `poweR_gt0`
+ `powere_posM` -> `poweRM`
+ `powere12_sqrt` -> `poweR12_sqrt`

### Generalized

- in `exp.v`:
+ lemmas `convex_expR`, `ler_power_pos`
+ lemmas `convex_expR`, `ler_power_pos` (now `ler_powR`)
- in `exp.v`:
+ lemma `ln_power_pos`
+ lemma `ln_power_pos` (now `ln_powR`)

### Deprecated

Expand Down
Loading

0 comments on commit a961322

Please sign in to comment.