proposition: Lemma maximal_inequality f c : locally_integrable setT f -> (0 < c)%R -> mu [set x | HL f x > c%:E] <= (3%:R / c)%:E * norm1 setT f.
proof: Proof. move=> /= locf c0. have r_proof x : HL f x > c%:E -> {r | (0 < r)%R & \int[mu]_(y in ball x r) `|(f y)%:E| > c%:E * mu (ball x r)}. move=> /ereal_sup_gt/cid2[y /= /cid2[r]]. rewrite in_itv/= andbT => rg0 <-{y} Hc; exists r => //. rewrite -(@fineK _ (mu (ball x r))) ?ge0_fin_numE//; last first. by rewrite lebesgue_measure_ball ?ltry// ltW. rewrite -lte_pdivl_mulr// 1?muleC// fine_gt0//. by rewrite lebesgue_measure_ball 1?ltW// ltry lte_fin mulrn_wgt0. rewrite lebesgue_regularity_inner_sup//; last first. rewrite -[X in measurable X]setTI; apply: emeasurable_fun_o_infty => //. exact: measurable_HL_maximal. apply: ub_ereal_sup => /= x /= [K [cK Kcmf <-{x}]]. pose r_ x := if pselect (HL f x > c%:E) is left H then s2val (r_proof _ H) else 1%R. have r_pos (x : R) : (0 < r_ x)%R. by rewrite /r_; case: pselect => //= cMfx; case: (r_proof _ cMfx). have cMfx_int x : c%:E < HL f x -> \int[mu]_(y in ball x (r_ x)) `|(f y)|%:E > c%:E * mu (ball x (r_ x)). move=> cMfx; rewrite /r_; case: pselect => //= => {}cMfx. by case: (r_proof _ cMfx). set B := fun r => ball r (r_ r). have {}Kcmf : K `<=` cover [set i | HL f i > c%:E] (fun i => ball i (r_ i)). by move=> r /Kcmf /= cMfr; exists r => //; exact: ballxx. have {Kcmf}[D Dsub Kcover] : finite_subset_cover [set i | c%:E < HL f i] (fun i => ball i (r_ i)) K. move: cK; rewrite compact_cover => /(_ _ _ _ _ Kcmf); apply. by move=> /= x cMfx; exact/ball_open/r_pos. have KDB : K `<=` cover [set` D] B. by apply: (subset_trans Kcover) => /= x [r Dr] rx; exists r. have is_ballB i : is_ball (B i) by exact: is_ball_ball. have Bset0 i : B i !=set0 by exists i; exact: ballxx. have [E [uE ED tEB DE]] := @vitali_lemma_finite_cover _ _ B is_ballB Bset0 D. rewrite (@le_trans _ _ (3%:R%:E * \sum_(i <- E) mu (B i)))//. have {}DE := subset_trans KDB DE. apply: (le_trans (@content_sub_additive _ _ _ [the measure _ _ of mu] K (fun i => 3%:R *` B (nth 0%R E i)) (size E) _ _ _)) => //. - by move=> k ?; rewrite scale_ballE//; exact: measurable_ball. - by apply: closed_measurable; apply: compact_closed => //; exact: Rhausdorff. - apply: (subset_trans DE); rewrite /cover bigcup_seq. by rewrite (big_nth 0%R)//= big_mkord. - rewrite ge0_sume_distrr//= (big_nth 0%R) big_mkord; apply: lee_sum => i _. rewrite scale_ballE// !lebesgue_measure_ball ?mulr_ge0 ?(ltW (r_pos _))//. by rewrite -mulrnAr EFinM. rewrite !EFinM -muleA lee_wpmul2l//=. apply: (@le_trans _ _ (\sum_(i <- E) c^-1%:E * \int[mu]_(y in B i) `|(f y)|%:E)). rewrite [in leLHS]big_seq [in leRHS]big_seq; apply: lee_sum => r /ED /Dsub /[!inE] rD. by rewrite -lee_pdivr_mull ?invr_gt0// invrK /B/=; exact/ltW/cMfx_int. rewrite -ge0_sume_distrr//; last by move=> x _; rewrite integral_ge0. rewrite lee_wpmul2l//; first by rewrite lee_fin invr_ge0 ltW. rewrite -ge0_integral_bigsetU//=. - apply: subset_integral => //. + by apply: bigsetU_measurable => ? ?; exact: measurable_ball. + by apply: measurableT_comp => //; apply: measurableT_comp => //; case: locf. - by move=> n; exact: measurable_ball. - apply: measurableT_comp => //; apply: measurable_funTS. by apply: measurableT_comp => //; case: locf. 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