Module mathcomp.analysis.charge

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.
Unset Strict Implicit.
Unset Printing Implicit Defensive.

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.

HB.mixin Record isAdditiveCharge d (T : semiRingOfSetsType d) (R : numFieldType)
  (mu : set T -> \bar R) := { charge_semi_additive : measure.semi_additive mu }.

#[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.

HB.mixin Record isSemiSigmaAdditive d (T : semiRingOfSetsType d) (R : numFieldType)
    (mu : set T -> \bar R) := {
  charge_semi_sigma_additive : semi_sigma_additive mu }.

#[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.

HB.factory Record isCharge d (T : semiRingOfSetsType d) (R : realFieldType)
    (mu : set T -> \bar R) := {
  charge0 : mu set0 = 0 ;
  charge_finite : forall x, d.-measurable x -> mu x \is a fin_num ;
  charge_sigma_additive : semi_sigma_additive mu
}.

HB.builders Context d (T : semiRingOfSetsType d) (R : realFieldType)
  mu of isCharge d T R mu.

Let finite : fin_num_fun mu

HB.instance Definition _ := SigmaFinite_isFinite.Build d T R mu finite.

Let semi_additive : measure.semi_additive mu.

HB.instance Definition _ := isAdditiveCharge.Build d T R mu semi_additive.

Let semi_sigma_additive : semi_sigma_additive mu.

HB.instance Definition _ :=
  isSemiSigmaAdditive.Build d T R mu semi_sigma_additive.

HB.end.

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 -> measure.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 (forall E, 0 <= nu E) := nu.

Section measure_of_charge.
Context d (T : ringOfSetsType d) (R : realFieldType).
Variables (nu : {charge set T -> \bar R}) (nupos : forall E, 0 <= nu E).

Local Notation mu := (measure_of_charge nupos).

Let mu0 : mu set0 = 0

Let mu_ge0 S : 0 <= mu S

Let mu_sigma_additive : semi_sigma_additive mu.

HB.instance Definition _ := isMeasure.Build _ T R (measure_of_charge nupos)
  mu0 mu_ge0 mu_sigma_additive.

End measure_of_charge.
Arguments measure_of_charge {d T R}.

Section charge_of_finite_measure.
Context d (T : measurableType d) (R : realType).
Variables (mu : {finite_measure set T -> \bar R}).

Definition charge_of_finite_measure : set T -> \bar R := mu.

Local Notation nu := charge_of_finite_measure.

Let nu0 : nu set0 = 0

Let nu_finite S : measurable S -> nu S \is a fin_num.

Let nu_sigma_additive : semi_sigma_additive nu.

HB.instance Definition _ := isCharge.Build _ T R nu
  nu0 nu_finite nu_sigma_additive.

End charge_of_finite_measure.
Arguments charge_of_finite_measure {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).

Local Notation restr := (crestr nu mD).

Let crestr_finite_measure_function U : measurable U -> restr U \is a fin_num.

HB.instance Definition _ := SigmaFinite_isFinite.Build _ _ _
  restr crestr_finite_measure_function.

Let crestr_semi_additive : measure.semi_additive restr.

HB.instance Definition _ :=
  isAdditiveCharge.Build _ _ _ restr crestr_semi_additive.

Let crestr_semi_sigma_additive : semi_sigma_additive restr.

HB.instance Definition _ :=
  isSemiSigmaAdditive.Build _ _ _ restr crestr_semi_sigma_additive.

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

Local Notation restr := (crestr0 nu mD).

Let crestr00 : restr set0 = 0.

Let crestr0_fin_num_fun : fin_num_fun restr.

Let crestr0_sigma_additive : semi_sigma_additive restr.

HB.instance Definition _ := isCharge.Build _ _ _
    restr crestr00 crestr0_fin_num_fun crestr0_sigma_additive.

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.

HB.instance Definition _ := isCharge.Build _ _ _ czero
     czero0 czero_finite_measure_function czero_sigma_additive.

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.

HB.instance Definition _ := SigmaFinite_isFinite.Build _ _ _
  cscale cscale_finite_measure_function.

Let cscale_semi_additive : measure.semi_additive cscale.

HB.instance Definition _ :=
  isAdditiveCharge.Build _ _ _ cscale cscale_semi_additive.

Let cscale_sigma_additive : semi_sigma_additive cscale.

HB.instance Definition _ := isCharge.Build _ _ _ cscale
  cscale0 cscale_finite_measure_function cscale_sigma_additive.

End charge_scale.

Lemma dominates_cscalel d (T : measurableType d) (R : realType)
  (mu : set T -> \bar R)
  (nu : {charge set T -> \bar R})
  (c : R) : nu `<< mu -> cscale c nu `<< mu.

Lemma dominates_cscaler d (T : measurableType d) (R : realType)
  (nu : {charge set T -> \bar R})
  (mu : set T -> \bar R)
  (c : R) : c != 0%R -> mu `<< nu -> mu `<< cscale c nu.

Section charge_add.
Local Open Scope ereal_scope.
Context d (T : measurableType d) (R : realType).
Variables (n1 n2 : {charge set T -> \bar R}).

Definition cadd := n1 \+ n2.

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.

HB.instance Definition _ := isCharge.Build _ _ _ cadd
  cadd0 cadd_finite cadd_sigma_additive.

End charge_add.

Lemma dominates_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 ->
  cadd nu0 nu1 `<< mu.

Section pushforward_charge.
Local Open Scope ereal_scope.
Context d1 d2 (T1 : measurableType d1) (T2 : measurableType d2) (f : T1 -> T2).
Variables (R : realFieldType) (nu : {charge set T1 -> \bar R}).

Hypothesis mf : measurable_fun setT f.

Let pushforward0 : pushforward nu mf set0 = 0.

Let pushforward_finite A : measurable A -> pushforward nu mf A \is a fin_num.

Let pushforward_sigma_additive : semi_sigma_additive (pushforward nu mf).

HB.instance Definition _ := isCharge.Build _ _ _ (pushforward nu mf)
  pushforward0 pushforward_finite pushforward_sigma_additive.

End pushforward_charge.

HB.builders Context d (T : measurableType d) (R : realType)
  (mu : set T -> \bar R) of Measure_isFinite d T R mu.

Let mu0 : mu set0 = 0.

HB.instance Definition _ := isCharge.Build _ _ _
  mu (measure0 [the content _ _ of mu])
    fin_num_measure measure_semi_sigma_additive.

HB.end.

Section dominates_pushforward.

Lemma dominates_pushforward d d' (T : measurableType d) (T' : measurableType d')
  (R : realType) (mu : {measure set T -> \bar R})
  (nu : {charge set T -> \bar R}) (f : T -> T') (mf : measurable_fun setT f) :
  nu `<< mu -> pushforward nu mf `<< pushforward mu mf.

End dominates_pushforward.

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 /\ forall A, measurable A -> A `<=` P -> nu A >= 0.

Definition negative_set nu (N : set T) :=
  measurable N /\ forall 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 ->
  forall 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) :
    (forall 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 mine2_cvg_0_cvg_0 (u : (\bar R)^nat) : (forall k, 0 <= u k) ->
  mine (u n * 2^-1%:E) 1 @[n --> \oo] --> 0 -> u n @[n --> \oo] --> 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 : exists 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 ->
  forall 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

Local Definition cjordan_pos : {charge set T -> \bar R} :=
  [the charge _ _ of crestr0 nu mP].

Lemma cjordan_posE A : cjordan_pos A = crestr0 nu mP A.

Let positive_set_cjordan_pos E : 0 <= cjordan_pos E.

Definition jordan_pos := measure_of_charge _ positive_set_cjordan_pos.

Lemma jordan_posE A : jordan_pos A = cjordan_pos A.

HB.instance Definition _ := Measure.on jordan_pos.

Let finite_jordan_pos : fin_num_fun jordan_pos.

HB.instance Definition _ := @Measure_isFinite.Build _ _ _
  jordan_pos finite_jordan_pos.

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

Lemma cjordan_negE A : cjordan_neg A = - crestr0 nu mN A.

Let positive_set_cjordan_neg E : 0 <= cjordan_neg E.

Definition jordan_neg := measure_of_charge _ positive_set_cjordan_neg.

Lemma jordan_negE A : jordan_neg A = cjordan_neg A.

HB.instance Definition _ := Measure.on jordan_neg.

Let finite_jordan_neg : fin_num_fun jordan_neg.

HB.instance Definition _ := @Measure_isFinite.Build _ _ _
  jordan_neg finite_jordan_neg.

Lemma jordan_decomp (A : set T) : measurable A ->
  nu A = (cadd [the charge _ _ of jordan_pos]
           ([the charge _ _ of cscale (-1) [the charge _ _ of 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 | [/\
  forall x, 0 <= g x, mu.-integrable [set: T] g &
  forall 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 : exists M, forall 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 |
  forall 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 : forall 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 @ \oo).

Lemma is_cvg_int_max_approxRN_seq A :
  measurable A -> cvg ((fun n => \int[mu]_(x in A) F_ n x) @ \oo).

Definition is_max_approxRN m j :=
  [set x | F_ m x = g_ j x /\ forall 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 |forall 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 @ \oo).

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 (\int[mu]_(x in A) F n x @[n --> \oo]).

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.

HB.instance Definition _ := @isCharge.Build _ _ _ sigmaRN
  sigmaRN0 fin_num_sigmaRN sigmaRN_sigma_additive.

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 -> exists f : T -> \bar R,
  [/\ forall x, f x >= 0, mu.-integrable [set: T] f &
      forall E, measurable E -> nu E = \int[mu]_(x in E) f x].

End radon_nikodym_finite.

Section radon_nikodym_sigma_finite.
Context d (T : measurableType d) (R : realType).
Variables (mu : {sigma_finite_measure set T -> \bar R})
          (nu : {finite_measure set T -> \bar R}).

Lemma radon_nikodym_sigma_finite : nu `<< mu ->
  exists f : T -> \bar R, [/\ forall x, f x >= 0, forall x, f x \is a fin_num,
    mu.-integrable [set: T] f &
    forall A, measurable A -> nu A = \int[mu]_(x in A) f x].

End radon_nikodym_sigma_finite.

Module Radon_Nikodym_SigmaFinite.
Section radon_nikodym_sigma_finite_def.
Context d (T : measurableType d) (R : realType).
Variables (nu : {finite_measure set T -> \bar R})
          (mu : {sigma_finite_measure set T -> \bar R}).

Definition f : T -> \bar R :=
  match pselect (nu `<< mu) with
  | left nu_mu => sval (cid (radon_nikodym_sigma_finite nu_mu))
  | right _ => cst -oo
  end.

Lemma f_ge0 : nu `<< mu -> forall x, 0 <= f x.

Lemma f_fin_num : nu `<< mu -> forall x, f x \is a fin_num.

Lemma f_integrable : nu `<< mu -> mu.-integrable [set: T] f.

Lemma f_integral : nu `<< mu -> forall A, measurable A ->
    nu A = \int[mu]_(x in A) f x.

End radon_nikodym_sigma_finite_def.

Section integrableM.
Context d (T : measurableType d) (R : realType).
Variables (nu : {finite_measure set T -> \bar R})
          (mu : {sigma_finite_measure set T -> \bar R}).
Hypothesis numu : nu `<< mu.
Implicit Types f : T -> \bar R.

Local Notation "'d nu '/d mu" := (f nu mu).

Lemma change_of_variables f E : (forall x, 0 <= f x) ->
    measurable E -> measurable_fun E f ->
  \int[mu]_(x in E) (f x * ('d nu '/d mu) x) = \int[nu]_(x in E) f x.

Lemma integrableM f E : (forall x, 0 <= f x) -> measurable E ->
  nu.-integrable E f -> mu.-integrable E (f \* 'd nu '/d mu).

End integrableM.

Section chain_rule.
Context d (T : measurableType d) (R : realType).
Variables (nu : {finite_measure set T -> \bar R})
          (la : {sigma_finite_measure set T -> \bar R})
          (mu : {finite_measure set T -> \bar R}).

Local Notation "'d nu '/d mu" := (f nu mu).

Lemma chain_rule E : nu `<< mu -> mu `<< la -> measurable E ->
  ae_eq la E ('d nu '/d la) ('d nu '/d mu \* 'd mu '/d la).

End chain_rule.
End Radon_Nikodym_SigmaFinite.

Section radon_nikodym.
Context d (T : measurableType d) (R : realType).
Variables (nu : {charge set T -> \bar R})
          (mu : {sigma_finite_measure set T -> \bar R}).

Local Lemma Radon_Nikodym0 : nu `<< mu ->
  exists f : T -> \bar R, [/\ (forall x, f x \is a fin_num),
    mu.-integrable [set: T] f &
    forall A, measurable A -> nu A = \int[mu]_(x in A) f x].

Definition Radon_Nikodym : T -> \bar R :=
  match pselect (nu `<< mu) with
  | left nu_mu => sval (cid (Radon_Nikodym0 nu_mu))
  | right _ => cst -oo
  end.

Lemma Radon_NikodymE (numu : nu `<< mu) :
  Radon_Nikodym = sval (cid (Radon_Nikodym0 numu)).

Lemma Radon_Nikodym_fin_num x : nu `<< mu ->
  Radon_Nikodym x \is a fin_num.

Lemma Radon_Nikodym_integrable : nu `<< mu ->
  mu.-integrable [set: T] Radon_Nikodym.

Lemma Radon_Nikodym_integral A : nu `<< mu ->
  measurable A -> nu A = \int[mu]_(x in A) Radon_Nikodym x.

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

#[global] Hint Extern 0 (_.-integrable setT ('d _ '/d _)) =>
  solve [apply: Radon_Nikodym_integrable] : core.
#[global] Hint Extern 0 (measurable_fun setT ('d _ '/d _)) =>
  solve [apply: measurable_int; exact: Radon_Nikodym_integrable] : core.

Section Radon_Nikodym_charge_of_finite_measure.
Context d (T : measurableType d) (R : realType).
Variables (nu : {finite_measure set T -> \bar R})
          (mu : {sigma_finite_measure set T -> \bar R}).
Hypothesis numu : nu `<< mu.
Implicit Types f : T -> \bar R.

Lemma ae_eq_Radon_Nikodym_SigmaFinite E : measurable E ->
  ae_eq mu E (Radon_Nikodym_SigmaFinite.f nu mu)
             ('d [the charge _ _ of charge_of_finite_measure nu] '/d mu).

Lemma Radon_Nikodym_change_of_variables f E : measurable E ->
    nu.-integrable E f ->
  \int[mu]_(x in E)
    (f x * ('d [the charge _ _ of charge_of_finite_measure nu] '/d mu) x) =
  \int[nu]_(x in E) f x.

End Radon_Nikodym_charge_of_finite_measure.

Section radon_nikodym_lemmas.
Context d (T : measurableType d) (R : realType).
Implicit Types (nu : {charge set T -> \bar R})
               (mu : {sigma_finite_measure set T -> \bar R}).

Lemma Radon_Nikodym_cscale mu nu c E : measurable E -> nu `<< mu ->
  ae_eq mu E ('d [the charge _ _ of cscale c nu] '/d mu)
             (fun x => c%:E * 'd nu '/d mu x).

Lemma Radon_Nikodym_cadd mu nu0 nu1 E : measurable E ->
  nu0 `<< mu -> nu1 `<< mu ->
  ae_eq mu E ('d [the charge _ _ of cadd nu0 nu1] '/d mu)
             ('d nu0 '/d mu \+ 'd nu1 '/d mu).

End radon_nikodym_lemmas.

Section Radon_Nikodym_chain_rule.
Context d (T : measurableType d) (R : realType).
Variables (nu : {charge set T -> \bar R})
          (la : {sigma_finite_measure set T -> \bar R})
          (mu : {finite_measure set T -> \bar R}).

Lemma Radon_Nikodym_chain_rule : nu `<< mu -> mu `<< la ->
  ae_eq la setT ('d nu '/d la)
                ('d nu '/d mu \*
                  'd [the charge _ _ of charge_of_finite_measure mu] '/d la).

End Radon_Nikodym_chain_rule.