Library mathcomp.analysis.charge
(* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C. *)
From mathcomp Require Import all_ssreflect ssralg ssrnum ssrint interval.
From mathcomp Require Import finmap fingroup perm rat.
From mathcomp.classical Require Import boolp classical_sets cardinality.
From mathcomp.classical Require Import mathcomp_extra functions fsbigop.
From mathcomp.classical Require Import set_interval.
From HB Require Import structures.
Require Import reals ereal signed topology numfun normedtype sequences.
Require Import esum measure realfun lebesgue_measure lebesgue_integral.
From mathcomp Require Import all_ssreflect ssralg ssrnum ssrint interval.
From mathcomp Require Import finmap fingroup perm rat.
From mathcomp.classical Require Import boolp classical_sets cardinality.
From mathcomp.classical Require Import mathcomp_extra functions fsbigop.
From mathcomp.classical Require Import set_interval.
From HB Require Import structures.
Require Import reals ereal signed topology numfun normedtype sequences.
Require Import esum measure realfun lebesgue_measure lebesgue_integral.
This file contains a formalization of charges (a.k.a. signed measures) and
a proof of the Hahn decomposition theorem.
isAdditiveCharge == mixin for additive charges
AdditiveCharge == structure of additive charges
{additive_charge set T -> \bar R} == additive charge over T, a semiring
of sets
additive_charge T R == type of additive charges
isCharge == mixin for charges
Charge == structure of charges
charge T R == type of charges
{charge set T -> \bar R} == charge over T, a semiring of sets
crestr nu mD == restriction of the charge nu to the domain D
where mD is a proof that D is measurable
czero == zero charge
cscale r nu == charge nu scaled by a factor r
positive_set nu P == P is a positive set
negative_set nu N == N is a negative set
hahn_decomposition nu P N == the charge nu is decomposed into the positive
set P and the negative set N
Reserved Notation "{ 'additive_charge' 'set' T '->' '\bar' R }"
(at level 36, T, R at next level,
format "{ 'additive_charge' 'set' T '->' '\bar' R }").
Reserved Notation "{ 'charge' 'set' T '->' '\bar' R }"
(at level 36, T, R at next level,
format "{ 'charge' 'set' T '->' '\bar' R }").
Set Implicit Arguments.
Import Order.TTheory GRing.Theory Num.Def Num.Theory.
Import numFieldTopology.Exports.
NB: in the next releases of Coq, dependent_choice will be
generalized from Set to Type making the following lemma redundant
Section dependent_choice_Type.
Context X (R : X → X → Prop).
Lemma dependent_choice_Type : (∀ x, {y | R x y}) →
∀ x0, {f | f 0 = x0 ∧ ∀ n, R (f n) (f n.+1)}.
End dependent_choice_Type.
Local Open Scope ring_scope.
Local Open Scope classical_set_scope.
Local Open Scope ereal_scope.
#[short(type=additive_charge)]
HB.structure Definition AdditiveCharge d (T : semiRingOfSetsType d)
(R : numFieldType) := { mu of isAdditiveCharge d T R mu & FinNumFun d mu }.
Notation "{ 'additive_charge' 'set' T '->' '\bar' R }" :=
(additive_charge T R) : ring_scope.
#[export] Hint Resolve charge_semi_additive : core.
#[short(type=charge)]
HB.structure Definition Charge d (T : algebraOfSetsType d) (R : numFieldType)
:= { mu of isCharge d T R mu & AdditiveCharge d mu }.
Notation "{ 'charge' 'set' T '->' '\bar' R }" := (charge T R) : ring_scope.
Section charge_lemmas.
Context d (T : measurableType d) (R : numFieldType).
Implicit Type nu : {charge set T → \bar R}.
Lemma charge0 nu : nu set0 = 0.
Hint Resolve charge0 : core.
Lemma charge_semi_additiveW nu :
nu set0 = 0 → semi_additive nu → semi_additive2 nu.
Lemma charge_semi_additive2E nu : semi_additive2 nu = additive2 nu.
Lemma charge_semi_additive2 nu : semi_additive2 nu.
Hint Resolve charge_semi_additive2 : core.
Lemma chargeU nu : additive2 nu.
Lemma chargeDI nu (A B : set T) : measurable A → measurable B →
nu A = nu (A `\` B) + nu (A `&` B).
Lemma charge_partition nu S P N :
measurable S → measurable P → measurable N →
P `|` N = setT → P `&` N = set0 → nu S = nu (S `&` P) + nu (S `&` N).
End charge_lemmas.
#[export] Hint Resolve charge0 : core.
#[export] Hint Resolve charge_semi_additive2 : core.
Section charge_lemmas_realFieldType.
Context d (T : measurableType d) (R : realFieldType).
Implicit Type nu : {charge set T → \bar R}.
Lemma chargeD nu (A B : set T) : measurable A → measurable B →
nu (A `\` B) = nu A - nu (A `&` B).
End charge_lemmas_realFieldType.
Definition crestr d (T : measurableType d) (R : numDomainType) (D : set T)
(f : set T → \bar R) of measurable D := fun X ⇒ f (X `&` D).
Section charge_restriction.
Context d (T : measurableType d) (R : numFieldType).
Variables (nu : {charge set T → \bar R}) (D : set T) (mD : measurable D).
Let crestr_finite_measure_function U : measurable U → restr U \is a fin_num.
Let crestr_semi_additive : semi_additive restr.
Let crestr_semi_sigma_additive : semi_sigma_additive restr.
End charge_restriction.
Section charge_zero.
Context d (T : measurableType d) (R : realFieldType).
Local Open Scope ereal_scope.
Definition czero (A : set T) : \bar R := 0.
Let czero0 : czero set0 = 0.
Let czero_finite_measure_function B : measurable B → czero B \is a fin_num.
Let czero_semi_additive : semi_additive czero.
Let czero_sigma_additive : semi_sigma_additive czero.
End charge_zero.
Arguments czero {d T R}.
Section charge_scale.
Local Open Scope ereal_scope.
Context d (T : measurableType d) (R : realFieldType).
Variables (r : R) (nu : {charge set T → \bar R}).
Definition cscale (A : set T) : \bar R := r%:E × nu A.
Let cscale0 : cscale set0 = 0.
Let cscale_finite_measure_function U : measurable U → cscale U \is a fin_num.
Let cscale_semi_additive : semi_additive cscale.
Let cscale_sigma_additive : semi_sigma_additive cscale.
End charge_scale.
Section positive_negative_set.
Context d (R : numDomainType) (T : measurableType d).
Implicit Types nu : set T → \bar R.
Definition positive_set nu (P : set T) :=
measurable P ∧ ∀ E, measurable E → E `<=` P → nu E ≥ 0.
Definition negative_set nu (N : set T) :=
measurable N ∧ ∀ E, measurable E → E `<=` N → nu E ≤ 0.
End positive_negative_set.
Section positive_negative_set_lemmas.
Context d (T : measurableType d) (R : numFieldType).
Implicit Types nu : {charge set T → \bar R}.
Lemma negative_set_charge_le0 nu N : negative_set nu N → nu N ≤ 0.
Lemma negative_set0 nu : negative_set nu set0.
Lemma positive_negative0 nu P N : positive_set nu P → negative_set nu N →
∀ S, measurable S → nu (S `&` P `&` N) = 0.
End positive_negative_set_lemmas.
Section positive_negative_set_realFieldType.
Context d (T : measurableType d) (R : realFieldType).
Implicit Types nu : {charge set T → \bar R}.
Lemma bigcup_negative_set nu (F : (set T)^nat) :
(∀ i, negative_set nu (F i)) →
negative_set nu (\bigcup_i F i).
Lemma negative_setU nu N M :
negative_set nu N → negative_set nu M → negative_set nu (N `|` M).
End positive_negative_set_realFieldType.
Section hahn_decomposition_lemma.
Context d (T : measurableType d) (R : realType).
Variables (nu : {charge set T → \bar R}) (D : set T).
Let elt_prop (x : set T × \bar R) := [/\ measurable x.1,
x.1 `<=` D, 0 ≤ x.2 & nu x.1 ≥ mine (x.2 × 2^-1%:E) 1].
Let elt_type := {x : set T × \bar R × set T | elt_prop x.1}.
Let A_ (x : elt_type) := (proj1_sig x).1.1.
Let d_ (x : elt_type) := (proj1_sig x).1.2.
Let U_ (x : elt_type) := (proj1_sig x).2.
Let mA_ x : measurable (A_ x).
Let A_D x : A_ x `<=` D.
Let d_ge0 x : 0 ≤ d_ x.
Let nuA_d_ x : nu (A_ x) ≥ mine (d_ x × 2^-1%:E) 1.
Let nuA_ge0 x : 0 ≤ nu (A_ x).
Let subDD A := [set nu E | E in [set E | measurable E ∧ E `<=` D `\` A] ].
Let t_ A := ereal_sup (subDD A).
Lemma t_ge0 X : 0 ≤ t_ X.
Let elt_rel i j :=
[/\ d_ j = t_ (U_ i), A_ j `<=` D `\` U_ i & U_ j = U_ i `|` A_ j ].
Let next_elt A : 0 ≤ t_ A →
{ B | [/\ measurable B, B `<=` D `\` A & nu B ≥ mine (t_ A × 2^-1%:E) 1] }.
Context X (R : X → X → Prop).
Lemma dependent_choice_Type : (∀ x, {y | R x y}) →
∀ x0, {f | f 0 = x0 ∧ ∀ n, R (f n) (f n.+1)}.
End dependent_choice_Type.
Local Open Scope ring_scope.
Local Open Scope classical_set_scope.
Local Open Scope ereal_scope.
#[short(type=additive_charge)]
HB.structure Definition AdditiveCharge d (T : semiRingOfSetsType d)
(R : numFieldType) := { mu of isAdditiveCharge d T R mu & FinNumFun d mu }.
Notation "{ 'additive_charge' 'set' T '->' '\bar' R }" :=
(additive_charge T R) : ring_scope.
#[export] Hint Resolve charge_semi_additive : core.
#[short(type=charge)]
HB.structure Definition Charge d (T : algebraOfSetsType d) (R : numFieldType)
:= { mu of isCharge d T R mu & AdditiveCharge d mu }.
Notation "{ 'charge' 'set' T '->' '\bar' R }" := (charge T R) : ring_scope.
Section charge_lemmas.
Context d (T : measurableType d) (R : numFieldType).
Implicit Type nu : {charge set T → \bar R}.
Lemma charge0 nu : nu set0 = 0.
Hint Resolve charge0 : core.
Lemma charge_semi_additiveW nu :
nu set0 = 0 → semi_additive nu → semi_additive2 nu.
Lemma charge_semi_additive2E nu : semi_additive2 nu = additive2 nu.
Lemma charge_semi_additive2 nu : semi_additive2 nu.
Hint Resolve charge_semi_additive2 : core.
Lemma chargeU nu : additive2 nu.
Lemma chargeDI nu (A B : set T) : measurable A → measurable B →
nu A = nu (A `\` B) + nu (A `&` B).
Lemma charge_partition nu S P N :
measurable S → measurable P → measurable N →
P `|` N = setT → P `&` N = set0 → nu S = nu (S `&` P) + nu (S `&` N).
End charge_lemmas.
#[export] Hint Resolve charge0 : core.
#[export] Hint Resolve charge_semi_additive2 : core.
Section charge_lemmas_realFieldType.
Context d (T : measurableType d) (R : realFieldType).
Implicit Type nu : {charge set T → \bar R}.
Lemma chargeD nu (A B : set T) : measurable A → measurable B →
nu (A `\` B) = nu A - nu (A `&` B).
End charge_lemmas_realFieldType.
Definition crestr d (T : measurableType d) (R : numDomainType) (D : set T)
(f : set T → \bar R) of measurable D := fun X ⇒ f (X `&` D).
Section charge_restriction.
Context d (T : measurableType d) (R : numFieldType).
Variables (nu : {charge set T → \bar R}) (D : set T) (mD : measurable D).
Let crestr_finite_measure_function U : measurable U → restr U \is a fin_num.
Let crestr_semi_additive : semi_additive restr.
Let crestr_semi_sigma_additive : semi_sigma_additive restr.
End charge_restriction.
Section charge_zero.
Context d (T : measurableType d) (R : realFieldType).
Local Open Scope ereal_scope.
Definition czero (A : set T) : \bar R := 0.
Let czero0 : czero set0 = 0.
Let czero_finite_measure_function B : measurable B → czero B \is a fin_num.
Let czero_semi_additive : semi_additive czero.
Let czero_sigma_additive : semi_sigma_additive czero.
End charge_zero.
Arguments czero {d T R}.
Section charge_scale.
Local Open Scope ereal_scope.
Context d (T : measurableType d) (R : realFieldType).
Variables (r : R) (nu : {charge set T → \bar R}).
Definition cscale (A : set T) : \bar R := r%:E × nu A.
Let cscale0 : cscale set0 = 0.
Let cscale_finite_measure_function U : measurable U → cscale U \is a fin_num.
Let cscale_semi_additive : semi_additive cscale.
Let cscale_sigma_additive : semi_sigma_additive cscale.
End charge_scale.
Section positive_negative_set.
Context d (R : numDomainType) (T : measurableType d).
Implicit Types nu : set T → \bar R.
Definition positive_set nu (P : set T) :=
measurable P ∧ ∀ E, measurable E → E `<=` P → nu E ≥ 0.
Definition negative_set nu (N : set T) :=
measurable N ∧ ∀ E, measurable E → E `<=` N → nu E ≤ 0.
End positive_negative_set.
Section positive_negative_set_lemmas.
Context d (T : measurableType d) (R : numFieldType).
Implicit Types nu : {charge set T → \bar R}.
Lemma negative_set_charge_le0 nu N : negative_set nu N → nu N ≤ 0.
Lemma negative_set0 nu : negative_set nu set0.
Lemma positive_negative0 nu P N : positive_set nu P → negative_set nu N →
∀ S, measurable S → nu (S `&` P `&` N) = 0.
End positive_negative_set_lemmas.
Section positive_negative_set_realFieldType.
Context d (T : measurableType d) (R : realFieldType).
Implicit Types nu : {charge set T → \bar R}.
Lemma bigcup_negative_set nu (F : (set T)^nat) :
(∀ i, negative_set nu (F i)) →
negative_set nu (\bigcup_i F i).
Lemma negative_setU nu N M :
negative_set nu N → negative_set nu M → negative_set nu (N `|` M).
End positive_negative_set_realFieldType.
Section hahn_decomposition_lemma.
Context d (T : measurableType d) (R : realType).
Variables (nu : {charge set T → \bar R}) (D : set T).
Let elt_prop (x : set T × \bar R) := [/\ measurable x.1,
x.1 `<=` D, 0 ≤ x.2 & nu x.1 ≥ mine (x.2 × 2^-1%:E) 1].
Let elt_type := {x : set T × \bar R × set T | elt_prop x.1}.
Let A_ (x : elt_type) := (proj1_sig x).1.1.
Let d_ (x : elt_type) := (proj1_sig x).1.2.
Let U_ (x : elt_type) := (proj1_sig x).2.
Let mA_ x : measurable (A_ x).
Let A_D x : A_ x `<=` D.
Let d_ge0 x : 0 ≤ d_ x.
Let nuA_d_ x : nu (A_ x) ≥ mine (d_ x × 2^-1%:E) 1.
Let nuA_ge0 x : 0 ≤ nu (A_ x).
Let subDD A := [set nu E | E in [set E | measurable E ∧ E `<=` D `\` A] ].
Let t_ A := ereal_sup (subDD A).
Lemma t_ge0 X : 0 ≤ t_ X.
Let elt_rel i j :=
[/\ d_ j = t_ (U_ i), A_ j `<=` D `\` U_ i & U_ j = U_ i `|` A_ j ].
Let next_elt A : 0 ≤ t_ A →
{ B | [/\ measurable B, B `<=` D `\` A & nu B ≥ mine (t_ A × 2^-1%:E) 1] }.
TODO: generalize?
Let minr_cvg_0_cvg_0 (x : R^nat) : (∀ k, 0 ≤ x k)%R →
(fun n ⇒ minr (x n × 2^-1) 1)%R --> (0:R)%R → x --> (0:R)%R.
Let mine_cvg_0_cvg_fin_num (x : (\bar R)^nat) : (∀ k, 0 ≤ x k) →
(fun n ⇒ mine (x n × (2^-1)%:E) 1) --> 0 →
\∀ n \near \oo, x n \is a fin_num.
Let mine_cvg_minr_cvg (x : (\bar R)^nat) : (∀ k, 0 ≤ x k) →
(fun n ⇒ mine (x n × (2^-1)%:E) 1) --> 0 →
(fun n ⇒ minr ((fine \o x) n / 2) 1%R) --> (0:R)%R.
Let mine_cvg_0_cvg_0 (x : (\bar R)^nat) : (∀ k, 0 ≤ x k) →
(fun n ⇒ mine (x n × (2^-1)%:E) 1) --> 0 → x --> 0.
Lemma hahn_decomposition_lemma : measurable D →
{A | [/\ A `<=` D, negative_set nu A & nu A ≤ nu D]}.
End hahn_decomposition_lemma.
Definition hahn_decomposition d (T : measurableType d) (R : realType)
(nu : {charge set T → \bar R}) P N :=
[/\ positive_set nu P, negative_set nu N, P `|` N = setT & P `&` N = set0].
Section hahn_decomposition_theorem.
Context d (T : measurableType d) (R : realType).
Variable nu : {charge set T → \bar R}.
Let elt_prop (x : set T × \bar R) := [/\ x.2 ≤ 0,
negative_set nu x.1 & nu x.1 ≤ maxe (x.2 × 2^-1%:E) (- 1%E) ].
Let elt_type := {AsU : set T × \bar R × set T | elt_prop AsU.1}.
Let A_ (x : elt_type) := (proj1_sig x).1.1.
Let z_ (x : elt_type) := (proj1_sig x).1.2.
Let U_ (x : elt_type) := (proj1_sig x).2.
Let mA_ x : measurable (A_ x).
Let negative_set_A_ x : negative_set nu (A_ x).
Let nuA_z_ x : nu (A_ x) ≤ maxe (z_ x × 2^-1%:E) (- 1%E).
Let nuA_le0 x : nu (A_ x) ≤ 0.
Let z_le0 x : z_ x ≤ 0.
Let subC A := [set nu E | E in [set E | measurable E ∧ E `<=` ~` A] ].
Let s_ A := ereal_inf (subC A).
Lemma s_le0 X : s_ X ≤ 0.
Let elt_rel i j :=
[/\ z_ j = s_ (U_ i), A_ j `<=` ~` U_ i & U_ j = U_ i `|` A_ j].
Let next_elt U : s_ U ≤ 0 → { A | [/\ A `<=` ~` U,
negative_set nu A & nu A ≤ maxe (s_ U × 2^-1%R%:E) (- 1%E)] }.
Theorem Hahn_decomposition : ∃ P N, hahn_decomposition nu P N.
Lemma Hahn_decomposition_uniq P1 N1 P2 N2 :
hahn_decomposition nu P1 N1 → hahn_decomposition nu P2 N2 →
∀ S, measurable S →
nu (S `&` P1) = nu (S `&` P2) ∧ nu (S `&` N1) = nu (S `&` N2).
End hahn_decomposition_theorem.
(fun n ⇒ minr (x n × 2^-1) 1)%R --> (0:R)%R → x --> (0:R)%R.
Let mine_cvg_0_cvg_fin_num (x : (\bar R)^nat) : (∀ k, 0 ≤ x k) →
(fun n ⇒ mine (x n × (2^-1)%:E) 1) --> 0 →
\∀ n \near \oo, x n \is a fin_num.
Let mine_cvg_minr_cvg (x : (\bar R)^nat) : (∀ k, 0 ≤ x k) →
(fun n ⇒ mine (x n × (2^-1)%:E) 1) --> 0 →
(fun n ⇒ minr ((fine \o x) n / 2) 1%R) --> (0:R)%R.
Let mine_cvg_0_cvg_0 (x : (\bar R)^nat) : (∀ k, 0 ≤ x k) →
(fun n ⇒ mine (x n × (2^-1)%:E) 1) --> 0 → x --> 0.
Lemma hahn_decomposition_lemma : measurable D →
{A | [/\ A `<=` D, negative_set nu A & nu A ≤ nu D]}.
End hahn_decomposition_lemma.
Definition hahn_decomposition d (T : measurableType d) (R : realType)
(nu : {charge set T → \bar R}) P N :=
[/\ positive_set nu P, negative_set nu N, P `|` N = setT & P `&` N = set0].
Section hahn_decomposition_theorem.
Context d (T : measurableType d) (R : realType).
Variable nu : {charge set T → \bar R}.
Let elt_prop (x : set T × \bar R) := [/\ x.2 ≤ 0,
negative_set nu x.1 & nu x.1 ≤ maxe (x.2 × 2^-1%:E) (- 1%E) ].
Let elt_type := {AsU : set T × \bar R × set T | elt_prop AsU.1}.
Let A_ (x : elt_type) := (proj1_sig x).1.1.
Let z_ (x : elt_type) := (proj1_sig x).1.2.
Let U_ (x : elt_type) := (proj1_sig x).2.
Let mA_ x : measurable (A_ x).
Let negative_set_A_ x : negative_set nu (A_ x).
Let nuA_z_ x : nu (A_ x) ≤ maxe (z_ x × 2^-1%:E) (- 1%E).
Let nuA_le0 x : nu (A_ x) ≤ 0.
Let z_le0 x : z_ x ≤ 0.
Let subC A := [set nu E | E in [set E | measurable E ∧ E `<=` ~` A] ].
Let s_ A := ereal_inf (subC A).
Lemma s_le0 X : s_ X ≤ 0.
Let elt_rel i j :=
[/\ z_ j = s_ (U_ i), A_ j `<=` ~` U_ i & U_ j = U_ i `|` A_ j].
Let next_elt U : s_ U ≤ 0 → { A | [/\ A `<=` ~` U,
negative_set nu A & nu A ≤ maxe (s_ U × 2^-1%R%:E) (- 1%E)] }.
Theorem Hahn_decomposition : ∃ P N, hahn_decomposition nu P N.
Lemma Hahn_decomposition_uniq P1 N1 P2 N2 :
hahn_decomposition nu P1 N1 → hahn_decomposition nu P2 N2 →
∀ S, measurable S →
nu (S `&` P1) = nu (S `&` P2) ∧ nu (S `&` N1) = nu (S `&` N2).
End hahn_decomposition_theorem.