diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 9f0d4b226..568d57437 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -56,12 +56,6 @@ - in `mathcomp_extra.v`: + lemma `invf_ltp` -### Changed - -- in `topology.v`: - + lemmas `subspace_pm_ball_center`, `subspace_pm_ball_sym`, - `subspace_pm_ball_triangle`, `subspace_pm_entourage` turned - into local `Let`'s - in `classical_sets.v`: + lemmas `setC_I`, `bigcup_subset` @@ -106,6 +100,11 @@ ### Changed +- in `topology.v`: + + lemmas `subspace_pm_ball_center`, `subspace_pm_ball_sym`, + `subspace_pm_ball_triangle`, `subspace_pm_entourage` turned + into local `Let`'s + - in `lebesgue_integral.v`: + lemma `measurable_int`: argument `mu` now explicit diff --git a/theories/charge.v b/theories/charge.v index 743c458d1..0e35a7dd7 100644 --- a/theories/charge.v +++ b/theories/charge.v @@ -13,7 +13,11 @@ Require Import esum measure realfun lebesgue_measure lebesgue_integral. (* NB: See CONTRIBUTING.md for an introduction to HB concepts and commands. *) (* *) (* This file contains a formalization of charges (a.k.a. signed measures) and *) -(* their theory (Hahn decomposition theorem, etc.). *) +(* their theory (Hahn decomposition theorem, Radon-Nikodym derivative, etc.). *) +(* *) +(* Reference: *) +(* - Y. Ishiguro, R. Affeldt. The Radon-Nikodym Theorem and the Lebesgue- *) +(* Stieltjes measure in Coq. Computer Software 41(2) 2024 *) (* *) (* ## Structures for functions on classes of sets *) (* ``` *) @@ -59,6 +63,10 @@ Require Import esum measure realfun lebesgue_measure lebesgue_integral. (* decomposition nuPN: hahn_decomposition nu P N *) (* charge_variation nuPN == variation of the charge nu *) (* := jordan_pos nuPN \+ jordan_neg nuPN *) +(* induced intf == charge induced by a function f : T -> \bar R *) +(* R has type realType; T is a measurableType. *) +(* intf is a proof that f is integrable over *) +(* [set: T] *) (* 'd nu '/d mu == Radon-Nikodym derivative of nu w.r.t. mu *) (* (the scope is charge_scope) *) (* ``` *) @@ -1073,12 +1081,12 @@ move=> /choice[F /= H]. have mF i : measurable (F i) by have [] := H i. have : mu (lim_sup_set F) = 0. apply: lim_sup_set_cvg0 => //. - have h : \sum_(0 <= n < k) (1 / 2 ^+ n.+1)%:E @[k --> \oo] --> (1 : \bar R). + have h : \sum_(0 <= n < k) (1 / 2 ^+ n.+1)%:E @[k --> \oo] --> (1%E : \bar R). apply/fine_cvgP; split. apply: nearW => /= n; rewrite sum_fin_num//. by apply/allP => /= r /mapP[/= k _] ->. - under eq_fun do rewrite sumEFin. have := @cvg_geometric_series_half R 1 0; rewrite {1}/series/= expr0 divr1. + under [in X in _ -> X]eq_fun do rewrite sumEFin. by under eq_fun do under eq_bigr do rewrite addn1 natrX. apply: (@le_lt_trans _ _ (\sum_(0 <= n = e%:E by exact: lt_le_trans. have echarge n : e%:E <= charge_variation nuPN (\bigcup_(j >= n) F j). have [_ _ /le_trans] := H n; apply. rewrite le_measure// ?inE//; first exact: bigcup_measurable. - by apply: bigcup_sup => //=. -have /(_ _ _)/cvg_lim <-// := @lim_sup_set_cvg _ _ _ (charge_variation nuPN) F. + by apply: bigcup_sup => /=. +have /(_ _ _)/cvg_lim <-// := lim_sup_set_cvg (charge_variation nuPN) F. apply: lime_ge. apply: ereal_nonincreasing_is_cvgn => a b ab. rewrite le_measure ?inE//; [exact: bigcup_measurable| diff --git a/theories/ftc.v b/theories/ftc.v index 38e865a94..5d0138223 100644 --- a/theories/ftc.v +++ b/theories/ftc.v @@ -10,6 +10,12 @@ Require Import derive charge. (**md**************************************************************************) (* # Fundamental Theorem of Calculus for the Lebesgue Integral *) (* *) +(* NB: See CONTRIBUTING.md for an introduction to HB concepts and commands. *) +(* *) +(* This file provides a proof of the first fundamental theorem of calculus *) +(* for the Lebesgue integral. We derive from this theorem a corollary to *) +(* compute the definite integral of continuous functions. *) +(* *) (* parameterized_integral mu a x f := \int[mu]_(t \in `[a, x] f t) *) (* *) (******************************************************************************) @@ -341,7 +347,7 @@ Unshelve. all: by end_near. Qed. Lemma parameterized_integral_continuous a b (f : R -> R) : a < b -> mu.-integrable `[a, b] (EFin \o f) -> - {within `[a,b], continuous (fun x => int a x f)}. + {within `[a, b], continuous (fun x => int a x f)}. Proof. move=> ab intf; apply/(continuous_within_itvP _ ab); split; last first. split; last exact: parameterized_integral_cvg_at_left. diff --git a/theories/lebesgue_stieltjes_measure.v b/theories/lebesgue_stieltjes_measure.v index a65d2e14c..958eab237 100644 --- a/theories/lebesgue_stieltjes_measure.v +++ b/theories/lebesgue_stieltjes_measure.v @@ -13,8 +13,10 @@ Require Import real_interval measure realfun. (* This file contains a formalization of the Lebesgue-Stieltjes measure using *) (* the Measure Extension theorem from measure.v. *) (* *) -(* Reference: *) +(* References: *) (* - Achim Klenke, Probability Theory 2nd edition, 2014 *) +(* - Y. Ishiguro, R. Affeldt. The Radon-Nikodym Theorem and the Lebesgue- *) +(* Stieltjes measure in Coq. Computer Software 41(2) 2024 *) (* *) (* ``` *) (* right_continuous f == the function f is right-continuous *) diff --git a/theories/measure.v b/theories/measure.v index f5d3173fb..75180d098 100644 --- a/theories/measure.v +++ b/theories/measure.v @@ -3701,7 +3701,7 @@ End measure_continuity. Definition lim_sup_set T (F : (set T)^nat) := \bigcap_n \bigcup_(j >= n) F j. Section borel_cantelli_realFieldType. -Context d (T : measurableType d) {R : realFieldType} +Context {d} {T : measurableType d} {R : realFieldType} (mu : {measure set T -> \bar R}). Implicit Types F : (set T)^nat. Local Open Scope ereal_scope. @@ -3728,6 +3728,7 @@ move=> mF mFoo; apply: nonincreasing_cvg_mu => //. Qed. End borel_cantelli_realFieldType. +Arguments lim_sup_set_cvg {d T R} mu F. Section borel_cantelli. Context d (T : measurableType d) {R : realType} (mu : {measure set T -> \bar R}).