proposition: Lemma HL_maximal_ge0 f D : locally_integrable D f -> forall x, 0 <= HL (f \_ D) x.
proof: Proof. move=> Df x; apply: ereal_sup_le => //=. pose k := \int[mu]_(x in D `&` ball x 1) `|f x|%:E. exists ((fine (mu (ball x 1)))^-1%:E * k); last first. rewrite mule_ge0//; last exact: integral_ge0. by rewrite lee_fin// invr_ge0// fine_ge0. exists 1%R; first by rewrite in_itv/= ltr01. rewrite iavg_restrict//; last exact: measurable_ball. by case: Df => _ /open_measurable. 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