proposition: Lemma lower_semicontinuous_HL_maximal f : locally_integrable setT f -> lower_semicontinuous (HL f).
proof: Proof. move=> [mf ? locf]; apply/lower_semicontinuousP => a. have [a0|a0] := lerP 0 a; last first. rewrite [X in open X](_ : _ = setT); first exact: openT. by apply/seteqP; split=> // x _; exact: (lt_le_trans _ (HL_maximalT_ge0 _ _)). rewrite openE /= => x /= /ereal_sup_gt[_ [r r0] <-] afxr. rewrite /= in_itv /= andbT in r0. rewrite /iavg in afxr; set k := \int[_]_(_ in _) _ in afxr. apply: nbhs_singleton; apply: nbhs_interior; rewrite nbhsE /=. have k_gt0 : 0 < k. rewrite lt0e integral_ge0// andbT; apply/negP => /eqP k0. by move: afxr; rewrite k0 mule0 lte_fin ltNge a0. move: a0; rewrite le_eqVlt => /predU1P[a0|a0]. move: afxr; rewrite -{a}a0 => xrk. near (0%R : R)^'+ => d. have xrdk : 0 < (fine (mu (ball x (r + d))))^-1%:E * k. rewrite mule_gt0// lte_fin invr_gt0// fine_gt0//. rewrite lebesgue_measure_ball; last by rewrite addr_ge0// ltW. by rewrite ltry andbT lte_fin pmulrn_lgt0// addr_gt0. exists (ball x d). by split; [exact: ball_open|exact: ballxx]. move=> y; rewrite /ball/= => xyd. have ? : ball x r `<=` ball y (r + d). move=> /= z; rewrite /ball/= => xzr; rewrite -(subrK x y) -(addrA (y - x)%R). by rewrite (le_lt_trans (ler_normD _ _))// addrC ltrD// distrC. have ? : k <= \int[mu]_(y in ball y (r + d)) `|(f y)%:E|. apply: subset_integral =>//; [exact:measurable_ball|exact:measurable_ball|]. apply: measurable_funTS; apply: measurableT_comp => //=. by apply/measurableT_comp => //=; case: locf. have : iavg f (ball y (r + d)) <= HL f y. apply: ereal_sup_ub => /=; exists (r + d)%R => //. by rewrite in_itv/= andbT addr_gt0. apply/lt_le_trans/(lt_le_trans xrdk); rewrite /iavg. do 2 (rewrite lebesgue_measure_ball; last by rewrite addr_ge0// ltW). rewrite lee_wpmul2l// lee_fin invr_ge0// fine_ge0// lee_fin pmulrn_rge0//. by rewrite addr_gt0. have ka_pos : fine k / a \is Num.pos. by rewrite posrE divr_gt0// fine_gt0 // k_gt0/= locally_integrable_ltbally. have k_fin_num : k \is a fin_num. by rewrite ge0_fin_numE ?locally_integrable_ltbally// integral_ge0. have kar : (0 < 2^-1 * (fine k / a) - r)%R. move: afxr; rewrite -{1}(fineK k_fin_num) -lte_pdivr_mulr; last first. by rewrite fine_gt0// k_gt0/= ltey_eq k_fin_num. rewrite (lebesgue_measure_ball _ (ltW r0))//. rewrite -!EFinM !lte_fin -invf_div ltf_pV2 ?posrE ?pmulrn_lgt0//. rewrite /= -[in X in X -> _]mulr_natl -ltr_pdivlMl//. by rewrite -[in X in X -> _]subr_gt0. near (0%R : R)^'+ => d. have axrdk : a%:E < (fine (mu (ball x (r + d))))^-1%:E * k. rewrite lebesgue_measure_ball//; last by rewrite addr_ge0// ltW. rewrite -(fineK k_fin_num) -lte_pdivr_mulr; last first. by rewrite fine_gt0// k_gt0/= locally_integrable_ltbally. rewrite -!EFinM !lte_fin -invf_div ltf_pV2//; last first. by rewrite posrE fine_gt0// ltry andbT lte_fin pmulrn_lgt0// addr_gt0. rewrite -mulr_natl -ltr_pdivlMl// -ltrBrDl. by near: d; exact: nbhs_right_lt. exists (ball x d). by split; [exact: ball_open|exact: ballxx]. move=> y; rewrite /ball/= => xyd. have ? : ball x r `<=` ball y (r + d). move=> /= z; rewrite /ball/= => xzr; rewrite -(subrK x y) -(addrA (y - x)%R). by rewrite (le_lt_trans (ler_normD _ _))// addrC ltrD// distrC. have ? : k <= \int[mu]_(z in ball y (r + d)) `|(f z)%:E|. apply: subset_integral => //; [exact: measurable_ball|exact: measurable_ball|]. by apply: measurable_funTS; do 2 apply: measurableT_comp => //. have afxrdi : a%:E < (fine (mu (ball x (r + d))))^-1%:E * \int[mu]_(z in ball y (r + d)) `|(f z)%:E|. by rewrite (lt_le_trans axrdk)// lee_wpmul2l// lee_fin invr_ge0// fine_ge0. have /lt_le_trans : a%:E < iavg f (ball y (r + d)). apply: (lt_le_trans afxrdi); rewrite /iavg. do 2 (rewrite lebesgue_measure_ball; last by rewrite addr_ge0// ltW). rewrite lee_wpmul2l// lee_fin invr_ge0// fine_ge0//= lee_fin pmulrn_rge0//. by rewrite addr_gt0. apply; apply: ereal_sup_ub => /=. by exists (r + d)%R => //; rewrite in_itv/= andbT addr_gt0. 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