Module mathcomp.analysis.lebesgue_integral_theory.lebesgue_integral_definition

From HB Require Import structures.
From mathcomp Require Import boot order ssralg ssrnum ssrint interval.
From mathcomp Require Import interval_inference finmap.
#[warning="-warn-library-file-internal-analysis"]
From mathcomp Require Import unstable.
From mathcomp Require Import mathcomp_extra boolp classical_sets functions.
From mathcomp Require Import cardinality reals fsbigop ereal topology tvs.
From mathcomp Require Import normedtype sequences real_interval esum measure.
From mathcomp Require Import lebesgue_measure numfun realfun simple_functions.
From mathcomp Require Import measurable_realfun.

# Definition of the Lebesgue integral This file contains the definition of the Lebesgue integral. It starts with the integral of simple functions, proves their basic properties (linearity, non-decreasingness, etc.), and then defines the integral of measurable functions. Main notations: | Coq notation | | Meaning | |----------------------:|--|:-------------------------------- | \int[mu]_(x in D) f x |==| $\int_D f(x)\mathbf{d}\mu(x)$ | \int[mu]_x f x |==| $\int f(x)\mathbf{d}\mu(x)$ Main reference: - Daniel Li, Intégration et applications, 2016 Detailed contents: ``` sintegral mu f == integral of the function f with the measure mu \int[mu]_(x in D) f x == integral of the measurable function f over the domain D with measure mu \int[mu]_x f x := \int[mu]_(x in setT) f x ```

Unset SsrOldRewriteGoalsOrder.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
Import Order.TTheory GRing.Theory Num.Theory.
Import numFieldNormedType.Exports.

Local Open Scope classical_set_scope.
Local Open Scope ring_scope.

Reserved Notation "\int [ mu ]_ ( i 'in' D ) F"
  (at level 36, F at level 36, i, D at level 60,
  format "'[' \int [ mu ]_ ( i 'in' D ) '/ ' F ']'").
Reserved Notation "\int [ mu ]_ i F"
  (F at level 36, i at level 0,
    right associativity, format "'[' \int [ mu ]_ i '/ ' F ']'").

Definition of simple integrals:

Section simple_fun_raw_integral.
Local Open Scope ereal_scope.
Variables ( : Type) ( : numDomainType) ( : set T -> \bar R) ( : T -> R).

Definition := \sum_( \in [set: R]) x%:E * mu (f @^-1` [set x]).

Lemma :
sintegral = \sum_( \in [set: R]) x%:E * mu (f @^-1` [set x]).

Proof.

by []. Qed.

End simple_fun_raw_integral.

#[global] Hint Extern 0 (is_true (0 <= _)) => solve [apply: measure_ge0] : core.

Section sintegral_lemmas.
Context ( : sigmaRingType d) ( : realType).
Variable : {measure set T -> \bar R}.
Local Open Scope ereal_scope.

Lemma :
sintegral mu f = \sum_( \in range f) x%:E * mu (f @^-1` [set x]).

Proof.

rewrite (fsbig_widen (range f) setT)//= => x [_ Nfx] /=.
by rewrite preimage10// measure0 mule0.
Qed.

Lemma : sintegral mu (cst 0%R) = 0.

Proof.

rewrite sintegralE fsbig1// => r _; rewrite preimage_cst.
by case: ifPn => [/[!inE] <-|]; rewrite ?mul0e// measure0 mule0.
Qed.

Import HBNNSimple.

Lemma ( : {nnsfun T >-> R}) : 0 <= sintegral mu f.

Proof.

by rewrite sintegralE fsume_ge0// => r _; exact: nnsfun_mulemu_ge0. Qed.

Lemma ( : set T) : sintegral mu \1_A = mu A.

Proof.

rewrite sintegralE (fsbig_widen _ [set 0%R; 1%R]) => //=.
- exact: image_indic_sub.
- by move=> t [[] -> /= /preimage10->]; rewrite measure0 mule0.
have N01 : (0 <> 1:> R)%R by apply/eqP; rewrite eq_sym oner_eq0.
rewrite fsbigU//=; first by move=> t [->].
rewrite !fsbig_set1 mul0e add0e mul1e.
by rewrite preimage_indic ifT ?inE// ifN ?notin_setE.
Qed.

Lemma ( : {nnsfun T >-> R}) : sintegral mu f =
\sum_( \in [set | r > 0]%R) x%:E * mu (f @^-1` [set x]).

Proof.

rewrite (fsbig_widen _ setT) ?sintegralET//.
move=> x [_ /=]; case: ltgtP => //= [xlt0 _|<-]; last by rewrite mul0e.
rewrite preimage10 ?measure0 ?mule0//= => -[t _ xE].
by apply/negP: xlt0; rewrite -leNgt -xE.
Qed.

End sintegral_lemmas.

Lemma ( : sigmaRingType d) ( : numDomainType)
( : set T -> \bar R) :
f =1 g -> sintegral mu f = sintegral mu g.

Proof.

by move=> /funext->. Qed.

Arguments eq_sintegral {d T R mu} g.

Section le_measure_sintegral.
Local Open Scope ereal_scope.
Context {} { : measurableType d} { : realType}.
Variables : {measure set T -> \bar R}.
Hypothesis : forall , measurable S -> m1 S <= m2 S.

Import HBNNSimple.
Import MeasurableR.

Lemma ( : {nnsfun T >-> R}) :
sintegral m1 f <= sintegral m2 f.

Proof.

by rewrite !sintegralE lee_fsum// => r [t _ <-]; rewrite lee_pmul ?lee_fin ?m12.
Qed.

End le_measure_sintegral.

Section sintegralrM.
Local Open Scope ereal_scope.
Context ( : sigmaRingType d) ( : realType).
Variables ( : {measure set T -> \bar R}) ( : R) ( : {nnsfun T >-> R}).

Import HBNNSimple.

Lemma : sintegral m (cst r \* f)%R = r%:E * sintegral m f.

Proof.

have [->|r0] := eqVneq r 0%R.
  by rewrite mul0e (eq_sintegral (cst 0%R)) ?sintegral0// => x/=; rewrite mul0r.
rewrite !sintegralET ge0_mule_fsumr.
  by move=> s ?; rewrite nnsfun_mulemu_ge0.
rewrite (reindex_fsbigT ( *%R r))/=.
  by exists ( *%R r^-1); [exact: mulKf|exact: mulVKf].
by apply: eq_fsbigr => x; rewrite preimage_cstM// [(_ / r)%R]mulrC mulKf// muleA.
Qed.

End sintegralrM.

Section sintegralD.
Local Open Scope ereal_scope.
Context ( : measurableType d) ( : realType).
Variables ( : {measure set T -> \bar R}).
Variables ( : set T) ( : measurable D) ( : {nnsfun T >-> R}).

Import HBNNSimple.
Import MeasurableR.

Lemma : sintegral m (f \+ g)%R = sintegral m f + sintegral m g.

Proof.

rewrite !sintegralE; set F := f @` _; set G := g @` _; set FG := _ @` _.
pose pf := f @^-1` [set x]; pose pg := g @^-1` [set y].
transitivity (\sum_( \in FG) z%:E * \sum_( \in F) m (pf a `&` pg (z - a)%R)).
  apply: eq_fsbigr => z _; rewrite preimageD1 -fsbig_setU// measure_fsbig//.
    by move=> x Fx; exact: measurableI.
  exact/trivIset_setIr/trivIset_preimage1.
under eq_fsbigr do rewrite ge0_mule_fsumr//; rewrite exchange_fsbig//=.
transitivity (\sum_( \in F) \sum_( \in G) (x + y)%:E * m (pf x `&` pg y)).
  apply: eq_fsbigr => x _; rewrite /pf /pg (fsbig_widen G setT)//=.
    by move=> y [_ /= /preimage10->]; rewrite setI0 measure0 mule0.
  rewrite (fsbig_widen FG setT)//=.
    move=> z [_ /= FGz]; rewrite [X in m X](_ : _ = set0) ?measure0 ?mule0//.
    rewrite -subset0 => //= {x}i /= [<-] /(canLR (@addrNK _ _)).
    by apply: contra_not FGz => <-; exists i; rewrite //= addrC.
  rewrite (reindex_fsbigT (+%R x))//=.
  by apply: eq_fsbigr => y; rewrite addrC addrK.
transitivity (\sum_( \in F) \sum_( \in G) x%:E * m (pf x `&` pg y) +
              \sum_( \in F) \sum_( \in G) y%:E * m (pf x `&` pg y)).
  do 2![rewrite -fsbig_split//; apply: eq_fsbigr => _ /set_mem [? _ <-]].
  by rewrite EFinD ge0_muleDl// ?lee_fin.
congr +%E; last rewrite exchange_fsbig//; apply: eq_fsbigr => x _.
  by rewrite -ge0_mule_fsumr// additive_nnsfunr nnsfun_cover setIT.
by rewrite -ge0_mule_fsumr// additive_nnsfunl nnsfun_cover setTI.
Qed.

End sintegralD.

Section le_sintegral.
Context ( : measurableType d) ( : realType) ( : {measure set T -> \bar R}).
Variables : {nnsfun T >-> R}.

Import HBNNSimple.

Hypothesis : forall , f x <= g x.

Let : @isNonNegFun T R (g \- f).

Proof.

by split=> x; rewrite subr_ge0 fg. Qed.

..

Lemma : (sintegral m f <= sintegral m g)%E.

Proof.

have gfgf : g =1 f \+ (g \- f) by move=> x /=; rewrite addrC subrK.
by rewrite (eq_sintegral _ _ gfgf) sintegralD// leeDl // sintegral_ge0.
Qed.

End le_sintegral.

Section is_cvg_sintegral.
Import HBNNSimple.

Lemma ( : measurableType d) ( : realType)
( : {measure set T -> \bar R}) ( : {nnsfun T >-> R}^nat) :
(forall , nondecreasing_seq (f ^~ x)) -> cvgn (sintegral m \o f).

Proof.

move=> nd_f; apply/cvg_ex; eexists; apply/ereal_nondecreasing_cvgn => a b ab.
by apply: le_sintegral => // => x; exact/nd_f.
Qed.

End is_cvg_sintegral.

Section sintegral_nondecreasing_limit_lemma.
Context ( : measurableType d) ( : realType).
Variable : {measure set T -> \bar R}.
Variables ( : {nnsfun T >-> R}^nat) ( : {nnsfun T >-> R}).

Import HBNNSimple.

Hypothesis : forall , nondecreasing_seq (g^~ x).
Hypothesis : forall , cvgn (g^~ x) -> f x <= limn (g^~ x).

Let : (set T)^nat := fun => [set | c * f x <= g n x].

Let : {homo fleg c : / (n <= m)%N >-> (n <= m)%O}.

Proof.

move=> n m nm; rewrite /fleg; apply/subsetPset => x /= cfg.
by move: cfg => /le_trans; apply; exact: nd_g.
Qed.

Import MeasurableR.

Let : measurable (fleg c n).

Proof.

rewrite /fleg [X in _ X](_ : _ = \big[setU/set0]_( <- fset_set (range f))
    \big[setU/set0]_( <- fset_set (range (g n)) | c * y <= x)
      (f @^-1` [set y] `&` (g n @^-1` [set x]))); last first.
  apply: bigsetU_measurable => r _; apply: bigsetU_measurable => r' crr'.
  exact/measurableI.
rewrite predeqE => t; split => [/= cfgn|].
- rewrite -bigcup_seq; exists (f t); first by rewrite /= in_fset_set//= mem_set.
  rewrite -bigcup_seq_cond; exists (g n t) => //=.
  by rewrite in_fset_set// mem_set.
- rewrite bigsetU_fset_set// => -[r [x _ fxr]].
  rewrite bigsetU_fset_set_cond// => -[r' [[x' _ gnx'r'] crr']].
  by rewrite /preimage/= => -[-> ->].
Qed.

Let : {nnsfun T >-> R} := proj_nnsfun f (mfleg c n).

Let : {homo (fun => g1 c p x): / (m <= n)%N >-> (m <= n)%O}.

Proof.

move=> m n mn; apply/asboolP => t; rewrite /g1/= ler_pM// 2!mindicE/= ler_nat.
have [|//] := boolP (t \in fleg c m); rewrite inE => cnt.
by have := nd_fleg c mn => /subsetPset/(_ _ cnt) cmt; rewrite mem_set.
Qed.

Let : c < 1 -> \bigcup_ fleg c n = setT.

Proof.

move=> c1; rewrite predeqE => x; split=> // _.
have := @fun_ge0 _ _ f x; rewrite le_eqVlt => /predU1P[|] gx0.
  by exists O => //; rewrite /fleg /=; rewrite -gx0 mulr0 fun_ge0.
have [cf|df] := pselect (cvgn (g^~ x)).
  have cfg : limn (g^~ x) > c * f x.
    by rewrite (lt_le_trans _ (gf cf)) // gtr_pMl.
  suff [n cfgn] : exists , g n x >= c * f x by exists n.
  move/(@lt_lim _ _ _ (nd_g x) cf) : cfg => [n _ nf].
  by exists n; apply: nf => /=.
have /cvgryPge/(_ (c * f x))[n _ ncfgn]:= nondecreasing_dvgn_lt (nd_g x) df.
by exists n => //; rewrite /fleg /=; apply: ncfgn => /=.
Qed.

Local Open Scope ereal_scope.

Lemma : sintegral mu f <= limn (sintegral mu \o g).

Proof.

suff ? : forall , (0 < c < 1)%R ->
    c%:E * sintegral mu f <= limn (sintegral mu \o g).
  by apply/lee_mul01Pr => //; exact: sintegral_ge0.
move=> c /andP[c0 c1].
have cg1g n : c%:E * sintegral mu (g1 c n) <= sintegral mu (g n).
  rewrite -sintegralrM (_ : (_ \* _)%R = scale_nnsfun (g1 c n) (ltW c0)) //.
  apply: le_sintegral => // t.
  suff : forall , (c * g1 c m x <= g m x)%R by move=> /(_ n t).
  move=> m x; rewrite /g1 /proj_nnsfun/= mindicE.
  by have [|] := boolP (_ \in _); [rewrite inE mulr1|rewrite 2!mulr0 fun_ge0].
suff {cg1g}<- : limn (fun => sintegral mu (g1 c n)) = sintegral mu f.
  have is_cvg_g1 : cvgn (fun => sintegral mu (g1 c n)).
    by apply: is_cvg_sintegral => //= x m n /(le_ffleg c)/lefP/(_ x).
  rewrite -limeMl // lee_lim//; first exact: is_cvgeZl.
  - by apply: is_cvg_sintegral => // m n mn; apply/lefP => t; apply: nd_g.
  - exact/nearW/cg1g.
suff : sintegral mu (g1 c n) @[ \oo] --> sintegral mu f by apply/cvg_lim.
rewrite [X in X @ \oo --> _](_ : _ = fun => \sum_( <- fset_set (range f))
    x%:E * mu (f @^-1` [set x] `&` fleg c n)).
  rewrite funeqE => n; rewrite sintegralE.
  transitivity (\sum_( \in range f) x%:E * mu (g1 c n @^-1` [set x])).
    apply: eq_fbigl => r.
    do 2 (rewrite in_finite_support; first exact/finite_setIl).
    apply/idP/idP.
      rewrite in_setI => /andP[]; rewrite inE/= => -[x _]; rewrite mindicE.
      have [_|xcn] := boolP (_ \in _).
        by rewrite mulr1 => <-; rewrite !inE/= => ?; split => //; exists x.
      by rewrite mulr0 => /esym ->; rewrite !inE/= mul0e.
    rewrite in_setI => /andP[]; rewrite inE => -[x _ <-].
    rewrite !inE/= => h; split=> //; move: h; rewrite mindicE => /eqP.
    rewrite mule_eq0 negb_or => /andP[_]; set S := (X in mu X) => mS0.
    suff : S !=set0 by move=> [y yx]; exists y.
    by apply/set0P; apply: contra mS0 => /eqP ->; rewrite measure0.
  rewrite fsbig_finite//=; apply: eq_fbigr => r.
  rewrite in_fset_set// inE => -[t _ ftr _].
  have [->|r0] := eqVneq r 0%R; first by rewrite 2!mul0e.
  congr (_ * mu _); apply/seteqP; split => x.
    rewrite /preimage/= mindicE.
    have [|_] := boolP (_ \in _); first by rewrite mulr1 inE.
    by rewrite mulr0 => /esym/eqP; rewrite (negbTE r0).
  by rewrite /preimage/= => -[fxr cnx]; rewrite mindicE mem_set// mulr1.
rewrite sintegralE fsbig_finite//=.
apply: cvg_nnesum=> [r _|r _].
  near=> A; apply: (mulemu_ge0 (fun => f @^-1` [set x] `&` fleg c A)) => r0.
  by rewrite preimage_nnfun0// set0I.
apply: cvgeZl => //=; rewrite [X in _ --> X](_ : _ =
    mu (\bigcup_ (f @^-1` [set r] `&` fleg c n))).
  by rewrite -setI_bigcupr bigcup_fleg// setIT.
have ? k i : measurable (f @^-1` [set k] `&` fleg c i) by exact: measurableI.
apply: nondecreasing_cvg_measure; [by []|exact: bigcupT_measurable|].
move=> n m nm; apply/subsetPset; apply: setIS.
by move/(nd_fleg c) : nm => /subsetPset.
Unshelve. all: by end_near. Qed.

End sintegral_nondecreasing_limit_lemma.

Section sintegral_nondecreasing_limit.
Context ( : measurableType d) ( : realType).
Variable : {measure set T -> \bar R}.
Variables ( : {nnsfun T >-> R}^nat) ( : {nnsfun T >-> R}).

Import HBNNSimple.

Hypothesis : forall , nondecreasing_seq (g^~ x).
Hypothesis : forall , g ^~ x @ \oo --> f x.

Let : limn (g^~ x) = f x.

Proof.

by apply/cvg_lim => //; exact: gf. Qed.

Lemma : sintegral mu f = limn (sintegral mu \o g).

Proof.

apply/eqP; rewrite eq_le; apply/andP; split.
by apply: nd_sintegral_lim_lemma => // x; rewrite -limg.
have : nondecreasing_seq (sintegral mu \o g).
by move=> m n mn; apply: le_sintegral => // x; exact/nd_g.
move=> /ereal_nondecreasing_cvgn/cvg_lim -> //.
apply: ge_ereal_sup => _ [n _ <-] /=; apply: le_sintegral => // x.
rewrite -limg // (nondecreasing_cvgn_le (nd_g x)) //.
by apply/cvg_ex; exists (f x); exact: gf.
Qed.

End sintegral_nondecreasing_limit.

Section integral.
Local Open Scope ereal_scope.
Context ( : measurableType d) ( : realType).
Implicit Types (f g : T -> \bar R) (D : set T).

Import HBNNSimple.

Let := ereal_sup [set sintegral mu h |
in [set : {nnsfun T >-> R} | forall , (h x)%:E <= f x]].

Definition ( := f \_ D) :=
nnintegral mu (g ^\+) - nnintegral mu (g ^\-).

Variable ( : {measure set T -> \bar R}).

Let : (forall , 0 <= f x) -> 0 <= nnintegral mu f.

Proof.

by move=> f0; apply: ereal_sup_ubound; exists nnsfun0 => //; exact: sintegral0.
Qed.

Let : f =1 g -> nnintegral mu f = nnintegral mu g.

Proof.

by move=> /funext->. Qed.

Let : nnintegral mu (cst 0) = 0.

Proof.

rewrite /nnintegral /=; apply/eqP; rewrite eq_le; apply/andP; split; last first.
by apply/ereal_sup_ubound; exists nnsfun0; [|exact: sintegral0].
apply/ge_ereal_sup => /= x [f /= f0 <-]; have {}f0 : forall , f x = 0%R.
by move=> y; apply/eqP; rewrite eq_le -2!lee_fin f0 //= lee_fin//.
by rewrite (eq_sintegral (@nnsfun0 _ T R)) ?sintegral0.
Qed.

Let ( : {nnsfun T >-> R}) :
nnintegral mu (EFin \o h) = sintegral mu h.

Proof.

apply/eqP; rewrite eq_le; apply/andP; split.
by apply/ge_ereal_sup => /= _ -[g /= gh <-]; rewrite le_sintegral.
by apply: ereal_sup_ubound => /=; exists h.
Qed.

Local Notation := (integral mu D (fun => F)%E)
  (at level 36, F at level 36, x, D at level 50,
  format "'[' \int_ ( x 'in' D ) '/ ' F ']'").

Lemma : {in D, f =1 g} ->
  \int_( in D) f x = \int_( in D) g x.

Proof.

by rewrite /integral => /eq_restrictP->. Qed.

Lemma : (forall , D x -> 0 <= f x) ->
\int_( in D) f x = nnintegral mu (f \_ D).

Proof.

move=> f0; rewrite /integral funeneg_restrict funepos_restrict.
have /eq_restrictP-> := ge0_funeposE f0.
have /eq_restrictP-> := ge0_funenegE f0.
by rewrite erestrict0 nnintegral0 sube0.
Qed.

Lemma : (forall , 0 <= f x) ->
\int_( in setT) f x = nnintegral mu f.

Proof.

by move=> f0; rewrite ge0_integralE// patch_setT. Qed.

Lemma :
\int_( in D) f x = \int_( in D) (f ^\+ x) - \int_( in D) f ^\- x.

Proof.

by rewrite [in LHS]/integral funepos_restrict funeneg_restrict -!ge0_integralE.
Qed.

Lemma : \int_( in D) cst 0 x = 0.

Proof.

by rewrite ge0_integralE// erestrict0 nnintegral0. Qed.

Lemma :
(forall , D x -> f x = 0) -> \int_( in D) f x = 0.

Proof.

move=> f0; under eq_integral; first by move=> x /[1!inE] /f0 ->; over.
by rewrite integral0.
Qed.

Lemma : (forall , D x -> 0 <= f x) -> 0 <= \int_( in D) f x.

Proof.

move=> f0; rewrite ge0_integralE// nnintegral_ge0// => x.
by rewrite /patch; case: ifP; rewrite // inE => /f0->.
Qed.

Lemma ( : measurable D) ( : {nnsfun T >-> R}) :
\int_( in D) (h x)%:E = sintegral mu (h \_ D).

Proof.

rewrite mrestrict -nnintegral_nnsfun// -mrestrict ge0_integralE ?comp_patch//.
by move=> x Dx /=; rewrite lee_fin; exact: fun_ge0.
Qed.

End integral.

Notation :=
  (integral mu D (fun => f)%E) : ereal_scope.
Notation :=
  ((integral mu setT (fun => f)%E))%E : ereal_scope.
Arguments eq_integral {d T R mu D} g.

Section ge0_le_measure_integral.
Local Open Scope ereal_scope.
Context {} { : measurableType d} { : realType}.
Variables : {measure set T -> \bar R}.
Hypothesis : forall , measurable S -> m1 S <= m2 S.

Import HBNNSimple.

Lemma ( : T -> \bar R) : measurable S ->
  (forall , 0 <= f x) -> measurable_fun [set: T] f ->
  \int[m1]_( in S) f x <= \int[m2]_( in S) f x.

Proof.

move=> ms f0 mf; rewrite !ge0_integralE //= ge_ereal_sup// => _ [h/= hfS] <-.
by apply: le_ereal_sup_tmp; exists (sintegral m2 h);
[exists h|exact: le_measure_sintegral].
Qed.

End ge0_le_measure_integral.

Section integral_indic.
Local Open Scope ereal_scope.
Context ( : measurableType d) ( : realType)
( : {measure set T -> \bar R}) ( : set T) ( : measurable D).
Implicit Type A : set T.

Import HBNNSimple.

Lemma : measurable A ->
\int[mu]_( in D) (\1_A x)%:E = mu (A `&` D).

Proof.

move=> mA; rewrite (_ : \1_A = indic_nnsfun R mA)// integral_nnsfun//=.
by rewrite restrict_indic sintegral_indic//; exact: measurableI.
Qed.

End integral_indic.

Section domain_change.
Local Open Scope ereal_scope.
Context {} { : measurableType d} { : realType}
( : {measure set T -> \bar R}).

Lemma : \int[mu]_( in D) f x = \int[mu]_ (f \_ D) x.

Proof.

by rewrite /integral patch_setT. Qed.

Import HBNNSimple.

Lemma ( : {nnsfun T >-> R}) :
\int[mu]_ (h x)%:E = sintegral mu h.

Proof.

by rewrite integral_nnsfun// patch_setT. Qed.

Lemma :
\int[mu]_( in D `&` P) f x = \int[mu]_( in D) (f \_ P) x.

Proof.

by rewrite integral_mkcond [RHS]integral_mkcond patch_setI. Qed.

Lemma :
\int[mu]_( in P `&` D) f x = \int[mu]_( in D) (f \_ P) x.

Proof.

by rewrite setIC integral_mkcondr. Qed.

End domain_change.
Arguments integral_mkcond {d T R mu} D f.

Files

Module mathcomp.analysis.lebesgue_integral_theory.lebesgue_integral_definition