Library mathcomp.analysis.charge

(* mathcomp analysis (c) 2022 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.

Charges 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.).

Mathematical structures

additive_charge T R == type of additive charges over T a semiring of sets The HB class is AdditiveCharge. {additive_charge set T -> \bar R} == notation for additive_charge T R charge T R == type of charges over T a semiring of sets The HB class is Charge. {charge set T -> \bar R} == notation for charge T R measure_of_charge nu nu0 == measure corresponding to the charge nu, nu0 is a proof that nu is non-negative

Instances of mathematical structures

crestr nu mD == restriction of the charge nu to the domain D where mD is a proof that D is measurable crestr0 nu mD == csrestr nu mD that returns 0 for non-measurable sets czero == zero charge cscale r nu == charge nu scaled by a factor r : R

Theory

positive_set nu P == P is a positive set with nu a charge negative_set nu N == N is a negative set with nu a charge hahn_decomposition nu P N == the full set can be decomposed in P and N, a positive set and a negative set for the charge nu jordan_pos nu nuPN == the charge obtained by restricting the charge nu to the positive set P of the Hahn decomposition nuPN: hahn_decomposition nu P N jordan_neg nu nuPN == the charge obtained by restricting the charge nu to the positive set N of the Hahn decomposition nuPN: hahn_decomposition nu P N 'd nu '/d mu == Radon-Nikodym derivative of nu w.r.t. mu (the scope is charge_scope)

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 }").
Reserved Notation "'d nu '/d mu" (at level 10, nu, mu at next level,
  format "''d' nu ''/d' mu").

Declare Scope charge_scope.

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 : semiRingOfSetsType 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 = [set: T] → 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.

Definition measure_of_charge d (T : measurableType d) (R : realType)
  (nu : set T → \bar R) of (∀ E, 0 ≤ nu E) := nu.

Section measure_of_charge.
Context d (T : measurableType d) (R : realType).
Variables (nu : {charge set T → \bar R}) (nupos : ∀ E, 0 ≤ nu E).


Let mu0 : mu set0 = 0.

Let mu_ge0 S : 0 ≤ mu S.

Let mu_sigma_additive : semi_sigma_additive mu.


End measure_of_charge.
Arguments measure_of_charge {d T R}.

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.

Definition crestr0 d (T : measurableType d) (R : realFieldType) (D : set T)
  (f : set T → \bar R) (mD : measurable D) :=
    fun X ⇒ if X \in measurable then crestr f mD X else 0.

Section charge_restriction0.
Context d (T : measurableType d) (R : realFieldType).
Variables (nu : {charge set T → \bar R}) (D : set T) (mD : measurable D).


Let crestr0_fin_num_fun : fin_num_fun restr.


Let crestr0_additive : semi_additive restr.


Let crestr0_sigma_additive : semi_sigma_additive restr.


End charge_restriction0.

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 ∧ ∀ A, measurable A → A `<=` P → nu A ≥ 0.

Definition negative_set nu (N : set T) :=
  measurable N ∧ ∀ A, measurable A → A `<=` N → nu A ≤ 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 g_ (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 g_ge0 x : 0 ≤ g_ x.
Let nuA_g_ x : nu (A_ x) ≥ mine (g_ 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 d_ A := ereal_sup (subDD A).

Let d_ge0 X : 0 ≤ d_ X.

Let elt_rel i j :=
  [/\ g_ j = d_ (U_ i), A_ j `<=` D `\` U_ i & U_ j = U_ i `|` A_ j ].

Let next_elt A :
  { B | [/\ measurable B, B `<=` D `\` A & nu B ≥ mine (d_ 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 = [set: T] & 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 := {AzU : set T × \bar R × set T | elt_prop AzU.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).

Let 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 : { 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.

Section jordan_decomposition.
Context d (T : measurableType d) (R : realType).
Variable nu : {charge set T → \bar R}.
Variables (P N : set T) (nuPN : hahn_decomposition nu P N).

Let mP : measurable P.

Let mN : measurable N.

Let cjordan_pos : {charge set T → \bar R} :=
  [the charge _ _ of crestr0 nu mP].

Let positive_set_cjordan_pos E : 0 ≤ cjordan_pos E.

Definition jordan_pos := measure_of_charge _ positive_set_cjordan_pos.


Let finite_jordan_pos : fin_num_fun jordan_pos.


Let cjordan_neg : {charge set T → \bar R} :=
  [the charge _ _ of cscale (-1) [the charge _ _ of crestr0 nu mN]].

Let positive_set_cjordan_neg E : 0 ≤ cjordan_neg E.

Definition jordan_neg := measure_of_charge _ positive_set_cjordan_neg.


Let finite_jordan_neg : fin_num_fun jordan_neg.


Lemma jordan_decomp A : measurable A → nu A = jordan_pos A - jordan_neg A.

Lemma jordan_pos_dominates (mu : {measure set T → \bar R}) :
  nu `<< mu → jordan_pos `<< mu.

Lemma jordan_neg_dominates (mu : {measure set T → \bar R}) :
  nu `<< mu → jordan_neg `<< mu.

End jordan_decomposition.

We put definitions and lemmas used only in the proof of the Radon-Nikodym theorem as Definition's and Lemma's in the following modules. See https://staff.aist.go.jp/reynald.affeldt/documents/measure-ppl2023.pdf for an overview.
Module approxRN.
Section approxRN.
Context d (T : measurableType d) (R : realType).
Variables mu nu : {measure set T → \bar R}.

Definition approxRN := [set g : T → \bar R | [/\
  ∀ x, 0 ≤ g x, mu.-integrable [set: T] g &
  ∀ E, measurable E → \int[mu]_(x in E) g x ≤ nu E] ].

Let approxRN_neq0 : approxRN !=set0.

Definition int_approxRN := [set \int[mu]_x g x | g in approxRN].

Definition sup_int_approxRN := ereal_sup int_approxRN.

Lemma sup_int_approxRN_ge0 : 0 ≤ sup_int_approxRN.

End approxRN.
End approxRN.

Module approxRN_seq.
Section approxRN_seq.
Context d (T : measurableType d) (R : realType).
Variable mu : {measure set T → \bar R}.
Variable nu : {finite_measure set T → \bar R}.

Import approxRN.

Let approxRN := approxRN mu nu.
Let int_approxRN := int_approxRN mu nu.
Let M := sup_int_approxRN mu nu.

Let int_approxRN_ub : ∃ M, ∀ x, x \in int_approxRN → x ≤ M%:E.

Lemma sup_int_approxRN_lty : M < +oo.

Lemma sup_int_approxRN_fin_num : M \is a fin_num.

Lemma approxRN_seq_ex : { g : (T → \bar R)^nat |
  ∀ k, g k \in approxRN ∧ \int[mu]_x g k x > M - k.+1%:R^-1%:E }.

Definition approxRN_seq : (T → \bar R)^nat := sval approxRN_seq_ex.

Let g_ := approxRN_seq.

Lemma approxRN_seq_prop : ∀ m,
  g_ m \in approxRN ∧ \int[mu]_x (g_ m x) > M - m.+1%:R^-1%:E.

Lemma approxRN_seq_ge0 x n : 0 ≤ g_ n x.

Lemma measurable_approxRN_seq n : measurable_fun setT (g_ n).

Definition max_approxRN_seq n x := \big[maxe/-oo]_(j < n.+1) g_ j x.

Let F_ := max_approxRN_seq.

Lemma measurable_max_approxRN_seq n : measurable_fun [set: T] (F_ n).

Lemma max_approxRN_seq_ge0 n x : 0 ≤ F_ n x.

Lemma max_approxRN_seq_ge n x : F_ n x ≥ g_ n x.

Lemma max_approxRN_seq_nd x : nondecreasing_seq (F_ ^~ x).

Lemma is_cvg_max_approxRN_seq n : cvg (F_ ^~ n).

Lemma is_cvg_int_max_approxRN_seq A :
  measurable A → cvg (fun n ⇒ \int[mu]_(x in A) F_ n x).

Definition is_max_approxRN m j :=
  [set x | F_ m x = g_ j x ∧ ∀ k, (k < j)%N → g_ k x < g_ j x].

Let E := is_max_approxRN.

Lemma is_max_approxRNE m j : E m j = [set x| F_ m x = g_ j x] `&`
    [set x |∀ k, (k < j)%nat → g_ k x < g_ j x].

Lemma trivIset_is_max_approxRN n : trivIset [set: nat] (E n).

Lemma bigsetU_is_max_approxRN m : \big[setU/set0]_(j < m.+1) E m j = [set: T].

Lemma measurable_is_max_approxRN m j : measurable (E m j).

End approxRN_seq.
End approxRN_seq.

Module lim_max_approxRN_seq.
Section lim_max_approxRN_seq.
Context d (T : measurableType d) (R : realType).
Variables mu nu : {finite_measure set T → \bar R}.

Import approxRN.

Let G := approxRN mu nu.
Let M := sup_int_approxRN mu nu.

Import approxRN_seq.

Let g := approxRN_seq mu nu.
Let F := max_approxRN_seq mu nu.

Definition fRN := fun x ⇒ lim (F ^~ x).

Lemma measurable_fun_fRN : measurable_fun [set: T] fRN.

Lemma fRN_ge0 x : 0 ≤ fRN x.

Let int_fRN_lim A : measurable A →
  \int[mu]_(x in A) fRN x = lim (fun n ⇒ \int[mu]_(x in A) F n x).

Let E m j := is_max_approxRN mu nu m j.

Let int_F_nu m A (mA : measurable A) : \int[mu]_(x in A) F m x ≤ nu A.

Let F_G m : F m \in G.

Let M_g_F m : M - m.+1%:R^-1%:E < \int[mu]_x g m x ∧
              \int[mu]_x g m x ≤ \int[mu]_x F m x ≤ M.

Lemma int_fRN_lty : \int[mu]_x `|fRN x| < +oo.

Lemma int_fRN_ub A : measurable A → \int[mu]_(x in A) fRN x ≤ nu A.

Lemma int_fRNE : \int[mu]_x fRN x = M.

Section ab_absurdo.
Context A (mA : measurable A) (h : \int[mu]_(x in A) fRN x < nu A).

Lemma epsRN_ex :
  {eps : {posnum R} | \int[mu]_(x in A) (fRN x + eps%:num%:E) < nu A}.

Definition epsRN := sval epsRN_ex.

Definition sigmaRN B := nu B - \int[mu]_(x in B) (fRN x + epsRN%:num%:E).

Let fin_num_int_fRN_eps B : measurable B →
  \int[mu]_(x in B) (fRN x + epsRN%:num%:E) \is a fin_num.

Let fin_num_sigmaRN B : measurable B → sigmaRN B \is a fin_num.


Let sigmaRN_semi_additive : semi_additive sigmaRN.


Let sigmaRN_semi_sigma_additive : semi_sigma_additive sigmaRN.


End ab_absurdo.

End lim_max_approxRN_seq.
End lim_max_approxRN_seq.

Section radon_nikodym_finite.
Context d (T : measurableType d) (R : realType).
Variables mu nu : {finite_measure set T → \bar R}.

Import approxRN.

Let G := approxRN mu nu.
Let M := sup_int_approxRN mu nu.

Import lim_max_approxRN_seq.

Let f := fRN mu nu.
Let mf := measurable_fun_fRN.
Let f_ge0 := fRN_ge0.

Lemma radon_nikodym_finite : nu `<< mu → ∃ f : T → \bar R,
  [/\ ∀ x, f x ≥ 0, mu.-integrable [set: T] f &
      ∀ E, measurable E → nu E = \int[mu]_(x in E) f x].

End radon_nikodym_finite.

Section radon_nikodym.
Context d (T : measurableType d) (R : realType).

Let radon_nikodym_sigma_finite
    (mu : {sigma_finite_measure set T → \bar R})
    (nu : {finite_measure set T → \bar R}) :
  nu `<< mu →
  exists2 f : T → \bar R, mu.-integrable [set: T] f &
    ∀ E, E \in measurable → nu E = integral mu E f.

Let Radon_Nikodym0
  (mu : {sigma_finite_measure set T → \bar R}) (nu : {charge set T → \bar R}) :
  nu `<< mu →
  exists2 f : T → \bar R, mu.-integrable [set: T] f &
    ∀ A, measurable A → nu A = \int[mu]_(x in A) f x.

Definition Radon_Nikodym
    (mu : {sigma_finite_measure set T → \bar R})
    (nu : {charge set T → \bar R}) : T → \bar R :=
  match pselect (nu `<< mu) with
  | left nu_mu ⇒ sval (cid2 (Radon_Nikodym0 nu_mu))
  | right _ ⇒ cst -oo
  end.


Theorem Radon_Nikodym_integrable
    (mu : {sigma_finite_measure set T → \bar R})
    (nu : {charge set T → \bar R}) :
    nu `<< mu →
  mu.-integrable [set: T] ('d nu '/d mu).

Theorem Radon_Nikodym_integral
    (mu : {sigma_finite_measure set T → \bar R})
    (nu : {charge set T → \bar R}) :
    nu `<< mu →
  ∀ A, measurable A → nu A = \int[mu]_(x in A) ('d nu '/d mu) x.

End radon_nikodym.
Notation "'d nu '/d mu" := (Radon_Nikodym mu nu) : charge_scope.