Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

simplify proof script, %type in notations #1013

Merged
merged 1 commit into from
Aug 31, 2023
Merged

simplify proof script, %type in notations #1013

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
24 changes: 12 additions & 12 deletions theories/kernel.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -74,7 +74,7 @@ HB.mixin Record isKernel d d' (X : measurableType d) (Y : measurableType d')
HB.structure Definition Kernel d d'
(X : measurableType d) (Y : measurableType d') (R : realType) :=
{ k & isKernel _ _ X Y R k }.
Notation "R .-ker X ~> Y" := (kernel X Y R).
Notation "R .-ker X ~> Y" := (kernel X%type Y R).

Arguments measurable_kernel {_ _ _ _ _} _.

Expand Down Expand Up @@ -177,7 +177,7 @@ HB.structure Definition SFiniteKernel d d'
(X : measurableType d) (Y : measurableType d') (R : realType) :=
{ k of @Kernel _ _ _ _ R k &
Kernel_isSFinite_subdef _ _ X Y R k }.
Notation "R .-sfker X ~> Y" := (SFiniteKernel.type X Y R).
Notation "R .-sfker X ~> Y" := (SFiniteKernel.type X%type Y R).
Arguments sfinite_kernel_subdef {_ _ _ _ _} _.

Lemma eq_sfkernel d d' (T : measurableType d) (T' : measurableType d')
Expand All @@ -200,7 +200,7 @@ HB.structure Definition FiniteKernel d d'
(X : measurableType d) (Y : measurableType d') (R : realType) :=
{ k of @SFiniteKernel _ _ _ _ _ k &
SFiniteKernel_isFinite _ _ X Y R k }.
Notation "R .-fker X ~> Y" := (finite_kernel X Y R).
Notation "R .-fker X ~> Y" := (finite_kernel X%type Y R).
Arguments measure_uub {_ _ _ _ _} _.

HB.factory Record Kernel_isFinite d d'
Expand Down Expand Up @@ -356,7 +356,7 @@ HB.structure Definition SubProbabilityKernel
d d' (X : measurableType d) (Y : measurableType d') (R : realType) :=
{ k of @FiniteKernel _ _ _ _ _ k &
FiniteKernel_isSubProbability _ _ X Y R k }.
Notation "R .-spker X ~> Y" := (sprobability_kernel X Y R).
Notation "R .-spker X ~> Y" := (sprobability_kernel X%type Y R).

HB.factory Record Kernel_isSubProbability d d'
(X : measurableType d) (Y : measurableType d') (R : realType)
Expand Down Expand Up @@ -389,7 +389,7 @@ HB.structure Definition ProbabilityKernel d d'
(X : measurableType d) (Y : measurableType d') (R : realType) :=
{ k of @SubProbabilityKernel _ _ _ _ _ k &
SubProbability_isProbability _ _ X Y R k }.
Notation "R .-pker X ~> Y" := (probability_kernel X Y R).
Notation "R .-pker X ~> Y" := (probability_kernel X%type Y R).

HB.factory Record Kernel_isProbability d d'
(X : measurableType d) (Y : measurableType d') (R : realType)
Expand Down Expand Up @@ -507,7 +507,7 @@ Variable k : X * Y -> \bar R.

Lemma measurable_fun_xsection_integral
(l : X -> {measure set Y -> \bar R})
(k_ : ({nnsfun [the measurableType _ of (X * Y)%type] >-> R})^nat)
(k_ : ({nnsfun [the measurableType _ of X * Y] >-> R})^nat)
(ndk_ : nondecreasing_seq (k_ : (X * Y -> R)^nat))
(k_k : forall z, EFin \o (k_ ^~ z) --> k z) :
(forall n r,
Expand Down Expand Up @@ -847,7 +847,7 @@ Section kcomp_is_measure.
Context d1 d2 d3 (X : measurableType d1) (Y : measurableType d2)
(Z : measurableType d3) (R : realType).
Variable l : R.-ker X ~> Y.
Variable k : R.-ker [the measurableType _ of (X * Y)%type] ~> Z.
Variable k : R.-ker [the measurableType _ of X * Y] ~> Z.

Local Notation "l \; k" := (kcomp l k).

Expand Down Expand Up @@ -885,7 +885,7 @@ Module KCOMP_FINITE_KERNEL.
Section kcomp_finite_kernel_kernel.
Context d d' d3 (X : measurableType d) (Y : measurableType d')
(Z : measurableType d3) (R : realType) (l : R.-fker X ~> Y)
(k : R.-ker [the measurableType _ of (X * Y)%type] ~> Z).
(k : R.-ker [the measurableType _ of X * Y] ~> Z).

Lemma measurable_fun_kcomp_finite U :
measurable U -> measurable_fun [set: X] ((l \; k) ^~ U).
Expand All @@ -903,7 +903,7 @@ Section kcomp_finite_kernel_finite.
Context d d' d3 (X : measurableType d) (Y : measurableType d')
(Z : measurableType d3) (R : realType).
Variable l : R.-fker X ~> Y.
Variable k : R.-fker [the measurableType _ of (X * Y)%type] ~> Z.
Variable k : R.-fker [the measurableType _ of X * Y] ~> Z.

Let mkcomp_finite : measure_fam_uub (l \; k).
Proof.
Expand All @@ -927,7 +927,7 @@ Section kcomp_sfinite_kernel.
Context d d' d3 (X : measurableType d) (Y : measurableType d')
(Z : measurableType d3) (R : realType).
Variable l : R.-sfker X ~> Y.
Variable k : R.-sfker [the measurableType _ of (X * Y)%type] ~> Z.
Variable k : R.-sfker [the measurableType _ of X * Y] ~> Z.

Import KCOMP_FINITE_KERNEL.

Expand Down Expand Up @@ -973,7 +973,7 @@ Section kcomp_sfinite_kernel.
Context d d' d3 (X : measurableType d) (Y : measurableType d')
(Z : measurableType d3) (R : realType).
Variable l : R.-sfker X ~> Y.
Variable k : R.-sfker [the measurableType _ of (X * Y)%type] ~> Z.
Variable k : R.-sfker [the measurableType _ of X * Y] ~> Z.

HB.instance Definition _ :=
isKernel.Build _ _ X Z R (l \; k) (measurable_fun_mkcomp_sfinite l k).
Expand Down Expand Up @@ -1047,7 +1047,7 @@ Section integral_kcomp.
Context d d2 d3 (X : measurableType d) (Y : measurableType d2)
(Z : measurableType d3) (R : realType).
Variables (l : R.-sfker X ~> Y)
(k : R.-sfker [the measurableType _ of (X * Y)%type] ~> Z).
(k : R.-sfker [the measurableType _ of X * Y] ~> Z).

Let integral_kcomp_indic x E (mE : measurable E) :
\int[(l \; k) x]_z (\1_E z)%:E = \int[l x]_y (\int[k (x, y)]_z (\1_E z)%:E).
Expand Down
4 changes: 2 additions & 2 deletions theories/lebesgue_integral.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -104,7 +104,7 @@ Reserved Notation "{ 'nnsfun' aT >-> T }"
(at level 0, format "{ 'nnsfun' aT >-> T }").
Reserved Notation "[ 'nnsfun' 'of' f ]"
(at level 0, format "[ 'nnsfun' 'of' f ]").
Notation "{ 'nnsfun' aT >-> T }" := (@NonNegSimpleFun.type _ aT T) : form_scope.
Notation "{ 'nnsfun' aT >-> T }" := (@NonNegSimpleFun.type _ aT%type T) : form_scope.
Notation "[ 'nnsfun' 'of' f ]" := [the {nnsfun _ >-> _} of f] : form_scope.

Section mfun_pred.
Expand Down Expand Up @@ -4597,7 +4597,7 @@ Variable m1 : {sigma_finite_measure set T1 -> \bar R}.
Variable m2 : {sigma_finite_measure set T2 -> \bar R}.

Lemma product_measure_unique
(m' : {measure set [the semiRingOfSetsType _ of (T1 * T2)%type] -> \bar R}) :
(m' : {measure set [the semiRingOfSetsType _ of T1 * T2] -> \bar R}) :
(forall A1 A2, measurable A1 -> measurable A2 ->
m' (A1 `*` A2) = m1 A1 * m2 A2) ->
forall X : set (T1 * T2), measurable X -> (m1 \x m2) X = m' X.
Expand Down
14 changes: 7 additions & 7 deletions theories/measure.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1135,13 +1135,13 @@ Lemma measurable_fun_if (g h : T1 -> T2) D (mD : measurable D)
measurable_fun D (fun t => if f t then g t else h t).
Proof.
move=> mx my /= _ B mB; rewrite (_ : _ @^-1` B =
((f @^-1` [set true]) `&` (g @^-1` B) `&` (f @^-1` [set true])) `|`
((f @^-1` [set false]) `&` (h @^-1` B) `&` (f @^-1` [set false]))).
((f @^-1` [set true]) `&` (g @^-1` B)) `|`
((f @^-1` [set false]) `&` (h @^-1` B))).
rewrite setIUr; apply: measurableU.
- by rewrite setIAC setIid setIA; apply: mx => //; exact: mf.
- by rewrite setIAC setIid setIA; apply: my => //; exact: mf.
apply/seteqP; split=> [t /=| t]; first by case: ifPn => ft; [left|right].
by move=> /= [|]; case: ifPn => ft; case=> -[].
- by rewrite setIA; apply: mx => //; exact: mf.
- by rewrite setIA; apply: my => //; exact: mf.
apply/seteqP; split=> [t /=| t /= [] [] ->//].
by case: ifPn => ft; [left|right].
Qed.

Lemma measurable_fun_ifT (g h : T1 -> T2) (f : T1 -> bool)
Expand Down Expand Up @@ -1560,7 +1560,7 @@ HB.structure Definition Measure d (T : semiRingOfSetsType d)
(R : numFieldType) :=
{mu of Content_isMeasure d T R mu & Content d mu}.

Notation "{ 'measure' 'set' T '->' '\bar' R }" := (measure T R)
Notation "{ 'measure' 'set' T '->' '\bar' R }" := (measure T%type R)
(at level 36, T, R at next level,
format "{ 'measure' 'set' T '->' '\bar' R }") : ring_scope.

Expand Down