proposition: Lemma nd_sintegral_lim_lemma : sintegral mu f <= limn (sintegral mu \o g).
proof: Proof. suff ? : forall c, (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 m x, (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 n => sintegral mu (g1 c n)) = sintegral mu f. have is_cvg_g1 : cvgn (fun n => 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_cvgeMl. - by apply: is_cvg_sintegral => // m n mn; apply/lefP => t; apply: nd_g. - by apply: nearW; exact: cg1g. suff : sintegral mu (g1 c n) @[n \oo] --> sintegral mu f by apply/cvg_lim. rewrite [X in X @ \oo --> _](_ : _ = fun n => \sum_(x <- fset_set (range f)) x%:E * mu (f @^-1` [set x] `&` fleg c n)); last first. rewrite funeqE => n; rewrite sintegralE. transitivity (\sum_(x \in range f) x%:E * mu (g1 c n @^-1` [set x])). apply: eq_fbigl => r. do 2 (rewrite in_finite_support; last 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 x => f @^-1` [set x] `&` fleg c A)) => r0. by rewrite preimage_nnfun0// set0I. apply: cvgeMl => //=; rewrite [X in _ --> X](_ : _ = mu (\bigcup_n (f @^-1` [set r] `&` fleg c n))); last first. by rewrite -setI_bigcupr bigcup_fleg// setIT. have ? k i : measurable (f @^-1` [set k] `&` fleg c i) by exact: measurableI. apply: nondecreasing_cvg_mu; [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.
imports: HB(structures) mathcomp(all_ssreflect ssralg ssrnum ssrint interval finmap) mathcomp(mathcomp_extra boolp classical_sets functions) mathcomp(cardinality fsbigop ) signed reals ereal topology normedtype sequences real_interval esum measure lebesgue_measure numfun