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.
# 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.).
## Structures for functions on classes of sets
```
{additive_charge set T -> \bar R} == notation for additive charges where
T is a semiring of sets and R is a
numFieldType
The HB class is AdditiveCharge.
{charge set T -> \bar R} == type of charges over T a semiring of sets
where R is a numFieldType
The HB class is Charge.
isCharge == factory corresponding to the "textbook
definition" of charges
```
## Instances of mathematical structures
```
measure_of_charge nu nu0 == measure corresponding to the charge nu, nu0
is a proof that nu is non-negative
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
charge_add n1 n2 == the charge corresponding to the sum of
charges n1 and n2
charge_of_finite_measure mu == charge corresponding to a finite measure mu
```
## Theory
```
nu.-positive_set P == P is a positive set with nu a charge
nu.-negative_set 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").
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
: 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
Proof.
HB.instance Definition _ := SigmaFinite_isFinite.Build d T R mu finite.
Let
semi_additive
: semi_additive mu.
Proof.
HB.instance Definition _ := isAdditiveCharge.Build d T R mu semi_additive.
Let
semi_sigma_additive
: semi_sigma_additive mu.
Proof.
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.
Proof.
Hint Resolve charge0 : core.
Lemma
charge_semi_additiveW
nu
:
nu set0 = 0 -> semi_additive nu -> semi_additive2 nu.
Proof.
move=> nu0 anu A B mA mB + AB; rewrite -bigcup2inE bigcup_mkord.
move=> /(
anu (
bigcup2 A B))
->.
- by rewrite !(
big_ord_recl, big_ord0)
/= adde0.
- by move=> [|[|[]]]//=.
- move=> [|[|i]] [|[|j]]/= _ _ //.
+ by rewrite AB => -[].
+ by rewrite setI0 => -[].
+ by rewrite setIC AB => -[].
+ by rewrite setI0 => -[].
+ by rewrite set0I => -[].
+ by rewrite set0I => -[].
+ by rewrite setI0 => -[].
Qed.
Lemma
charge_semi_additive2E
nu
: semi_additive2 nu = additive2 nu.
Proof.
rewrite propeqE; split=> [anu A B ? ? ?|anu A B ? ? _ ?]; last by rewrite anu.
by rewrite anu //; exact: measurableU.
Qed.
Lemma
charge_semi_additive2
nu
: semi_additive2 nu.
Proof.
Hint Resolve charge_semi_additive2 : core.
Lemma
chargeU
nu
: additive2 nu
Proof.
by rewrite -charge_semi_additive2E. Qed.
Lemma
chargeDI
nu
(
A
B
: set T)
: measurable A -> measurable B ->
nu A = nu (
A `\` B)
+ nu (
A `&` B).
Proof.
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).
Proof.
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
Proof.
Let
mu_ge0
S
: 0 <= mu S
Proof.
Let
mu_sigma_additive
: semi_sigma_additive mu.
Proof.
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
Proof.
Let
nu_finite
S
: measurable S -> nu S \is a fin_num.
Proof.
Let
nu_sigma_additive
: semi_sigma_additive nu.
Proof.
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).
Proof.
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.
Proof.
HB.instance Definition _ := SigmaFinite_isFinite.Build _ _ _
restr crestr_finite_measure_function.
Let
crestr_semi_additive
: semi_additive restr.
Proof.
HB.instance Definition _ :=
isAdditiveCharge.Build _ _ _ restr crestr_semi_additive.
Let
crestr_semi_sigma_additive
: semi_sigma_additive restr.
Proof.
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.
Proof.
Let
crestr0_fin_num_fun
: fin_num_fun restr.
Proof.
Let
crestr0_sigma_additive
: semi_sigma_additive restr.
Proof.
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
Proof.
by []. Qed.
Let
czero_finite_measure_function
B
: measurable B -> czero B \is a fin_num.
Proof.
by []. Qed.
Let
czero_sigma_additive
: semi_sigma_additive czero.
Proof.
move=> F mF tF mUF; rewrite [X in X --> _](
_ : _ = cst 0)
; first exact: cvg_cst.
by apply/funext => n; rewrite big1.
Qed.
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
Proof.
Let
cscale_finite_measure_function
U
: measurable U -> cscale U \is a fin_num.
Proof.
Let
cscale_sigma_additive
: semi_sigma_additive cscale.
Proof.
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.
Proof.
by move=> numu E mE /numu; rewrite /cscale => ->//; rewrite mule0. Qed.
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.
Proof.
move=> /negbTE c0 munu E mE /eqP; rewrite /cscale mule_eq0 eqe c0/=.
by move=> /eqP/munu; exact.
Qed.
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.
Proof.
by rewrite /cadd 2!charge0 adde0. Qed.
Let
cadd_finite
A
: measurable A -> cadd A \is a fin_num.
Proof.
by move=> mA; rewrite fin_numD !fin_num_measure. Qed.
Let
cadd_sigma_additive
: semi_sigma_additive cadd.
Proof.
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.
Proof.
by move=> nu0mu nu1mu A mA A0; rewrite /cadd nu0mu// nu1mu// adde0.
Qed.
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.
Proof.
Let
pushforward_finite
A
: measurable A -> pushforward nu mf A \is a fin_num.
Proof.
Let
pushforward_sigma_additive
: semi_sigma_additive (
pushforward nu mf).
Proof.
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.
Proof.
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.
Proof.
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.
Proof.
by move=> [mN]; exact. Qed.
Lemma
negative_set0
nu
: nu.
-negative_set set0.
Proof.
Lemma
positive_negative0
nu
P
N
: nu.
-positive_set P -> nu.
-negative_set N ->
forall
S,
measurable S -> nu (
S `&` P `&` N)
= 0.
Proof.
move=> [mP posP] [mN negN] S mS; apply/eqP; rewrite eq_le; apply/andP; split.
apply: negN; first by apply: measurableI => //; exact: measurableI.
by apply/setIidPl; rewrite -setIA setIid.
rewrite -setIAC.
apply: posP; first by apply: measurableI => //; exact: measurableI.
by apply/setIidPl; rewrite -setIA setIid.
Qed.
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).
Proof.
Lemma
negative_setU
nu
N
M
:
nu.
-negative_set N -> nu.
-negative_set M -> nu.
-negative_set (
N `|` M).
Proof.
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)
Proof.
by move: x => [[[? ?] ?]] []. Qed.
Let
A_D
x
: A_ x `<=` D
Proof.
by move: x => [[[? ?] ?]] []. Qed.
Let
g_ge0
x
: 0 <= g_ x
Proof.
by move: x => [[[? ?] ?]] []. Qed.
Let
nuA_g_
x
: nu (
A_ x)
>= mine (
g_ x * 2^-1%:E)
1.
Proof.
by move: x => [[[? ?] ?]] []. Qed.
Let
nuA_ge0
x
: 0 <= nu (
A_ x).
Proof.
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.
Proof.
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] }.
Proof.
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 --> 0.
Proof.
Lemma
hahn_decomposition_lemma
: measurable D ->
{A | [/\ A `<=` D, nu.
-negative_set A & nu A <= nu D]}.
Proof.
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)
Proof.
by move: x => [[[? ?] ?] [/= ? []]]. Qed.
Let
negative_set_A_
x
: nu.
-negative_set (
A_ x).
Proof.
by move: x => [[[? ?] ?]] -[]. Qed.
Let
nuA_z_
x
: nu (
A_ x)
<= maxe (
z_ x * 2^-1%:E) (
- 1%E).
Proof.
by move: x => [[[? ?] ?]] -[]. Qed.
Let
nuA_le0
x
: nu (
A_ x)
<= 0.
Proof.
Let
z_le0
x
: z_ x <= 0.
Proof.
by move: x => [[[? ?] ?]] -[]. Qed.
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.
Proof.
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)
] }.
Proof.
Theorem
Hahn_decomposition
: exists
P
N,
hahn_decomposition nu P N.
Proof.
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).
Proof.
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
Proof.
by have [[mP _] _ _ _] := nuPN. Qed.
Let
mN
: measurable N
Proof.
by have [_ [mN _] _ _] := nuPN. Qed.
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.
Proof.
by []. Qed.
Let
positive_set_cjordan_pos
E
: 0 <= cjordan_pos E.
Proof.
Definition
jordan_pos
:= measure_of_charge _ positive_set_cjordan_pos.
Lemma
jordan_posE
A
: jordan_pos A = cjordan_pos A.
Proof.
by []. Qed.
HB.instance Definition _ := Measure.on jordan_pos.
Let
finite_jordan_pos
: fin_num_fun jordan_pos.
Proof.
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.
Proof.
Let
positive_set_cjordan_neg
E
: 0 <= cjordan_neg E.
Proof.
Definition
jordan_neg
:= measure_of_charge _ positive_set_cjordan_neg.
Lemma
jordan_negE
A
: jordan_neg A = cjordan_neg A.
Proof.
by []. Qed.
HB.instance Definition _ := Measure.on jordan_neg.
Let
finite_jordan_neg
: fin_num_fun jordan_neg.
Proof.
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.
Proof.
Lemma
jordan_pos_dominates
(
mu
: {measure set T -> \bar R})
:
nu `<< mu -> jordan_pos `<< mu.
Proof.
Lemma
jordan_neg_dominates
(
mu
: {measure set T -> \bar R})
:
nu `<< mu -> jordan_neg `<< mu.
Proof.
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.
Proof.
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.
Proof.
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.
Proof.
Lemma
sup_int_approxRN_lty
: M < +oo.
Proof.
Lemma
sup_int_approxRN_fin_num
: M \is a fin_num.
Proof.
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 }.
Proof.
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.
Proof.
Lemma
approxRN_seq_ge0
x
n
: 0 <= g_ n x.
Proof.
Lemma
measurable_approxRN_seq
n
: measurable_fun setT (
g_ n).
Proof.
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).
Proof.
Lemma
max_approxRN_seq_ge0
n
x
: 0 <= F_ n x.
Proof.
Lemma
max_approxRN_seq_ge
n
x
: F_ n x >= g_ n x.
Proof.
by apply/bigmax_geP; right => /=; exists ord_max. Qed.
Lemma
max_approxRN_seq_nd
x
: nondecreasing_seq (
F_ ^~ x).
Proof.
Lemma
is_cvg_max_approxRN_seq
n
: cvg (
F_ ^~ n).
Proof.
Lemma
is_cvg_int_max_approxRN_seq
A
:
measurable A -> cvg (
fun
n
=> \int[mu]_(
x
in A)
F_ n x).
Proof.
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].
Proof.
by apply/seteqP; split. Qed.
Lemma
trivIset_is_max_approxRN
n
: trivIset [set: nat] (
E n).
Proof.
apply/trivIsetP => /= i j _ _ ij.
apply/seteqP; split => // x []; rewrite /E/= => -[+ + [+ +]].
wlog : i j ij / (
i < j)
%N.
move=> h Fmgi iFm Fmgj jFm.
have := ij; rewrite neq_lt => /orP[ji|ji]; first exact: (
h i j).
by apply: (
h j i)
=> //; rewrite eq_sym.
by move=> {}ij Fmgi h Fmgj => /(
_ _ ij)
; rewrite -Fmgi -Fmgj ltxx.
Qed.
Lemma
bigsetU_is_max_approxRN
m
: \big[setU/set0]_(
j
< m.
+1)
E m j = [set: T].
Proof.
apply/seteqP; split => // x _; rewrite -bigcup_mkord.
pose j := [arg max_(
j
> @ord0 m)
g_ j x]%O.
have j0_proof : exists
k,
(
k < m.
+1)
%N && (
g_ k x == g_ j x).
by exists j => //; rewrite eqxx andbT.
pose j0 := ex_minn j0_proof.
have j0m : (
j0 < m.
+1)
%N by rewrite /j0; case: ex_minnP => // ? /andP[].
have j0max k : (
k < j0)
%N -> g_ k x < g_ j0 x.
rewrite /j0; case: ex_minnP => //= j' /andP[j'm j'j] h kj'.
rewrite lt_neqAle; apply/andP; split; last first.
rewrite (
eqP j'j)
/j; case: arg_maxP => //= i _.
by move/(
_ (
Ordinal (
ltn_trans kj' j'm)))
; exact.
apply/negP => /eqP gkj'.
have := h k; rewrite -(
eqP j'j)
-gkj' eqxx andbT (
ltn_trans kj' j'm).
by move=> /(
_ erefl)
; rewrite leqNgt kj'.
exists j0 => //; split.
rewrite /F_ /max_approxRN_seq (
bigmax_eq_arg _ ord0)
//; last first.
by move=> ? _; rewrite leNye.
rewrite /j0/=; case: ex_minnP => //= j' /andP[j'm /eqP].
by rewrite /g_ => -> h.
by move=> k kj; exact: j0max.
Qed.
Lemma
measurable_is_max_approxRN
m
j
: measurable (
E m j).
Proof.
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.
Proof.
Lemma
fRN_ge0
x
: 0 <= fRN x.
Proof.
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).
Proof.
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.
Proof.
Let
F_G
m
: F m \in G.
Proof.
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.
Proof.
Lemma
int_fRN_lty
: \int[mu]_x `|fRN x| < +oo.
Proof.
Lemma
int_fRN_ub
A
: measurable A -> \int[mu]_(
x
in A)
fRN x <= nu A.
Proof.
Lemma
int_fRNE
: \int[mu]_x fRN x = M.
Proof.
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}.
Proof.
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.
Proof.
Let
fin_num_int_fRN_eps
B
: measurable B ->
\int[mu]_(
x
in B) (
fRN x + epsRN%:num%:E)
\is a fin_num.
Proof.
Let
fin_num_sigmaRN
B
: measurable B -> sigmaRN B \is a fin_num.
Proof.
Let
sigmaRN_sigma_additive
: semi_sigma_additive sigmaRN.
Proof.
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].
Proof.
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].
Proof.
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.
Proof.
by rewrite /f; case: pselect => // numu _; case: cid => x []. Qed.
Lemma
f_fin_num
: nu `<< mu -> forall
x,
f x \is a fin_num.
Proof.
by rewrite /f; case: pselect => // numu _; case: cid => x []. Qed.
Lemma
f_integrable
: nu `<< mu -> mu.
-integrable [set: T] f.
Proof.
by rewrite /f; case: pselect => // numu _; case: cid => x []. Qed.
Lemma
f_integral
: nu `<< mu -> forall
A,
measurable A ->
nu A = \int[mu]_(
x
in A)
f x.
Proof.
by rewrite /f; case: pselect => // numu _; case: cid => x []. Qed.
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.
Proof.
Lemma
integrableM
f
E
: (
forall
x,
0 <= f x)
-> measurable E ->
nu.
-integrable E f -> mu.
-integrable E (
f \* 'd nu '/d mu).
Proof.
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).
Proof.
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].
Proof.
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)).
Proof.
Lemma
Radon_Nikodym_fin_num
x
: nu `<< mu ->
Radon_Nikodym x \is a fin_num.
Proof.
Lemma
Radon_Nikodym_integrable
: nu `<< mu ->
mu.
-integrable [set: T] Radon_Nikodym.
Proof.
Lemma
Radon_Nikodym_integral
A
: nu `<< mu ->
measurable A -> nu A = \int[mu]_(
x
in A)
Radon_Nikodym x.
Proof.
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).
Proof.
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.
Proof.
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).
Proof.
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).
Proof.
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).
Proof.
End Radon_Nikodym_chain_rule.