instead of lspace_master

CHANGELOG_UNRELEASED.md

@@ -88,6 +88,55 @@
   + lemmas `ess_infr_bounded`, `ess_infrZl`, `ess_inf_ger`, `ess_inf_ler`,
     `ess_inf_cstr`
 
+- in `simple_functions.v`:
+  + lemma `mfunMn`
+
+- in `hoelder.v`
+  + lemmas `Lnorm0`, `Lnorm_cst1`
+  + definition `hoelder_conjugate`
+  + lemmas `hoelder_conjugate0`, `hoelder_conjugate1`, `hoelder_conjugate2`,
+    `hoelder_conjugatey`, `hoelder_conjugateK`
+  + lemmas `lerB_DLnorm`, `lerB_LnormD`, `eminkowski`
+  + definition `finite_norm`
+  + mixin `isLfunction` with field `Lfunction_finite`
+  + structure `Lfunction`
+  + notation `LfunType`
+  + definition `Lequiv`
+  + canonical `Lequiv_canonical`
+  + definition `LspaceType`
+  + lemma `LequivP`
+  + record `LType`
+  + coercion `LfunType_of_LType`
+  + definition `Lspace` with notation `mu.-Lspace p`
+  + lemma `Lfun_integrable`, `Lfun1_integrable`, `Lfun2_integrable_sqr`, `Lfun2_mul_Lfun1`
+  + lemma `Lfun_scale`, `Lfun_cst`,
+  + definitions `finLfun`, `Lfun`, `Lfun_key`
+  + canonical `Lfun_keyed`
+  + lemmas `sub_Lfun_mfun`, `sub_Lfun_finLfun`
+  + definition `Lfun_Sub`
+  + lemmas `Lfun_rect`, `Lfun_valP`, `LfuneqP`, `finite_norm_cst0`, `mfunP`, `LfunP`,
+    `mfun_scaler_closed`
+  + lemmas `LnormZ`, `Lfun_submod_closed`
+  + lemmas `finite_norm_fine`, `ler_LnormD`,
+    `LnormrN`, `fine_Lnormr_eq0`
+  + lemma `fine_Lnormr_eq0`
+  + lemma `Lfun_subset`, `Lfun_subset12`
+  + lemma `Lfun_oppr_closed`
+  + lemma `Lfun_addr_closed`
+  + lemmas `poweR_Lnorm`, `oppe_Lnorm`
+  + lemma `integrable_poweR`
+
+- in `hoelder.v`:
+  + lemmas `hoelder_conjugate_div`, `hoelder_div_conjugate`,
+    `hoelder_Mconjugate`, `hoelder_conjugateP`,
+    `hoelder_conjugate_eq1`, `hoelder_conjugate_eqNy`, `hoelder_conjugate_eqy`,
+    `hoelder_conjugateNy`
+
+- in `constructive_ereal.v`:
+  + lemmas `div1e`, `divee`, `inve_eq1`, `Nyconjugate`
+
+### Changed
+
 - in `measure.v`:
   + notation `{ae mu, P}` (near use `{near _, _}` notation)
   + definition `ae_eq`
@@ -126,13 +175,27 @@
   + HB class `UniformZmodule` moved to `PreUniformZmodule`
   + HB class `UniformLmodule` moved to `PreUniformLmodule`
 
+- in `hoelder.v`:
+  + `minkowski` -> `minkowski_EFin`
 
 ### Generalized
 
 - in `derive.v`:
   + `derive_cst`, `derive1_cst`
 - in `convex.v`
   + parameter `R` of `convType` from `realDomainType` to `numDomainType`
+- in `hoelder.v`:
+  + definition `Lnorm` generalized to functions with codomain `\bar R`
+    (this impacts the notation `'N_p[f]`)
+  + lemmas `Lnorm1`, `eq_Lnorm`, `Lnorm_counting` (from `f : _ -> R` to `f : _ -> \bar R`)
+
+- in `probability.v`
+  + lemma `cantelli`
+  + lemmas `expectation_fin_num`, `expectationZl`, `expectationD`, `expectationB`, `expectation_sum`,
+    `covarianceE`, `covariance_fin_num`, `covarianceZl`, `covarianceZr`, `covarianceNl`,
+    `covarianceNr`, `covarianceNN`, `covarianceDl`, `covarianceDr`, `covarianceBl`, `covarianceBr`,
+     `varianceE`, `variance_fin_num`, `varianceZ`, `varianceN`, `varianceD`, `varianceB`,
+     `varianceD_cst_l`, `varianceD_cst_r`, `varianceB_cst_l`, `varianceB_cst_r`, `covariance_le`
 
 ### Deprecated
 

reals/constructive_ereal.v

@@ -2418,6 +2418,15 @@ Qed.
 Lemma inve_eq0 x : (x^-1 == 0) = (x == +oo).
 Proof. by case: inveP; rewrite ?eqxx //= => r /negPf; rewrite eqe invr_eq0. Qed.
 
+Lemma inve_eq1 x : (x^-1 == 1) = (x == 1).
+Proof.
+move: x => [x| |]/=.
+- rewrite inver; case: ifPn => [/eqP ->|x0]; last by rewrite !eqe invr_eq1.
+  by rewrite eqe// [RHS]eq_sym oner_eq0; apply/negbTE.
+- by rewrite invey eq_sym onee_eq0.
+- by rewrite inveNy.
+Qed.
+
 Lemma inve_ge0 x : (0 <= x^-1) = (0 <= x).
 Proof.
 by case: inveP; rewrite ?le0y ?lexx //= => r; rewrite lee_fin invr_ge0.
@@ -2452,6 +2461,13 @@ Proof.
 by move: x => [x| |]//; rewrite eqe => x0 _; rewrite inver (negbTE x0).
 Qed.
 
+Lemma div1e x : 1 / x = x^-1.
+Proof.
+move: x => [x| |]/=; first by rewrite mul1e.
+- by rewrite invey mule0.
+- by rewrite inveNy mul1e.
+Qed.
+
 Lemma gee_pMl y x : y \is a fin_num -> 0 <= x -> y <= 1 -> y * x <= x.
 Proof.
 move=> yfin; rewrite le_eqVlt => /predU1P[<-|]; first by rewrite mule0.
@@ -3478,6 +3494,41 @@ Proof. by move=> x0; rewrite inve_pgt ?inve1//= inE/= ?lee01. Qed.
 Lemma inve_ge1 x : 0 <= x -> (1 <= x^-1) = (x <= 1).
 Proof. by move=> x0; rewrite inve_pge ?inve1//= inE/= ?lee01. Qed.
 
+Lemma divee x : x \is a fin_num -> x != 0 -> x / x = 1.
+Proof.
+move: x => [x|//|//] _.
+by rewrite eqe => x0; rewrite inver (negbTE x0) -EFinM divff.
+Qed.
+
+Lemma Nyconjugate x y : x \is a fin_num -> y != -oo ->
+  x^-1 + y^-1 = 1 -> y = x / (x - 1).
+Proof.
+move=> xfin yNy; have [->|x1] := eqVneq x 1.
+  rewrite subee// inve0 mul1e inve1 => /eqP.
+  rewrite -addeC eq_sym -sube_eq//; last by rewrite fin_num_adde_defl.
+  rewrite subee// => /eqP /esym; case: y yNy => // r _.
+  rewrite inver; case: ifPn => // r0 [] /(congr1 (fun z => z^-1)%R).
+  by rewrite invrK invr0 => /eqP; rewrite (negbTE r0).
+have [->|x0] := eqVneq x 0.
+  rewrite inve0 mul0e => /eqP; rewrite addeC eq_sym -sube_eq//; last first.
+    rewrite /adde_def eqxx/= andbT negb_and/= orbT/=.
+    apply: contra yNy => /eqP /(congr1 inve).
+    by rewrite inveK inveNy => ->.
+  rewrite eq_sym/= addeC/= => /eqP /(congr1 inve).
+  by rewrite inveK// inveNy => /eqP; rewrite (negbTE yNy).
+have xNy : x != -oo by move: xfin; rewrite fin_numE => /andP[].
+move=> /eqP; rewrite eq_sym addeC -sube_eq//; last first.
+  by rewrite fin_num_adde_defl// fin_numV.
+move=> /eqP /(congr1 inve) /=; rewrite inveK => <-.
+rewrite -[X in X - _](@divee x)// -[X in _ - X]div1e -muleBl.
+- move: x xfin {xNy} x1 x0 => [x| |]// _; rewrite !eqe => x1 x0.
+  rewrite inver/= (negbTE x0)/= -EFinD -EFinM.
+  rewrite inver mulf_eq0 subr_eq0 (negbTE x1)/= invr_eq0.
+  by rewrite (negbTE x0) invfM// invrK mulrC EFinM inver/= subr_eq0 (negbTE x1).
+- by rewrite fin_numV// ?gt_eqF// ltNye.
+- by rewrite fin_num_adde_defl.
+Qed.
+
 Lemma lee_addgt0Pr x y :
   reflect (forall e, (0 < e)%R -> x <= y + e%:E) (x <= y).
 Proof.