(* 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 Require Import mathcomp_extra boolp classical_sets cardinality.
From mathcomp Require Import functions fsbigop 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.

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").
Reserved Notation "nu .-negative_set" (at level 2, format "nu .-negative_set").
Reserved Notation "nu .-positive_set" (at level 2, format "nu .-positive_set").

Declare Scope charge_scope.

Set Implicit Arguments.

Import Order.TTheory GRing.Theory Num.Def Num.Theory.
Import numFieldTopology.Exports.

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 isSemiSigmaAdditive d T R mu & AdditiveCharge d mu }.

Notation "{ 'charge' 'set' T '->' '\bar' R }" := (charge T R) : ring_scope.



Let finite : fin_num_fun mu.


Let semi_additive : semi_additive mu.


Let semi_sigma_additive : semi_sigma_additive mu.



Section charge_lemmas.
Context d (T : ringOfSetsType 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 : semiRingOfSetsType d) (R : numFieldType)
  (nu : set T → \bar R) of (∀ E, 0 ≤ nu E) := nu.

Section measure_of_charge.
Context d (T : ringOfSetsType d) (R : realFieldType).
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 : ringOfSetsType 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 : semiRingOfSetsType 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 : semiRingOfSetsType d) (R : numFieldType) (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 crestr00 : restr set0 = 0.

Let crestr0_fin_num_fun : fin_num_fun restr.

Let crestr0_sigma_additive : semi_sigma_additive restr.


End charge_restriction0.

Section charge_zero.
Context d (T : semiRingOfSetsType 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_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 : ringOfSetsType 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_sigma_additive : semi_sigma_additive cscale.


End charge_scale.

Section charge_add.
Local Open Scope ereal_scope.
Context d (T : measurableType d) (R : realType).
Variables (m1 m2 : {charge set T → \bar R}).

Definition cadd := m1 \+ m2.

Let cadd0 : cadd set0 = 0.

Let cadd_finite A : measurable A → cadd A \is a fin_num.

Let cadd_sigma_additive : semi_sigma_additive cadd.


End charge_add.

Section positive_negative_set.
Context d (T : semiRingOfSetsType d) (R : numDomainType).
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.

Notation "nu .-negative_set" := (negative_set nu) : charge_scope.
Notation "nu .-positive_set" := (positive_set nu) : charge_scope.
Local Open Scope charge_scope.

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 : nu.-negative_set N → nu N ≤ 0.

Lemma negative_set0 nu : nu.-negative_set set0.

Lemma positive_negative0 nu P N : nu.-positive_set P → nu.-negative_set 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, nu.-negative_set (F i)) →
  nu.-negative_set (\bigcup_i F i).

Lemma negative_setU nu N M :
  nu.-negative_set N → nu.-negative_set M → nu.-negative_set (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] }.

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, nu.-negative_set A & nu A ≤ nu D]}.

End hahn_decomposition_lemma.

Definition hahn_decomposition d (T : semiRingOfSetsType d) (R : numFieldType)
    (nu : {charge set T → \bar R}) P N :=
  [/\ nu.-positive_set P, nu.-negative_set 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,
  nu.-negative_set 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 : nu.-negative_set (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.

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 sigmaRN0 : sigmaRN set0 = 0.

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_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.

Section radon_nikodym_lemmas.

Lemma dominates_cscale d (T : measurableType d) (R : realType)
  (mu : {sigma_finite_measure set T → \bar R})
  (nu : {charge set T → \bar R})
  (c : R) : nu `<< mu → cscale c nu `<< mu.

Lemma Radon_Nikodym_cscale d (T : measurableType d) (R : realType)
  (mu : {sigma_finite_measure set T → \bar R})
  (nu : {charge set T → \bar R}) (c : R) :
  nu `<< mu →
  ae_eq mu [set: T] ('d [the charge _ _ of cscale c nu] '/d mu)
                    (fun x ⇒ c%:E × 'd nu '/d mu x).

Lemma dominates_caddl d (T : measurableType d)
  (R : realType) (mu : {sigma_finite_measure set T → \bar R})
  (nu0 nu1 : {charge set T → \bar R}) :
  nu0 `<< mu → nu1 `<< mu →
  cadd nu0 nu1 `<< mu.

Lemma Radon_Nikodym_cadd d (T : measurableType d) (R : realType)
    (mu : {sigma_finite_measure set T → \bar R})
    (nu0 nu1 : {charge set T → \bar R}) :
  nu0 `<< mu → nu1 `<< mu →
  ae_eq mu [set: T] ('d [the charge _ _ of cadd nu0 nu1] '/d mu)
                    ('d nu0 '/d mu \+ 'd nu1 '/d mu).

End radon_nikodym_lemmas.