proposition: Lemma lebesgue_differentiation_continuous (f : R -> rT^o) (A : set R) (x : R) : open A -> mu.-integrable A (EFin \o f) -> {for x, continuous f} -> A x -> (fun r => 1 / (r *+ 2) * \int[mu]_(z in ball x r) f z) @ 0^'+ --> (f x : R^o).
proof: Proof. have ball_itvr r : 0 < r -> `[x - r, x + r] `\` ball x r = [set x + r; x - r]. move: r => _/posnumP[r]. rewrite -setU1itv ?bnd_simp ?lerBlDr -?addrA ?ler_wpDr//. rewrite -setUitv1 ?bnd_simp ?ltrBlDr -?addrA ?ltr_pwDr//. rewrite setUA setUC setUA setDUl !ballE setDv setU0 setDidl// -subset0. by move=> z /= [[]] ->; rewrite in_itv/= ltxx// andbF. have ball_itv2 r : 0 < r -> ball x r = `[x - r, x + r] `\` [set x + r; x - r]. move: r => _/posnumP[r]. rewrite -ball_itvr // setDD setIC; apply/esym/setIidPl. by rewrite ballE set_itvcc => ?/=; rewrite in_itv => /andP [/ltW -> /ltW ->]. have ritv r : 0 < r -> mu `[x - r, x + r]%classic = (r *+ 2)%:E. move=> /gt0_cp rE; rewrite /= lebesgue_measure_itv/= lte_fin. rewrite ler_ltD // ?rE // -EFinD; congr (_ _). by rewrite opprB addrAC [_ - _]addrC addrA subrr add0r. move=> oA intf ctsfx Ax. apply: cvg_zero. apply/cvgrPdist_le => eps epos; apply: filter_app (@nbhs_right_gt rT 0). move/cvgrPdist_le/(_ eps epos)/at_right_in_segment : ctsfx; apply: filter_app. apply: filter_app (open_itvcc_subset oA Ax). have mA : measurable A := open_measurable oA. near=> r => xrA; rewrite addrfctE opprfctE => feps rp. have cptxr : compact `[x - r, x + r] := @segment_compact _ _ _. rewrite distrC subr0. have -> : \int[mu]_(z in ball x r) f z = \int[mu]_(z in `[x - r, x + r]) f z. rewrite ball_itv2 //; congr (fine _); rewrite -negligible_integral //. - by apply/measurableU; exact: measurable_set1. - exact: (integrableS mA). - by rewrite measureU0//; exact: lebesgue_measure_set1. have r20 : 0 <= 1 / (r *+ 2) by rewrite ?divr_ge0 // mulrn_wge0. have -> : f x = 1 / (r *+ 2) * \int[mu]_(z in `[x - r, x + r]) cst (f x) z. rewrite /Rintegral /= integral_cst /= ?ritv // mulrC mul1r. by rewrite -mulrA divff ?mulr1//; apply: lt0r_neq0; rewrite mulrn_wgt0. have intRf : mu.-integrable `[x - r, x + r] (EFin \o f). exact: (@integrableS _ _ _ mu _ _ _ _ _ xrA intf). rewrite /= -mulrBr -fineB; first last. - rewrite integral_fune_fin_num// continuous_compact_integrable// => ?. exact: cvg_cst. - by rewrite integral_fune_fin_num. rewrite -integralB_EFin //; first last. by apply: continuous_compact_integrable => // ?; exact: cvg_cst. under [fun _ => _ + _ ]eq_fun => ? do rewrite -EFinD. have int_fx : mu.-integrable `[x - r, x + r] (fun z => (f z - f x)%:E). under [fun z => (f z - _)%:E]eq_fun => ? do rewrite EFinB. rewrite integrableB// continuous_compact_integrable// => ?. exact: cvg_cst. rewrite normrM [ `|_/_| ]ger0_norm // -fine_abse //; first last. by rewrite integral_fune_fin_num. suff : (\int[mu]_(z in `[(x - r)%R, (x + r)%R]) `|f z - f x|%:E <= (r *+ 2 * eps)%:E)%E. move=> intfeps; apply: le_trans. apply: (ler_pM r20 _ (le_refl _)); first exact: fine_ge0. apply: fine_le; last apply: le_abse_integral => //. - by rewrite abse_fin_num integral_fune_fin_num. - by rewrite integral_fune_fin_num// integrable_abse. - by case/integrableP : int_fx. rewrite div1r ler_pdivrMl ?mulrn_wgt0 // -[_ * _]/(fine (_%:E)). by rewrite fine_le// integral_fune_fin_num// integrable_abse. apply: le_trans. - apply: (@integral_le_bound _ _ _ _ _ (fun z => (f z - f x)%:E) eps%:E) => //. + by case/integrableP: int_fx. + exact: ltW. + by apply: aeW => ? ?; rewrite /= lee_fin distrC feps. by rewrite ritv //= -EFinM lee_fin mulrC. 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