Library Lebesgue.Subset_system
This file is part of the Coq Numerical Analysis library
Copyright (C) Boldo, Clément, Martin, Mayero, Mouhcine
This library is free software; you can redistribute it and/or
modify it under the terms of the GNU Lesser General Public
License as published by the Free Software Foundation; either
version 3 of the License, or (at your option) any later version.
This library is distributed in the hope that it will be useful,
but WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
COPYING file for more details.
Support for subset systems.
Brief description
Used logic axioms
From Subsets Require Import Subsets_wDep Subset_finite Subset_seq.
From Lebesgue Require Import Subset_system_def Subset_system_base Subset_system_gen.
Section Subset_systems_Def1.
Context {U : Type}.
Variable gen : (U → Prop) → Prop. Variable A0 : U → Prop.
Inductive Psyst : (U → Prop) → Prop :=
| Psyst_Gen : Incl gen Psyst
| Psyst_Mem : Psyst A0
| Psyst_Inter : Inter Psyst.
Inductive Ring : (U → Prop) → Prop :=
| Ring_Gen : Incl gen Ring
| Ring_wEmpty : wEmpty Ring
| Ring_Diff : Diff Ring
| Ring_Union : Union Ring.
Inductive Algebra : (U → Prop) → Prop :=
| Algebra_Gen : Incl gen Algebra
| Algebra_wEmpty : wEmpty Algebra
| Algebra_Compl : Compl Algebra
| Algebra_Union : Union Algebra.
Inductive Monotone_class : (U → Prop) → Prop :=
| Monotone_class_Gen : Incl gen Monotone_class
| Monotone_class_Inter_monot_seq : Inter_monot_seq Monotone_class
| Monotone_class_Union_monot_seq : Union_monot_seq Monotone_class.
Inductive Lsyst : (U → Prop) → Prop :=
| Lsyst_Gen : Incl gen Lsyst
| Lsyst_wFull : wFull Lsyst
| Lsyst_Compl : Compl Lsyst
| Lsyst_Union_disj_seq : Union_disj_seq Lsyst.
Inductive Sigma_ring : (U → Prop) → Prop :=
| Sigma_ring_Gen : Incl gen Sigma_ring
| Sigma_ring_wEmpty : wEmpty Sigma_ring
| Sigma_ring_Diff : Diff Sigma_ring
| Sigma_ring_Union_seq : Union_seq Sigma_ring.
Inductive Sigma_algebra : (U → Prop) → Prop :=
| Sigma_algebra_Gen : Incl gen Sigma_algebra
| Sigma_algebra_wEmpty : wEmpty Sigma_algebra
| Sigma_algebra_Compl : Compl Sigma_algebra
| Sigma_algebra_Union_seq : Union_seq Sigma_algebra.
End Subset_systems_Def1.
Section Subset_systems_Def2.
Context {U : Type}.
Variable P : (U → Prop) → Prop. Variable A0 : U → Prop.
Definition is_Psyst : Prop := Psyst P A0 = P.
Definition is_Semi_ring : Prop :=
wEmpty P ∧ Inter P ∧ Part_diff_finite P.
Definition is_Ring : Prop := Ring P = P.
Definition is_Semi_algebra : Prop :=
wFull P ∧ Inter P ∧ Part_compl_finite P.
Definition is_Algebra : Prop := Algebra P = P.
Definition is_Monotone_class : Prop := Monotone_class P = P.
Definition is_Lsyst : Prop := Lsyst P = P.
Definition is_Sigma_ring : Prop := Sigma_ring P = P.
Definition is_Sigma_algebra : Prop := Sigma_algebra P = P.
End Subset_systems_Def2.
Global Hint Constructors Psyst : subset_systems.
Global Hint Unfold is_Semi_ring : subset_systems.
Global Hint Constructors Ring : subset_systems.
Global Hint Unfold is_Semi_algebra : subset_systems.
Global Hint Constructors Algebra : subset_systems.
Global Hint Constructors Monotone_class : subset_systems.
Global Hint Constructors Lsyst : subset_systems.
Global Hint Constructors Sigma_ring : subset_systems.
Global Hint Constructors Sigma_algebra : subset_systems.
Section Subset_systems_Facts1.
Context {U : Type}.
Variable P : (U → Prop) → Prop.
Lemma Psyst_equiv :
∀ (A0 : U → Prop),
is_Psyst P A0 ↔ P A0 ∧ Inter P.
Proof.
split.
intros H; rewrite <- H; auto with subset_systems.
intros [H1 H2]; apply Ext; split.
intros H3; induction H3; try easy.
now apply H2.
apply Psyst_Gen.
Qed.
Lemma Ring_equiv :
is_Ring P ↔ wEmpty P ∧ Diff P ∧ Union P.
Proof.
split.
intros H; rewrite <- H; auto with subset_systems.
intros [H1 [H2 H3]]; apply Ext; split.
intros H4; induction H4; try easy; [now apply H2 | now apply H3].
apply Ring_Gen.
Qed.
Lemma Algebra_equiv :
is_Algebra P ↔ wEmpty P ∧ Compl P ∧ Union P.
Proof.
split.
intros H; rewrite <- H; auto with subset_systems.
intros [H1 [H2 H3]]; apply Ext; split.
intros H4; induction H4; try easy; [now apply H2 | now apply H3].
apply Algebra_Gen.
Qed.
Lemma Monotone_class_equiv :
is_Monotone_class P ↔ Inter_monot_seq P ∧ Union_monot_seq P.
Proof.
split.
intros H; split; rewrite <- H.
apply Monotone_class_Inter_monot_seq.
apply Monotone_class_Union_monot_seq.
intros [H1 H2]; apply Ext; split.
intros H3; induction H3; try easy; [now apply H1 | now apply H2].
apply Monotone_class_Gen.
Qed.
Lemma Lsyst_equiv :
is_Lsyst P ↔ wFull P ∧ Compl P ∧ Union_disj_seq P.
Proof.
split.
intros H; repeat split; rewrite <- H.
apply Lsyst_wFull.
apply Lsyst_Compl.
apply Lsyst_Union_disj_seq.
intros [H1 [H2 H3]]; apply Ext; split.
intros H4; induction H4; try easy; [now apply H2 | now apply H3].
apply Lsyst_Gen.
Qed.
Lemma Sigma_ring_equiv :
is_Sigma_ring P ↔ wEmpty P ∧ Diff P ∧ Union_seq P.
Proof.
split.
intros H; repeat split; rewrite <- H.
apply Sigma_ring_wEmpty.
apply Sigma_ring_Diff.
apply Sigma_ring_Union_seq.
intros [H1 [H2 H3]]; apply Ext; split.
intros H4; induction H4; try easy.
now apply H2.
now apply H3.
apply Sigma_ring_Gen.
Qed.
Lemma Sigma_algebra_equiv :
is_Sigma_algebra P ↔ wEmpty P ∧ Compl P ∧ Union_seq P.
Proof.
split.
intros H; repeat split; rewrite <- H.
apply Sigma_algebra_wEmpty.
apply Sigma_algebra_Compl.
apply Sigma_algebra_Union_seq.
intros [H1 [H2 H3]]; apply Ext; split.
intros H4; induction H4; try easy; [now apply H2 | now apply H3].
apply Sigma_algebra_Gen.
Qed.
End Subset_systems_Facts1.
Section Subset_systems_Facts2.
Context {U : Type}.
Variable gen0 gen1 : (U → Prop) → Prop. Variable A0 : U → Prop.
Lemma Psyst_lub_alt :
Incl gen0 (Psyst gen1 A0) →
Incl (Psyst gen0 A0) (Psyst gen1 A0).
Proof.
intros H A HA; induction HA.
now apply H.
apply Psyst_Mem.
now apply Psyst_Inter.
Qed.
Lemma Ring_lub_alt :
Incl gen0 (Ring gen1) →
Incl (Ring gen0) (Ring gen1).
Proof.
intros H A HA; induction HA.
now apply H.
apply Ring_wEmpty.
now apply Ring_Diff.
now apply Ring_Union.
Qed.
Lemma Algebra_lub_alt :
Incl gen0 (Algebra gen1) →
Incl (Algebra gen0) (Algebra gen1).
Proof.
intros H A HA; induction HA.
now apply H.
apply Algebra_wEmpty.
now apply Algebra_Compl.
now apply Algebra_Union.
Qed.
Lemma Monotone_class_lub_alt :
Incl gen0 (Monotone_class gen1) →
Incl (Monotone_class gen0) (Monotone_class gen1).
Proof.
intros H A HA; induction HA.
now apply H.
now apply Monotone_class_Inter_monot_seq.
now apply Monotone_class_Union_monot_seq.
Qed.
Lemma Lsyst_lub_alt :
Incl gen0 (Lsyst gen1) →
Incl (Lsyst gen0) (Lsyst gen1).
Proof.
intros H A HA; induction HA.
now apply H.
apply Lsyst_wFull.
now apply Lsyst_Compl.
now apply Lsyst_Union_disj_seq.
Qed.
Lemma Sigma_ring_lub_alt :
Incl gen0 (Sigma_ring gen1) →
Incl (Sigma_ring gen0) (Sigma_ring gen1).
Proof.
intros H A HA; induction HA.
now apply H.
apply Sigma_ring_wEmpty.
now apply Sigma_ring_Diff.
now apply Sigma_ring_Union_seq.
Qed.
Lemma Sigma_algebra_lub_alt :
Incl gen0 (Sigma_algebra gen1) →
Incl (Sigma_algebra gen0) (Sigma_algebra gen1).
Proof.
intros H A HA; induction HA.
now apply H.
apply Sigma_algebra_wEmpty.
now apply Sigma_algebra_Compl.
now apply Sigma_algebra_Union_seq.
Qed.
End Subset_systems_Facts2.
Section Subset_systems_Facts3.
Context {U : Type}.
Variable P : (U → Prop) → Prop. Variable gen : (U → Prop) → Prop. Variable A0 : U → Prop.
Lemma Psyst_lub :
is_Psyst P A0 → Incl gen P → Incl (Psyst gen A0) P.
Proof.
intros H; rewrite <- H; apply Psyst_lub_alt.
Qed.
Lemma Ring_lub :
is_Ring P → Incl gen P → Incl (Ring gen) P.
Proof.
intros H; rewrite <- H; apply Ring_lub_alt.
Qed.
Lemma Algebra_lub :
is_Algebra P → Incl gen P → Incl (Algebra gen) P.
Proof.
intros H; rewrite <- H; apply Algebra_lub_alt.
Qed.
Lemma Monotone_class_lub :
is_Monotone_class P → Incl gen P → Incl (Monotone_class gen) P.
Proof.
intros H; rewrite <- H; apply Monotone_class_lub_alt.
Qed.
Lemma Lsyst_lub :
is_Lsyst P → Incl gen P → Incl (Lsyst gen) P.
Proof.
intros H; rewrite <- H; apply Lsyst_lub_alt.
Qed.
Lemma Sigma_ring_lub :
is_Sigma_ring P → Incl gen P → Incl (Sigma_ring gen) P.
Proof.
intros H; rewrite <- H; apply Sigma_ring_lub_alt.
Qed.
Lemma Sigma_algebra_lub :
is_Sigma_algebra P → Incl gen P → Incl (Sigma_algebra gen) P.
Proof.
intros H; rewrite <- H; apply Sigma_algebra_lub_alt.
Qed.
End Subset_systems_Facts3.
Section Subset_systems_Facts4.
Context {U : Type}.
Variable gen : (U → Prop) → Prop. Variable A0 : U → Prop.
Lemma Psyst_idem :
is_Psyst (Psyst gen A0) A0.
Proof.
apply Ext_equiv; split; [now apply Psyst_lub_alt | apply Psyst_Gen].
Qed.
Lemma Ring_idem :
is_Ring (Ring gen).
Proof.
apply Ext_equiv; split; [now apply Ring_lub_alt | apply Ring_Gen].
Qed.
Lemma Algebra_idem :
is_Algebra (Algebra gen).
Proof.
apply Ext_equiv; split; [now apply Algebra_lub_alt | apply Algebra_Gen].
Qed.
Lemma Monotone_class_idem :
is_Monotone_class (Monotone_class gen).
Proof.
apply Ext_equiv; split; [now apply Monotone_class_lub_alt | apply Monotone_class_Gen].
Qed.
Lemma Lsyst_idem :
is_Lsyst (Lsyst gen).
Proof.
apply Ext_equiv; split; [now apply Lsyst_lub_alt | apply Lsyst_Gen].
Qed.
Lemma Sigma_ring_idem :
is_Sigma_ring (Sigma_ring gen).
Proof.
apply Ext_equiv; split; [now apply Sigma_ring_lub_alt | apply Sigma_ring_Gen].
Qed.
Lemma Sigma_algebra_idem :
is_Sigma_algebra (Sigma_algebra gen).
Proof.
apply Ext_equiv; split; [now apply Sigma_algebra_lub_alt | apply Sigma_algebra_Gen].
Qed.
Variable gen0 gen1 : (U → Prop) → Prop.
Lemma Psyst_monot :
Incl gen0 gen1 → Incl (Psyst gen0 A0) (Psyst gen1 A0).
Proof.
intros; apply Psyst_lub_alt, Incl_trans with gen1; [easy | apply Psyst_Gen].
Qed.
Lemma Ring_monot :
Incl gen0 gen1 → Incl (Ring gen0) (Ring gen1).
Proof.
intros; apply Ring_lub_alt, Incl_trans with gen1; [easy | apply Ring_Gen].
Qed.
Lemma Algebra_monot :
Incl gen0 gen1 → Incl (Algebra gen0) (Algebra gen1).
Proof.
intros; apply Algebra_lub_alt, Incl_trans with gen1; [easy | apply Algebra_Gen].
Qed.
Lemma Monotone_class_monot :
Incl gen0 gen1 → Incl (Monotone_class gen0) (Monotone_class gen1).
Proof.
intros; apply Monotone_class_lub_alt, Incl_trans with gen1; [easy | apply Monotone_class_Gen].
Qed.
Lemma Lsyst_monot :
Incl gen0 gen1 → Incl (Lsyst gen0) (Lsyst gen1).
Proof.
intros; apply Lsyst_lub_alt, Incl_trans with gen1; [easy | apply Lsyst_Gen].
Qed.
Lemma Sigma_ring_monot :
Incl gen0 gen1 → Incl (Sigma_ring gen0) (Sigma_ring gen1).
Proof.
intros; apply Sigma_ring_lub_alt, Incl_trans with gen1; [easy | apply Sigma_ring_Gen].
Qed.
Lemma Sigma_algebra_monot :
Incl gen0 gen1 → Incl (Sigma_algebra gen0) (Sigma_algebra gen1).
Proof.
intros; apply Sigma_algebra_lub_alt, Incl_trans with gen1; [easy | apply Sigma_algebra_Gen].
Qed.
Lemma Psyst_ext :
Incl gen0 (Psyst gen1 A0) →
Incl gen1 (Psyst gen0 A0) →
Psyst gen0 A0 = Psyst gen1 A0.
Proof.
intros; apply Ext_equiv; split; now apply Psyst_lub_alt.
Qed.
Lemma Ring_ext :
Incl gen0 (Ring gen1) →
Incl gen1 (Ring gen0) →
Ring gen0 = Ring gen1.
Proof.
intros; apply Ext_equiv; split; now apply Ring_lub_alt.
Qed.
Lemma Algebra_ext :
Incl gen0 (Algebra gen1) →
Incl gen1 (Algebra gen0) →
Algebra gen0 = Algebra gen1.
Proof.
intros; apply Ext_equiv; split; now apply Algebra_lub_alt.
Qed.
Lemma Monotone_class_ext :
Incl gen0 (Monotone_class gen1) →
Incl gen1 (Monotone_class gen0) →
Monotone_class gen0 = Monotone_class gen1.
Proof.
intros; apply Ext_equiv; split; now apply Monotone_class_lub_alt.
Qed.
Lemma Sigma_ring_ext :
Incl gen0 (Sigma_ring gen1) →
Incl gen1 (Sigma_ring gen0) →
Sigma_ring gen0 = Sigma_ring gen1.
Proof.
intros; apply Ext_equiv; split; now apply Sigma_ring_lub_alt.
Qed.
Lemma Lsyst_ext :
Incl gen0 (Lsyst gen1) →
Incl gen1 (Lsyst gen0) →
Lsyst gen0 = Lsyst gen1.
Proof.
intros; apply Ext_equiv; split; now apply Lsyst_lub_alt.
Qed.
Lemma Sigma_algebra_ext :
Incl gen0 (Sigma_algebra gen1) →
Incl gen1 (Sigma_algebra gen0) →
Sigma_algebra gen0 = Sigma_algebra gen1.
Proof.
intros; apply Ext_equiv; split; now apply Sigma_algebra_lub_alt.
Qed.
End Subset_systems_Facts4.
Section Subset_system_alt_Facts1.
Context {U : Type}.
Variable gen : (U → Prop) → Prop.
Lemma Algebra_equiv_alt :
Algebra gen = Gen is_Algebra gen.
Proof.
apply Ext_equiv; split; intros A HA.
induction HA.
now apply Gen_ni_gen.
1,2,3: intros SS HSS1 HSS2; rewrite <- HSS1.
apply Algebra_wEmpty.
apply Algebra_Compl; now apply (Algebra_monot gen SS).
apply Algebra_Union; now apply (Algebra_monot gen SS).
apply HA.
apply Algebra_idem.
apply Algebra_Gen.
Qed.
End Subset_system_alt_Facts1.
Section Subset_system_alt_Facts2.
Context {U : Type}.
Lemma is_Algebra_Inter_compat :
@IInter_compat U is_Algebra.
Proof.
intros Idx HIdx; rewrite Algebra_equiv; repeat split.
intros SS HSS; rewrite <- (HIdx SS HSS); apply Algebra_wEmpty.
intros A HA SS HSS; rewrite <- (HIdx SS HSS).
now apply Algebra_Compl, Algebra_Gen, HA.
intros A B HA HB SS HSS; rewrite <- (HIdx SS HSS).
now apply Algebra_Union; apply Algebra_Gen; [apply HA | apply HB].
Qed.
Variable gen0 gen1 : (U → Prop) → Prop.
Lemma Algebra_lub_alt_bis :
Incl gen0 (Algebra gen1) →
Incl (Algebra gen0) (Algebra gen1).
Proof.
intros; rewrite (Algebra_equiv_alt gen0), (Algebra_equiv_alt gen1).
apply (Gen_lub_alt is_Algebra).
apply is_Algebra_Inter_compat.
now rewrite <- Algebra_equiv_alt.
Qed.
End Subset_system_alt_Facts2.
Section Psyst_Facts.
Context {U : Type}.
Variable gen : (U → Prop) → Prop. Variable A0 : U → Prop.
Lemma Psyst_Nonempty :
Nonempty (Psyst gen A0).
Proof.
∃ A0; apply Psyst_Mem.
Qed.
Lemma Psyst_Inter_finite :
Inter_finite (Psyst gen A0).
Proof.
apply Inter_finite_equiv, Psyst_Inter.
Qed.
Lemma Psyst_Inter_monot_finite :
Inter_monot_finite (Psyst gen A0).
Proof.
apply Inter_finite_monot, Psyst_Inter_finite.
Qed.
Lemma Psyst_wEmpty :
Compl (Psyst gen A0) → wEmpty (Psyst gen A0).
Proof.
intros H; apply Nonempty_wEmpty; [easy | apply Psyst_Inter | ].
∃ A0; apply Psyst_Mem.
Qed.
Variable P : (U → Prop) → Prop.
Lemma is_Psyst_wEmpty :
is_Psyst P A0 → is_Psyst (fun A ⇒ P A ∨ A = emptyset) emptyset.
Proof.
intros H; rewrite Psyst_equiv in *; split.
now right.
now apply Inter_with_empty.
Qed.
End Psyst_Facts.
Section is_Semi_ring_Facts.
Context {U : Type}.
Variable P : (U → Prop) → Prop.
Lemma is_Semi_ring_wEmpty :
is_Semi_ring P → wEmpty P.
Proof.
now intros [H _].
Qed.
Lemma is_Semi_ring_Inter :
is_Semi_ring P → Inter P.
Proof.
now intros [_ [H _]].
Qed.
Lemma is_Semi_ring_Part_diff_finite :
is_Semi_ring P → Part_diff_finite P.
Proof.
now intros [_ [_ H]].
Qed.
Lemma is_Semi_ring_is_Psyst :
is_Semi_ring P → is_Psyst P emptyset.
Proof.
intros; apply Psyst_equiv; split.
now apply is_Semi_ring_wEmpty.
now apply is_Semi_ring_Inter.
Qed.
Lemma is_Semi_ring_Inter_finite :
is_Semi_ring P → Inter_finite P.
Proof.
intros; rewrite <- is_Semi_ring_is_Psyst; try easy.
apply Psyst_Inter_finite.
Qed.
Lemma is_Semi_ring_Inter_monot_finite :
is_Semi_ring P → Inter_monot_finite P.
Proof.
intros; rewrite <- is_Semi_ring_is_Psyst; try easy.
apply Psyst_Inter_monot_finite.
Qed.
End is_Semi_ring_Facts.
Section Ring_Facts1.
Context {U : Type}.
Variable gen : (U → Prop) → Prop.
Lemma Ring_Inter :
Inter (Ring gen).
Proof.
apply Diff_Inter, Ring_Diff.
Qed.
Lemma Ring_is_Psyst :
is_Psyst (Ring gen) emptyset.
Proof.
apply Psyst_equiv; split; try easy.
apply Ring_wEmpty.
apply Ring_Inter.
Qed.
Lemma Ring_Inter_finite :
Inter_finite (Ring gen).
Proof.
rewrite <- Ring_is_Psyst; apply Psyst_Inter_finite.
Qed.
Lemma Ring_Compl_loc :
Compl_loc (Ring gen).
Proof.
apply Diff_Compl_loc, Ring_Diff.
Qed.
Lemma Ring_Sym_diff :
Sym_diff (Ring gen).
Proof.
apply Sym_diff_Diff_equiv; [apply Ring_Union | apply Ring_Diff].
Qed.
Lemma Ring_Union_disj :
Union_disj (Ring gen).
Proof.
apply Union_Union_disj, Ring_Union.
Qed.
Lemma Ring_Inter_monot_finite :
Inter_monot_finite (Ring gen).
Proof.
apply Inter_finite_monot, Ring_Inter_finite.
Qed.
Lemma Ring_Union_finite :
Union_finite (Ring gen).
Proof.
apply Union_finite_equiv, Ring_Union.
Qed.
Lemma Ring_Union_monot_finite :
Union_monot_finite (Ring gen).
Proof.
apply Union_finite_monot, Ring_Union_finite.
Qed.
Lemma Ring_Union_disj_finite :
Union_disj_finite (Ring gen).
Proof.
apply Union_finite_disj, Ring_Union_finite.
Qed.
Variable P : (U → Prop) → Prop.
Lemma Ring_equiv_def :
is_Ring P ↔
(Nonempty P ∨ wEmpty P) ∧
(Diff P ∧ Union P ∨
Diff P ∧ Union_disj P ∨
Sym_diff P ∧ Inter P ∨
Compl_loc P ∧ Union_disj P ∧ Inter P).
Proof.
rewrite Ring_equiv; split.
intros [H1 H2]; repeat split.
now right.
now left.
intros [[H1 | H1] [[H2 H3] | [[H2 H3] | [[H2 H3] | [H2 [H3 H4]]]]]]; repeat split; try easy.
1,2,4,7: apply Nonempty_wEmpty_Diff; try easy.
1,4,9: now apply Sym_diff_Diff.
2,5,6,9: apply Union_disj_Union; try easy.
1,2,3,5,7: now apply Compl_loc_Diff.
1,2: now apply Sym_diff_Union.
Qed.
Lemma is_Psyst_Sym_diff_is_Ring :
∀ (A0 : U → Prop),
is_Psyst P A0 → Sym_diff P → is_Ring P.
Proof.
intros A0 H1 H2; rewrite Ring_equiv_def; split.
left; rewrite <- H1; apply Psyst_Nonempty.
right; right; left; split; try easy.
rewrite <- H1; apply Psyst_Inter.
Qed.
End Ring_Facts1.
Section Ring_Facts2.
Context {U : Type}.
Variable gen : (U → Prop) → Prop.
Lemma Incl_Psyst_Ring :
Incl (Psyst gen emptyset) (Ring gen).
Proof.
rewrite <- Ring_is_Psyst; apply Psyst_monot, Ring_Gen.
Qed.
Lemma Incl_Ring_Psyst :
let P := Psyst gen emptyset in
Sym_diff P → Incl (Ring gen) P.
Proof.
intros P H1; assert (H2 : is_Ring P).
apply Ring_equiv; repeat split.
apply Psyst_Mem.
apply Sym_diff_Diff; try easy; apply Psyst_Inter.
apply Sym_diff_Union; try easy; apply Psyst_Inter.
apply Ring_lub; [easy | apply Psyst_Gen].
Qed.
Lemma Ring_Psyst :
Ring (Psyst gen emptyset) = Ring gen.
Proof.
intros; apply Ext_equiv; split.
now apply Ring_lub_alt, Incl_Psyst_Ring.
apply Ring_monot, Psyst_Gen.
Qed.
End Ring_Facts2.
Section Ring_Facts3.
Context {U : Type}.
Variable gen : (U → Prop) → Prop.
Hypothesis H : is_Semi_ring gen.
Lemma Explicit_ring_Gen :
Incl gen (Union_disj_finite_closure gen).
Proof.
intros A HA.
∃ (repeat_1 A), 0; repeat split; try easy.
now rewrite union_finite_0.
apply disj_finite_0.
Qed.
Lemma Explicit_ring_wEmpty :
wEmpty (Union_disj_finite_closure gen).
Proof.
destruct H as [H1 _].
now apply Explicit_ring_Gen.
Qed.
Lemma Explicit_ring_Diff :
Diff (Union_disj_finite_closure gen).
Proof.
destruct H as [_ [H2 H3]].
now apply Diff_Union_disj_finite_closure.
Qed.
Lemma Explicit_ring_Union_disj :
Union_disj (Union_disj_finite_closure gen).
Proof.
apply Union_disj_Union_disj_finite_closure.
Qed.
Lemma Ring_explicit_aux1 :
Incl (Ring gen) (Union_disj_finite_closure gen).
Proof.
apply Ring_lub.
apply Ring_equiv_def; split.
right; apply Explicit_ring_wEmpty.
right; left; split; [apply Explicit_ring_Diff | apply Explicit_ring_Union_disj].
apply Explicit_ring_Gen.
Qed.
Lemma Ring_explicit_aux2 :
Incl (Union_finite_closure gen) (Ring gen).
Proof.
intros A [B [N [HB1 HB2]]].
rewrite HB2; apply Ring_Union_finite.
intros; now apply Ring_Gen, HB1.
Qed.
Lemma Ring_explicit_aux :
Ring gen = Union_disj_finite_closure gen ∧
Union_disj_finite_closure gen = Union_finite_closure gen.
Proof.
split; apply Ext_equiv; split.
2: apply Incl_trans with (Union_finite_closure gen).
5: apply Incl_trans with (Ring gen).
1,6: apply Ring_explicit_aux1.
1,3: apply Union_finite_closure_Incl.
1,2: apply Ring_explicit_aux2.
Qed.
Lemma Ring_explicit :
Ring gen = Union_disj_finite_closure gen.
Proof.
apply Ring_explicit_aux.
Qed.
Lemma Ring_explicit_alt :
Ring gen = Union_finite_closure gen.
Proof.
destruct Ring_explicit_aux as [H1 H2].
now rewrite H1.
Qed.
End Ring_Facts3.
Section Semi_algebra_Facts.
Context {U : Type}.
Variable gen : (U → Prop) → Prop.
Lemma is_Semi_algebra_equiv_def_Part_diff_finite :
is_Semi_algebra gen ↔ wFull gen ∧ Inter gen ∧ Part_diff_finite gen.
Proof.
split.
intros [H1 [H2 H3]]; repeat split; try easy.
now apply Part_compl_Part_diff_finite.
intros [H1 [H2 H3]]; repeat split; try easy.
now apply Part_diff_Part_compl_finite.
Qed.
Lemma is_Semi_algebra_equiv_def_Semi_ring :
is_Semi_algebra gen ↔ is_Semi_ring gen ∧ wFull gen.
Proof.
rewrite is_Semi_algebra_equiv_def_Part_diff_finite; unfold is_Semi_ring.
repeat split; try easy.
apply wFull_wEmpty_finite; try easy.
now apply Part_diff_Part_compl_finite.
Qed.
Lemma is_Semi_algebra_is_Semi_ring :
is_Semi_algebra gen → is_Semi_ring gen.
Proof.
now rewrite is_Semi_algebra_equiv_def_Semi_ring.
Qed.
End Semi_algebra_Facts.
Global Hint Resolve <- Ring_equiv : subset_systems.
Section Algebra_Facts1.
Context {U : Type}.
Variable gen : (U → Prop) → Prop.
Lemma Algebra_Diff :
Diff (Algebra gen).
Proof.
apply Union_Diff_equiv; auto with subset_systems.
Qed.
Local Hint Resolve Algebra_Diff : subset_systems.
Lemma Algebra_is_Ring :
is_Ring (Algebra gen).
Proof.
apply Ring_equiv; auto with subset_systems.
Qed.
Lemma Algebra_Compl_loc :
Compl_loc (Algebra gen).
Proof.
rewrite <- Algebra_is_Ring; apply Ring_Compl_loc.
Qed.
Lemma Algebra_Sym_diff :
Sym_diff (Algebra gen).
Proof.
rewrite <- Algebra_is_Ring; apply Ring_Sym_diff.
Qed.
Lemma Algebra_Inter :
Inter (Algebra gen).
Proof.
rewrite <- Algebra_is_Ring; apply Ring_Inter.
Qed.
Lemma Algebra_Union_disj :
Union_disj (Algebra gen).
Proof.
rewrite <- Algebra_is_Ring; apply Ring_Union_disj.
Qed.
Lemma Algebra_Inter_finite :
Inter_finite (Algebra gen).
Proof.
rewrite <- Algebra_is_Ring; apply Ring_Inter_finite.
Qed.
Lemma Algebra_Inter_monot_finite :
Inter_monot_finite (Algebra gen).
Proof.
rewrite <- Algebra_is_Ring; apply Ring_Inter_monot_finite.
Qed.
Lemma Algebra_Union_finite :
Union_finite (Algebra gen).
Proof.
rewrite <- Algebra_is_Ring; apply Ring_Union_finite.
Qed.
Lemma Algebra_Union_monot_finite :
Union_monot_finite (Algebra gen).
Proof.
rewrite <- Algebra_is_Ring; apply Ring_Union_monot_finite.
Qed.
Lemma Algebra_Union_disj_finite :
Union_disj_finite (Algebra gen).
Proof.
rewrite <- Algebra_is_Ring; apply Ring_Union_disj_finite.
Qed.
Lemma Algebra_wFull :
wFull (Algebra gen).
Proof.
apply wFull_wEmpty_equiv.
apply Algebra_Compl.
apply Algebra_wEmpty.
Qed.
Lemma Algebra_Compl_rev :
Compl_rev (Algebra gen).
Proof.
apply Compl_equiv, Algebra_Compl.
Qed.
Lemma Algebra_is_Psyst :
is_Psyst (Algebra gen) emptyset.
Proof.
rewrite <- Algebra_is_Ring; apply Ring_is_Psyst.
Qed.
Lemma Algebra_equiv_def :
is_Algebra gen ↔ wFull gen ∧ Diff gen.
Proof.
split.
intros H; rewrite <- H; split; [apply Algebra_wFull | apply Algebra_Diff].
intros [H1 H2]; assert (H3 : Compl gen) by now apply Compl_loc_Compl.
rewrite Algebra_equiv; repeat split; try easy.
now apply wFull_wEmpty_equiv.
now apply Union_Diff_equiv.
Qed.
End Algebra_Facts1.
Section Algebra_Facts2.
Context {U : Type}.
Variable gen : (U → Prop) → Prop.
Lemma Incl_Ring_Algebra :
Incl (Ring gen) (Algebra gen).
Proof.
rewrite <- Algebra_is_Ring; apply Ring_lub_alt.
intros A HA; now apply Ring_Gen, Algebra_Gen.
Qed.
Lemma Incl_Psyst_Algebra :
Incl (Psyst gen emptyset) (Algebra gen).
Proof.
apply Incl_trans with (Ring gen).
apply Incl_Psyst_Ring.
apply Incl_Ring_Algebra.
Qed.
Lemma Upgrade_Ring_is_Algebra :
∀ (P : (U → Prop) → Prop),
is_Ring P →
(wFull P ∨ Compl P) →
is_Algebra P.
Proof.
intros P H1 [H2 | H2].
rewrite Algebra_equiv_def; now rewrite Ring_equiv in H1.
rewrite Algebra_equiv; repeat split.
rewrite <- H1; apply Ring_wEmpty.
1,2: now rewrite Ring_equiv in H1.
Qed.
Lemma Algebra_of_Ring :
Algebra (Ring gen) = Algebra gen.
Proof.
apply Ext_equiv; split.
rewrite <- (Algebra_idem gen).
apply Algebra_monot, Incl_Ring_Algebra.
apply Algebra_monot, Ring_Gen.
Qed.
Lemma Upgrade_Ring_Algebra :
(wFull (Ring gen) ∨ Compl (Ring gen)) →
Ring gen = Algebra gen.
Proof.
intros H.
generalize (Upgrade_Ring_is_Algebra (Ring gen)); intros H3.
rewrite <- H3; try easy.
apply Algebra_of_Ring.
apply Ring_idem.
Qed.
Lemma Incl_Algebra_Psyst :
let P := Psyst gen emptyset in
Compl P → Incl (Algebra gen) P.
Proof.
intros P H1; assert (H2 : is_Algebra P).
apply Algebra_equiv; repeat split; try easy.
now apply Psyst_wEmpty.
apply Union_Inter_equiv; [easy | apply Psyst_Inter].
apply Algebra_lub; [easy | apply Psyst_Gen].
Qed.
Lemma Algebra_Psyst :
Algebra (Psyst gen emptyset) = Algebra gen.
Proof.
apply Ext_equiv; split.
now apply Algebra_lub_alt, Incl_Psyst_Algebra.
apply Algebra_monot, Psyst_Gen.
Qed.
End Algebra_Facts2.
Section Algebra_Facts3.
Context {U : Type}.
Variable gen : (U → Prop) → Prop.
Hypothesis H : is_Semi_algebra gen.
Lemma Algebra_explicit_aux :
Algebra gen = Union_disj_finite_closure gen ∧
Union_disj_finite_closure gen = Union_finite_closure gen.
Proof.
rewrite is_Semi_algebra_equiv_def_Semi_ring in H.
destruct H as [H1 H2]; clear H.
destruct (Ring_explicit_aux gen H1) as [H3 H4].
split; try easy; clear H4.
rewrite <- H3; symmetry; rewrite Upgrade_Ring_Algebra; try easy.
left; now apply Ring_Gen.
Qed.
Lemma Algebra_explicit :
Algebra gen = Union_disj_finite_closure gen.
Proof.
apply Algebra_explicit_aux.
Qed.
Lemma Algebra_explicit_alt :
Algebra gen = Union_finite_closure gen.
Proof.
destruct Algebra_explicit_aux as [H1 H2].
now rewrite H1.
Qed.
End Algebra_Facts3.
Section Monotone_class_Facts1.
Context {U : Type}.
Variable gen : (U → Prop) → Prop.
Lemma Monotone_class_Inter_monot_finite :
Inter_monot_finite (Monotone_class gen).
Proof.
apply Inter_monot_seq_finite, Monotone_class_Inter_monot_seq.
Qed.
Lemma Monotone_class_Union_monot_finite :
Union_monot_finite (Monotone_class gen).
Proof.
apply Union_monot_seq_finite, Monotone_class_Union_monot_seq.
Qed.
End Monotone_class_Facts1.
Section Monotone_class_Facts2.
Context {U : Type}.
Variable gen : (U → Prop) → Prop.
Hypothesis H : Diff gen.
Definition Monotone_class_diff : (U → Prop) → (U → Prop) → Prop :=
fun A B ⇒ Monotone_class gen (diff A B) ∧ Monotone_class gen (diff B A).
Lemma Monotone_class_diff_sym :
∀ (A B : U → Prop),
Monotone_class gen B → Monotone_class_diff B A → Monotone_class_diff A B.
Proof.
intros A B HB [H1 H2]; now split.
Qed.
Lemma Monotone_class_diff_is_Monotone_class :
∀ (A : U → Prop), is_Monotone_class (Monotone_class_diff A).
Proof.
intros A; apply Monotone_class_equiv; split; intros B HB1 HB2; split.
rewrite diff_inter_seq_r; apply Monotone_class_Union_monot_seq.
now apply diff_decr_seq_compat_l.
intros n; now destruct (HB2 n).
rewrite diff_inter_seq_distr_l; apply Monotone_class_Inter_monot_seq.
now apply diff_decr_seq_compat_r.
intros n; now destruct (HB2 n).
rewrite diff_union_seq_r; apply Monotone_class_Inter_monot_seq.
now apply diff_incr_seq_compat_l.
intros n; now destruct (HB2 n).
rewrite diff_union_seq_distr_l; apply Monotone_class_Union_monot_seq.
now apply diff_incr_seq_compat_r.
intros n; now destruct (HB2 n).
Qed.
Lemma Diff_Monotone_class_aux1 :
∀ A, gen A → Incl (Monotone_class gen) (Monotone_class_diff A).
Proof.
intros; apply Monotone_class_lub.
apply Monotone_class_diff_is_Monotone_class.
intros B HB; split; apply Monotone_class_Gen; now apply H.
Qed.
Lemma Diff_Monotone_class_aux2 :
∀ A,
Monotone_class gen A →
Incl (Monotone_class gen) (Monotone_class_diff A).
Proof.
intros; apply Monotone_class_lub.
apply Monotone_class_diff_is_Monotone_class.
intros B HB; apply Monotone_class_diff_sym.
now apply Monotone_class_Gen.
now apply Diff_Monotone_class_aux1.
Qed.
Lemma Diff_Monotone_class :
Diff (Monotone_class gen).
Proof.
intros A B HA HB; now apply Diff_Monotone_class_aux2.
Qed.
End Monotone_class_Facts2.
Section Lsyst_Facts1.
Context {U : Type}.
Variable gen : (U → Prop) → Prop.
Lemma Lsyst_wEmpty :
wEmpty (Lsyst gen).
Proof.
apply wFull_wEmpty_equiv.
apply Lsyst_Compl.
apply Lsyst_wFull.
Qed.
Lemma Lsyst_Compl_loc :
Compl_loc (Lsyst gen).
Proof.
apply Union_disj_seq_Compl_loc.
apply Lsyst_wFull.
apply Lsyst_Compl.
apply Lsyst_Union_disj_seq.
Qed.
Lemma Lsyst_Union_monot_seq :
Union_monot_seq (Lsyst gen).
Proof.
apply Union_disj_monot_seq.
apply Lsyst_Compl_loc.
apply Lsyst_Union_disj_seq.
Qed.
Lemma Lsyst_Inter_monot_seq :
Inter_monot_seq (Lsyst gen).
Proof.
apply Union_Inter_monot_seq_equiv.
apply Lsyst_Compl.
apply Lsyst_Union_monot_seq.
Qed.
Lemma Lsyst_is_Monotone_class :
is_Monotone_class (Lsyst gen).
Proof.
apply Monotone_class_equiv; split.
apply Lsyst_Inter_monot_seq.
apply Lsyst_Union_monot_seq.
Qed.
Lemma Lsyst_Union_monot_finite :
Union_monot_finite (Lsyst gen).
Proof.
rewrite <- Lsyst_is_Monotone_class; apply Monotone_class_Union_monot_finite.
Qed.
Lemma Lsyst_Inter_monot_finite :
Inter_monot_finite (Lsyst gen).
Proof.
rewrite <- Lsyst_is_Monotone_class; apply Monotone_class_Inter_monot_finite.
Qed.
Lemma Lsyst_Compl_rev :
Compl_rev (Lsyst gen).
Proof.
apply Compl_equiv, Lsyst_Compl.
Qed.
Lemma Lsyst_Union_disj_finite :
Union_disj_finite (Lsyst gen).
Proof.
apply Union_disj_seq_finite.
apply Lsyst_wEmpty.
apply Lsyst_Union_disj_seq.
Qed.
Lemma Lsyst_Union_disj :
Union_disj (Lsyst gen).
Proof.
apply Union_disj_finite_equiv, Lsyst_Union_disj_finite.
Qed.
Lemma Lsyst_equiv_def :
is_Lsyst gen ↔ wFull gen ∧ Compl_loc gen ∧ Union_monot_seq gen.
Proof.
split.
intros H; rewrite <- H; repeat split;
[apply Lsyst_wFull | apply Lsyst_Compl_loc | apply Lsyst_Union_monot_seq].
intros [H1 [H2 H3]]; assert (H4 : Compl gen) by now apply Compl_loc_Compl.
rewrite Lsyst_equiv; repeat split; try easy.
now apply Union_monot_disj_seq_alt.
Qed.
End Lsyst_Facts1.
Section Lsyst_Facts2.
Context {U : Type}.
Variable gen : (U → Prop) → Prop.
Lemma Incl_Monotone_class_Lsyst :
Incl (Monotone_class gen) (Lsyst gen).
Proof.
rewrite <- Lsyst_is_Monotone_class; apply Monotone_class_lub_alt.
intros A HA; now apply Monotone_class_Gen, Lsyst_Gen.
Qed.
Lemma Incl_Lsyst_Monotone_class_aux :
wFull (Monotone_class gen) → Compl (Monotone_class gen) →
Union_disj_seq (Monotone_class gen) →
Incl (Lsyst gen) (Monotone_class gen).
Proof.
intros H1 H2 H3; assert (H4 : is_Lsyst (Monotone_class gen)) by now apply Lsyst_equiv.
apply Lsyst_lub; [easy | apply Monotone_class_Gen].
Qed.
Lemma Incl_Lsyst_Monotone_class :
wFull (Monotone_class gen) → Compl_loc (Monotone_class gen) →
Incl (Lsyst gen) (Monotone_class gen).
Proof.
intros H1 H2; assert (H3 : Compl (Monotone_class gen)) by now apply Compl_loc_Compl.
apply Incl_Lsyst_Monotone_class_aux; try easy.
apply Union_monot_disj_seq_alt; try easy; apply Monotone_class_Union_monot_seq.
Qed.
Lemma Lsyst_Monotone_class :
Lsyst (Monotone_class gen) = Lsyst gen.
Proof.
apply Ext_equiv; split.
apply Lsyst_lub_alt, Incl_Monotone_class_Lsyst.
apply Lsyst_monot, Monotone_class_Gen.
Qed.
End Lsyst_Facts2.
Section Lsyst_Facts3.
Context {U : Type}.
Variable gen : (U → Prop) → Prop.
Hypothesis H : Inter gen.
Definition Lsyst_inter : (U → Prop) → (U → Prop) → Prop :=
fun A B ⇒ Lsyst gen B ∧ Lsyst gen (inter A B).
Lemma Lsyst_inter_sym :
∀ (A B : U → Prop),
Lsyst gen A → Lsyst_inter A B → Lsyst_inter B A.
Proof.
intros A B HA [H1 H2]; now rewrite inter_comm in H2.
Qed.
Lemma Lsyst_inter_is_Lsyst :
∀ (A : U → Prop), Lsyst gen A → is_Lsyst (Lsyst_inter A).
Proof.
intros A HA; apply Lsyst_equiv_def; split; [ | split].
split; [apply Lsyst_wFull | now rewrite inter_full_r].
intros B C HBC [HB1 HB2] [HC1 HC2]; split.
now apply Lsyst_Compl_loc.
rewrite inter_diff_distr_l; apply Lsyst_Compl_loc;
try easy; now apply inter_monot_r.
intros B HB1 HB2; split.
apply Lsyst_Union_monot_seq; try easy; intros n; now destruct (HB2 n).
rewrite inter_union_seq_distr_l; apply Lsyst_Union_monot_seq.
now apply inter_incr_seq_compat_l.
intros; apply HB2.
Qed.
Lemma Inter_Lsyst_aux1 :
∀ (A : U → Prop), gen A → Incl (Lsyst gen) (Lsyst_inter A).
Proof.
intros; apply Lsyst_lub.
apply Lsyst_inter_is_Lsyst; now apply Lsyst_Gen.
intros B HB; split; apply Lsyst_Gen; [easy | now apply H].
Qed.
Lemma Inter_Lsyst_aux2 :
∀ A, Lsyst gen A → Incl (Lsyst gen) (Lsyst_inter A).
Proof.
intros; apply Lsyst_lub.
now apply Lsyst_inter_is_Lsyst.
intros B HB; apply Lsyst_inter_sym; try easy.
now apply Lsyst_Gen.
now apply Inter_Lsyst_aux1.
Qed.
Lemma Inter_Lsyst :
Inter (Lsyst gen).
Proof.
intros A B HA HB; now apply Inter_Lsyst_aux2.
Qed.
End Lsyst_Facts3.
Section Sigma_algebra_Facts1.
Context {U : Type}.
Variable gen : (U → Prop) → Prop.
Lemma Sigma_algebra_Union :
Union (Sigma_algebra gen).
Proof.
apply Union_seq_Union, Sigma_algebra_Union_seq.
Qed.
Lemma Sigma_algebra_is_Algebra :
is_Algebra (Sigma_algebra gen).
Proof.
apply Algebra_equiv; repeat split.
apply Sigma_algebra_wEmpty.
apply Sigma_algebra_Compl.
apply Sigma_algebra_Union.
Qed.
Lemma Sigma_algebra_wFull :
wFull (Sigma_algebra gen).
Proof.
rewrite <- Sigma_algebra_is_Algebra; apply Algebra_wFull.
Qed.
Lemma Sigma_algebra_Compl_rev :
Compl_rev (Sigma_algebra gen).
Proof.
apply Compl_equiv, Sigma_algebra_Compl.
Qed.
Lemma Sigma_algebra_Compl_loc :
Compl_loc (Sigma_algebra gen).
Proof.
rewrite <- Sigma_algebra_is_Algebra; apply Algebra_Compl_loc.
Qed.
Lemma Sigma_algebra_Diff :
Diff (Sigma_algebra gen).
Proof.
rewrite <- Sigma_algebra_is_Algebra; apply Algebra_Diff.
Qed.
Lemma Sigma_algebra_Sym_diff :
Sym_diff (Sigma_algebra gen).
Proof.
rewrite <- Sigma_algebra_is_Algebra; apply Algebra_Sym_diff.
Qed.
Lemma Sigma_algebra_Inter :
Inter (Sigma_algebra gen).
Proof.
rewrite <- Sigma_algebra_is_Algebra; apply Algebra_Inter.
Qed.
Lemma Sigma_algebra_Union_disj :
Union_disj (Sigma_algebra gen).
Proof.
rewrite <- Sigma_algebra_is_Algebra; apply Algebra_Union_disj.
Qed.
Lemma Sigma_algebra_Inter_finite :
Inter_finite (Sigma_algebra gen).
Proof.
rewrite <- Sigma_algebra_is_Algebra; apply Algebra_Inter_finite.
Qed.
Lemma Sigma_algebra_Inter_monot_finite :
Inter_monot_finite (Sigma_algebra gen).
Proof.
rewrite <- Sigma_algebra_is_Algebra; apply Algebra_Inter_monot_finite.
Qed.
Lemma Sigma_algebra_Union_finite :
Union_finite (Sigma_algebra gen).
Proof.
rewrite <- Sigma_algebra_is_Algebra; apply Algebra_Union_finite.
Qed.
Lemma Sigma_algebra_Union_monot_finite :
Union_monot_finite (Sigma_algebra gen).
Proof.
rewrite <- Sigma_algebra_is_Algebra; apply Algebra_Union_monot_finite.
Qed.
Lemma Sigma_algebra_Union_disj_finite :
Union_disj_finite (Sigma_algebra gen).
Proof.
rewrite <- Sigma_algebra_is_Algebra; apply Algebra_Union_disj_finite.
Qed.
Lemma Sigma_algebra_Inter_seq :
Inter_seq (Sigma_algebra gen).
Proof.
apply Union_Inter_seq_equiv.
apply Sigma_algebra_Compl.
apply Sigma_algebra_Union_seq.
Qed.
Lemma Sigma_algebra_Inter_monot_seq :
Inter_monot_seq (Sigma_algebra gen).
Proof.
apply Inter_seq_monot, Sigma_algebra_Inter_seq.
Qed.
Lemma Sigma_algebra_Union_monot_seq :
Union_monot_seq (Sigma_algebra gen).
Proof.
apply Union_seq_monot, Sigma_algebra_Union_seq.
Qed.
Lemma Sigma_algebra_Union_disj_seq :
Union_disj_seq (Sigma_algebra gen).
Proof.
apply Union_seq_disj, Sigma_algebra_Union_seq.
Qed.
Lemma Sigma_algebra_gen_remove :
∀ A, Sigma_algebra gen A →
Incl (Sigma_algebra (add gen A)) (Sigma_algebra gen).
Proof.
intros A HA B HB; induction HB as [B [ | HB] | | | ].
now apply Sigma_algebra_Gen.
now rewrite HB.
apply Sigma_algebra_wEmpty.
now apply Sigma_algebra_Compl.
now apply Sigma_algebra_Union_seq.
Qed.
Lemma Sigma_algebra_gen_remove_alt :
∀ A, Sigma_algebra gen A → Incl (add gen A) (Sigma_algebra gen).
Proof.
intros A HA; apply Incl_trans with (2 := Sigma_algebra_gen_remove _ HA).
apply Sigma_algebra_Gen.
Qed.
Lemma Sigma_algebra_gen_remove_full :
Incl (add gen fullset) (Sigma_algebra gen).
Proof.
apply Sigma_algebra_gen_remove_alt, Sigma_algebra_wFull.
Qed.
Lemma Sigma_algebra_gen_add_eq :
∀ A, Sigma_algebra gen A → Sigma_algebra (add gen A) = Sigma_algebra gen.
Proof.
intros; apply Ext_equiv; split.
now apply Sigma_algebra_gen_remove.
apply Sigma_algebra_monot, incl_add_r.
Qed.
End Sigma_algebra_Facts1.
Section Sigma_algebra_Facts2.
Context {U1 U2 : Type}. Variable genU1 : (U1 → Prop) → Prop. Variable genU2 : (U2 → Prop) → Prop.
Variable f : U1 → U2.
Lemma is_Sigma_algebra_Image : is_Sigma_algebra (Image f (Sigma_algebra genU1)).
Proof.
apply Sigma_algebra_equiv; repeat split.
apply Sigma_algebra_wEmpty.
intros A2 HA2; apply Sigma_algebra_Compl; easy.
intros A2 HA2; apply Sigma_algebra_Union_seq; easy.
Qed.
Lemma is_Sigma_algebra_Preimage :
is_Sigma_algebra (Preimage f (Sigma_algebra genU2)).
Proof.
apply Sigma_algebra_equiv; repeat split.
unfold wEmpty; rewrite <- (preimage_emptyset f).
apply Im, Sigma_algebra_wEmpty.
intros A1 [A2 HA2]; rewrite <- preimage_compl.
apply Im, Sigma_algebra_Compl; easy.
intros A1 HA1; unfold Preimage in *; rewrite image_eq in HA1.
destruct (choice (fun n A2 ⇒
Sigma_algebra genU2 A2 ∧ A1 n = preimage f A2) HA1) as [A2 HA2].
assert (H : union_seq A1 = preimage f (union_seq A2)).
rewrite preimage_union_seq_distr; f_equal.
apply subset_seq_ext; intros n; rewrite (proj2 (HA2 n)); easy.
rewrite H; apply Im; apply Sigma_algebra_Union_seq; intro; apply HA2.
Qed.
End Sigma_algebra_Facts2.
Section Sigma_algebra_Facts3.
Context {U1 U2 : Type}. Variable genU1 : (U1 → Prop) → Prop. Variable genU2 : (U2 → Prop) → Prop.
Variable f : U1 → U2.
Lemma Sigma_algebra_Preimage :
Sigma_algebra (Preimage f genU2) = Preimage f (Sigma_algebra genU2).
Proof.
apply Ext_equiv; split.
rewrite <- is_Sigma_algebra_Preimage.
apply Sigma_algebra_monot, Preimage_monot, Sigma_algebra_Gen.
apply Incl_Image_Preimage_Incl, Sigma_algebra_lub.
apply is_Sigma_algebra_Image.
apply Preimage_Incl_Incl_Image, Sigma_algebra_Gen.
Qed.
End Sigma_algebra_Facts3.
Section Sigma_algebra_Facts4.
Context {U : Type}.
Variable gen : (U → Prop) → Prop.
Lemma Sigma_algebra_is_Psyst :
is_Psyst (Sigma_algebra gen) emptyset.
Proof.
rewrite <- Sigma_algebra_is_Algebra; apply Algebra_is_Psyst.
Qed.
Lemma Incl_Psyst_Sigma_algebra :
Incl (Psyst gen emptyset) (Sigma_algebra gen).
Proof.
rewrite <- Sigma_algebra_is_Psyst; apply Psyst_lub_alt.
intros A HA; now apply Psyst_Gen, Sigma_algebra_Gen.
Qed.
Lemma Incl_Sigma_algebra_Psyst_aux :
let P := Psyst gen emptyset in
Compl P → Union_seq P →
Incl (Sigma_algebra gen) P.
Proof.
intros P H1 H2; assert (H3 : is_Sigma_algebra P).
apply Sigma_algebra_equiv; repeat split; try easy.
now apply Psyst_wEmpty.
apply Sigma_algebra_lub; [easy | apply Psyst_Gen].
Qed.
Lemma Incl_Sigma_algebra_Psyst :
let P := Psyst gen emptyset in
Compl P → Union_disj_seq P →
Incl (Sigma_algebra gen) P.
Proof.
intros; apply Incl_Sigma_algebra_Psyst_aux; try easy.
apply Union_disj_seq_Union_seq_alt; try easy.
apply Psyst_Inter.
Qed.
Lemma Sigma_algebra_Psyst :
Sigma_algebra (Psyst gen emptyset) = Sigma_algebra gen.
Proof.
apply Ext_equiv; split.
now apply Sigma_algebra_lub_alt, Incl_Psyst_Sigma_algebra.
apply Sigma_algebra_monot, Psyst_Gen.
Qed.
Lemma Incl_Algebra_Sigma_algebra :
Incl (Algebra gen) (Sigma_algebra gen).
Proof.
rewrite <- Sigma_algebra_is_Algebra; apply Algebra_lub_alt.
intros A HA; now apply Algebra_Gen, Sigma_algebra_Gen.
Qed.
Lemma Incl_Sigma_algebra_Algebra_aux :
Union_seq (Algebra gen) → Incl (Sigma_algebra gen) (Algebra gen).
Proof.
intros H1; assert (H2 : is_Sigma_algebra (Algebra gen)).
apply Sigma_algebra_equiv; repeat split; try easy.
apply Algebra_wEmpty.
apply Algebra_Compl.
apply Sigma_algebra_lub; [easy | apply Algebra_Gen].
Qed.
Lemma Incl_Sigma_algebra_Algebra :
Union_monot_seq (Algebra gen) → Incl (Sigma_algebra gen) (Algebra gen).
Proof.
intros; apply Incl_Sigma_algebra_Algebra_aux,
Union_monot_seq_Union_seq_alt; try easy.
apply Algebra_Compl.
apply Algebra_Union.
Qed.
Lemma Sigma_algebra_Algebra :
Sigma_algebra (Algebra gen) = Sigma_algebra gen.
Proof.
apply Ext_equiv; split.
apply Sigma_algebra_lub_alt, Incl_Algebra_Sigma_algebra.
apply Sigma_algebra_monot, Algebra_Gen.
Qed.
Lemma Sigma_algebra_is_Monotone_class :
is_Monotone_class (Sigma_algebra gen).
Proof.
apply Monotone_class_equiv; split.
apply Sigma_algebra_Inter_monot_seq.
apply Sigma_algebra_Union_monot_seq.
Qed.
Lemma Incl_Monotone_class_Sigma_algebra :
Incl (Monotone_class gen) (Sigma_algebra gen).
Proof.
rewrite <- Sigma_algebra_is_Monotone_class; apply Monotone_class_lub_alt.
intros A HA; now apply Monotone_class_Gen, Sigma_algebra_Gen.
Qed.
Lemma Incl_Sigma_algebra_Monotone_class_aux :
wEmpty (Monotone_class gen) → Compl (Monotone_class gen) →
Union_seq (Monotone_class gen) →
Incl (Sigma_algebra gen) (Monotone_class gen).
Proof.
intros H1 H2 H3; assert (H4 : is_Sigma_algebra (Monotone_class gen)).
apply Sigma_algebra_equiv; now repeat split.
apply Sigma_algebra_lub; [easy | apply Monotone_class_Gen].
Qed.
Lemma Incl_Sigma_algebra_Monotone_class :
wEmpty (Monotone_class gen) → Compl (Monotone_class gen) →
Union (Monotone_class gen) →
Incl (Sigma_algebra gen) (Monotone_class gen).
Proof.
intros; apply Incl_Sigma_algebra_Monotone_class_aux; try easy.
apply Union_monot_seq_Union_seq_alt; try easy.
apply Monotone_class_Union_monot_seq.
Qed.
Lemma Sigma_algebra_Monotone_class :
Sigma_algebra (Monotone_class gen) = Sigma_algebra gen.
Proof.
apply Ext_equiv; split.
apply Sigma_algebra_lub_alt, Incl_Monotone_class_Sigma_algebra.
apply Sigma_algebra_monot, Monotone_class_Gen.
Qed.
Lemma Sigma_algebra_is_Lsyst :
is_Lsyst (Sigma_algebra gen).
Proof.
apply Lsyst_equiv; repeat split.
apply Sigma_algebra_wFull.
apply Sigma_algebra_Compl.
apply Sigma_algebra_Union_disj_seq.
Qed.
Lemma Incl_Lsyst_Sigma_algebra :
Incl (Lsyst gen) (Sigma_algebra gen).
Proof.
rewrite <- Sigma_algebra_is_Lsyst; apply Lsyst_lub_alt.
intros A HA; now apply Lsyst_Gen, Sigma_algebra_Gen.
Qed.
Lemma Incl_Sigma_algebra_Lsyst_aux :
Union_seq (Lsyst gen) →
Incl (Sigma_algebra gen) (Lsyst gen).
Proof.
intros H1; assert (H2 : is_Sigma_algebra (Lsyst gen)).
apply Sigma_algebra_equiv; repeat split; try easy.
apply Lsyst_wEmpty.
apply Lsyst_Compl.
apply Sigma_algebra_lub; [easy | apply Lsyst_Gen].
Qed.
Lemma Incl_Sigma_algebra_Lsyst :
Inter (Lsyst gen) →
Incl (Sigma_algebra gen) (Lsyst gen).
Proof.
intros; apply Incl_Sigma_algebra_Lsyst_aux.
apply Union_disj_seq_Union_seq_alt; try easy.
apply Lsyst_Compl.
apply Lsyst_Union_disj_seq.
Qed.
Lemma Sigma_algebra_Lsyst :
Sigma_algebra (Lsyst gen) = Sigma_algebra gen.
Proof.
apply Ext_equiv; split.
apply Sigma_algebra_lub_alt, Incl_Lsyst_Sigma_algebra.
apply Sigma_algebra_monot, Lsyst_Gen.
Qed.
Lemma Psyst_Lsyst_is_Sigma_algebra :
∀ (A0 : U → Prop),
is_Psyst gen A0 → is_Lsyst gen → is_Sigma_algebra gen.
Proof.
intros A0 H1 H2; unfold is_Sigma_algebra.
rewrite <- H2 at 2; rewrite Psyst_equiv in H1.
apply Ext_equiv; split.
apply Incl_Sigma_algebra_Lsyst; now rewrite H2.
apply Incl_Lsyst_Sigma_algebra.
Qed.
Lemma Algebra_Monotone_class_is_Sigma_algebra :
is_Algebra gen → is_Monotone_class gen → is_Sigma_algebra gen.
Proof.
intros H1 H2; unfold is_Sigma_algebra.
rewrite <- H2 at 2; rewrite Algebra_equiv in H1.
apply Ext_equiv; split.
apply Incl_Sigma_algebra_Monotone_class; now rewrite H2.
apply Incl_Monotone_class_Sigma_algebra.
Qed.
End Sigma_algebra_Facts4.
Section Dynkin_pi_lambda_Theorem.
Context {U : Type}.
Variable gen : (U → Prop) → Prop.
Lemma Lsyst_Psyst_Inter :
∀ (A0 : U → Prop),
Inter (Lsyst (Psyst gen A0)).
Proof.
intros; apply Inter_Lsyst, Psyst_Inter.
Qed.
Lemma Lsyst_Psyst_is_Psyst :
∀ (A0 : U → Prop),
is_Psyst (Lsyst (Psyst gen A0)) A0.
Proof.
intros; apply Psyst_equiv; split.
apply Lsyst_Gen, Psyst_Mem.
apply Lsyst_Psyst_Inter.
Qed.
Theorem Dynkin_pi_lambda :
∀ (A0 : U → Prop),
Sigma_algebra (Psyst gen A0) = Lsyst (Psyst gen A0).
Proof.
intros A0; rewrite <- Sigma_algebra_Lsyst.
apply (Psyst_Lsyst_is_Sigma_algebra _ A0).
apply Lsyst_Psyst_is_Psyst.
apply Lsyst_idem.
Qed.
Theorem Dynkin_pi_lambda_Prop :
∀ (P : (U → Prop) → Prop) (A0 : U → Prop),
is_Lsyst P →
Incl (Psyst gen A0) P → Incl (Sigma_algebra gen) P.
Proof.
intros P A0 H1 H2; rewrite <- H1.
apply Incl_trans with (Sigma_algebra (Psyst gen A0)).
apply Sigma_algebra_monot, Psyst_Gen.
rewrite Dynkin_pi_lambda.
now apply Lsyst_monot.
Qed.
End Dynkin_pi_lambda_Theorem.
Section Monotone_class_Theorem.
Context {U : Type}.
Variable gen : (U → Prop) → Prop.
Lemma Monotone_class_Algebra_wFull :
wFull (Monotone_class (Algebra gen)).
Proof.
apply Monotone_class_Gen, Algebra_wFull.
Qed.
Lemma Monotone_class_Algebra_Diff :
Diff (Monotone_class (Algebra gen)).
Proof.
apply Diff_Monotone_class, Algebra_Diff.
Qed.
Lemma Monotone_class_Algebra_is_Algebra :
is_Algebra (Monotone_class (Algebra gen)).
Proof.
apply Algebra_equiv_def; repeat split.
apply Monotone_class_Algebra_wFull.
apply Monotone_class_Algebra_Diff.
Qed.
Theorem monotone_class :
Sigma_algebra (Algebra gen) = Monotone_class (Algebra gen).
Proof.
rewrite <- Sigma_algebra_Monotone_class.
apply Algebra_Monotone_class_is_Sigma_algebra.
apply Monotone_class_Algebra_is_Algebra.
apply Monotone_class_idem.
Qed.
Theorem monotone_class_Prop :
∀ (P : (U → Prop) → Prop),
is_Monotone_class P →
Incl (Algebra gen) P → Incl (Sigma_algebra gen) P.
Proof.
intros P H1 H2; rewrite <- H1.
apply Incl_trans with (Sigma_algebra (Algebra gen)).
apply Sigma_algebra_monot, Algebra_Gen.
rewrite monotone_class.
now apply Monotone_class_monot.
Qed.
End Monotone_class_Theorem.
Section Gen_Prod_Def0.
Context {U1 U2 : Type}.
Variable genU1 : (U1 → Prop) → Prop. Variable genU2 : (U2 → Prop) → Prop.
Definition Prod_Sigma_algebra : (U1 × U2 → Prop) → Prop :=
Prod (Sigma_algebra genU1) (Sigma_algebra genU2).
Definition Sigma_algebra_Prod : (U1 × U2 → Prop) → Prop :=
Sigma_algebra Prod_Sigma_algebra.
Definition Gen_Prod : (U1 × U2 → Prop) → Prop :=
Prod (add genU1 fullset) (add genU2 fullset).
End Gen_Prod_Def0.
Section Gen_Prod_Def1.
Context {U : Type}.
Variable genU : (U → Prop) → Prop.
Definition Gen_Prod_diag : (U × U → Prop) → Prop := Gen_Prod genU genU.
End Gen_Prod_Def1.
Section Prod_Sigma_algebra_Facts1.
Context {U1 U2 : Type}. Variable genU1 : (U1 → Prop) → Prop. Variable genU2 : (U2 → Prop) → Prop.
Let genU1xU2 := Gen_Prod genU1 genU2.
Lemma Sigma_algebra_prod_alt :
∀ A1 A2, Sigma_algebra genU1 A1 → Sigma_algebra genU2 A2 →
Sigma_algebra_Prod genU1 genU2 (prod A1 A2).
Proof.
intros; apply Sigma_algebra_Gen; now ∃ A1, A2.
Qed.
Lemma Sigma_algebra_prod_full_r :
∀ A1, Sigma_algebra genU1 A1 → Sigma_algebra genU1xU2 (prod A1 fullset).
Proof.
intros A1 HA1; induction HA1 as [A1 HA1 | | | ].
apply Sigma_algebra_Gen; ∃ A1, fullset; repeat split;
[now apply incl_add_r | apply add_in].
rewrite prod_empty_l; apply Sigma_algebra_wEmpty.
rewrite prod_compl_full; now apply Sigma_algebra_Compl.
rewrite prod_union_seq_full; now apply Sigma_algebra_Union_seq.
Qed.
Lemma Sigma_algebra_prod_full_l :
∀ A2, Sigma_algebra genU2 A2 → Sigma_algebra genU1xU2 (prod fullset A2).
Proof.
intros A2 HA2; induction HA2 as [A2 HA2 | | | ].
apply Sigma_algebra_Gen; ∃ fullset, A2; repeat split;
[apply add_in | now apply incl_add_r].
rewrite prod_empty_r; apply Sigma_algebra_wEmpty.
rewrite prod_full_compl; now apply Sigma_algebra_Compl.
rewrite prod_full_union_seq; now apply Sigma_algebra_Union_seq.
Qed.
Lemma Sigma_algebra_prod :
∀ A1 A2, Sigma_algebra genU1 A1 → Sigma_algebra genU2 A2 →
Sigma_algebra genU1xU2 (prod A1 A2).
Proof.
intros; rewrite prod_equiv; apply Sigma_algebra_Inter.
now apply Sigma_algebra_prod_full_r.
now apply Sigma_algebra_prod_full_l.
Qed.
Lemma Gen_Prod_is_Prod_Sigma_algebra :
Incl genU1xU2 (Prod_Sigma_algebra genU1 genU2).
Proof.
apply Prod_monot;
(apply incl_add_l; split;
[apply Sigma_algebra_Gen | apply Sigma_algebra_wFull]).
Qed.
Lemma Sigma_algebra_Prod_eq :
Sigma_algebra_Prod genU1 genU2 = Sigma_algebra genU1xU2.
Proof.
apply Sigma_algebra_ext.
intros A [A1 [A2 [HA1 [HA2 HA]]]]; rewrite HA; now apply Sigma_algebra_prod.
apply Incl_trans with (2 := Sigma_algebra_Gen _), Gen_Prod_is_Prod_Sigma_algebra.
Qed.
End Prod_Sigma_algebra_Facts1.
Section Prod_Sigma_algebra_Facts2.
Context {U1 U2 : Type}. Variable genU1 : (U1 → Prop) → Prop. Variable genU2 : (U2 → Prop) → Prop.
Let genU1xU2 := Gen_Prod genU1 genU2.
Let genU2xU1 := Gen_Prod genU2 genU1.
Lemma Sigma_algebra_swap_c :
∀ A, Sigma_algebra genU1xU2 A → Sigma_algebra genU2xU1 (swap_c A).
Proof.
intros A HA; induction HA as [A [A1 [A2 [HA1 [HA2 HA]]]] | | | ].
rewrite HA, swap_c_prod.
apply Sigma_algebra_prod;
now apply Sigma_algebra_gen_remove_alt with (1 := Sigma_algebra_wFull _).
apply Sigma_algebra_wEmpty.
now apply Sigma_algebra_Compl.
now apply Sigma_algebra_Union_seq.
Qed.
End Prod_Sigma_algebra_Facts2.
Section Prod_Sigma_algebra_Facts3.
Context {U1 U2 : Type}. Variable genU1 : (U1 → Prop) → Prop. Variable genU2 : (U2 → Prop) → Prop.
Let genU1xU2 := Gen_Prod genU1 genU2.
Let genU2xU1 := Gen_Prod genU2 genU1.
Lemma Sigma_algebra_swap_c_rev :
∀ A, Sigma_algebra genU2xU1 (swap_c A) → Sigma_algebra genU1xU2 A.
Proof.
intros; rewrite <- swap_c_invol; now apply Sigma_algebra_swap_c.
Qed.
Lemma Sigma_algebra_swap_c_equiv :
∀ A, Sigma_algebra genU1xU2 A ↔ Sigma_algebra genU2xU1 (swap_c A).
Proof.
intros; split; [apply Sigma_algebra_swap_c | apply Sigma_algebra_swap_c_rev].
Qed.
End Prod_Sigma_algebra_Facts3.
Section Prod_Sigma_algebra_Facts4.
Context {U V : Type}. Variable genU1 genU2 : (U → Prop) → Prop. Variable genV1 genV2 : (V → Prop) → Prop.
Let genU1xU2 := Gen_Prod genU1 genV1.
Let genV1xV2 := Gen_Prod genU2 genV2.
Lemma Sigma_algebra_Gen_Prod_ext_aux :
Sigma_algebra genU1 = Sigma_algebra genU2 →
Sigma_algebra genV1 = Sigma_algebra genV2 →
Incl genU1xU2 (Sigma_algebra genV1xV2).
Proof.
intros H1 H2 A [A1 [A2 [HA1 [HA2 HA]]]]; rewrite HA.
apply Sigma_algebra_prod; [rewrite <- H1 | rewrite <- H2];
now apply Sigma_algebra_gen_remove_full.
Qed.
End Prod_Sigma_algebra_Facts4.
Section Prod_Sigma_algebra_Facts5.
Context {U V : Type}. Variable genU1 genU2 : (U → Prop) → Prop. Variable genV1 genV2 : (V → Prop) → Prop.
Let genU1xU2 := Gen_Prod genU1 genV1.
Let genV1xV2 := Gen_Prod genU2 genV2.
Lemma Sigma_algebra_Gen_Prod_ext :
Sigma_algebra genU1 = Sigma_algebra genU2 →
Sigma_algebra genV1 = Sigma_algebra genV2 →
Sigma_algebra genU1xU2 = Sigma_algebra genV1xV2.
Proof.
intros; apply Ext_equiv; split;
now apply Sigma_algebra_lub_alt, Sigma_algebra_Gen_Prod_ext_aux.
Qed.
End Prod_Sigma_algebra_Facts5.
Section Algebra_Facts4.
Context {U1 U2 : Type}.
Variable genU1 : (U1 → Prop) → Prop. Variable genU2 : (U2 → Prop) → Prop.
Lemma Prod_Sigma_algebra_wFull :
wFull (Prod_Sigma_algebra genU1 genU2).
Proof.
∃ fullset, fullset; repeat split; try apply Sigma_algebra_wFull.
now rewrite prod_full.
Qed.
Lemma Prod_Sigma_algebra_Inter :
Inter (Prod_Sigma_algebra genU1 genU2).
Proof.
intros A B [A1 [A2 HA]] [B1 [B2 HB]].
∃ (inter A1 B1), (inter A2 B2); repeat split.
1,2: now apply Sigma_algebra_Inter.
destruct HA as [_ [_ HA]]; rewrite HA.
destruct HB as [_ [_ HB]]; rewrite HB.
apply prod_inter.
Qed.
Lemma Prod_Sigma_algebra_Part_compl_finite :
Part_compl_finite (Prod_Sigma_algebra genU1 genU2).
Proof.
intros A [A1 [A2 HA]].
∃ (fun n ⇒ match n with
| 0 ⇒ prod (compl A1) A2
| 1 ⇒ prod fullset (compl A2)
| _ ⇒ emptyset
end).
∃ 1.
split.
intros n Hn; rewrite lt_2 in Hn; destruct Hn as [Hn | Hn]; rewrite Hn.
∃ (compl A1); ∃ A2; repeat split; try easy.
now apply Sigma_algebra_Compl.
∃ fullset; ∃ (compl A2); repeat split.
apply Sigma_algebra_wFull.
now apply Sigma_algebra_Compl.
apply partition_finite_1.
destruct HA as [_ [_ HA]]; rewrite HA.
apply prod_compl_partition.
Qed.
Lemma Algebra_product_explicit :
Algebra (Prod_Sigma_algebra genU1 genU2) =
Union_disj_finite_closure (Prod_Sigma_algebra genU1 genU2).
Proof.
apply Algebra_explicit; repeat split.
apply Prod_Sigma_algebra_wFull.
apply Prod_Sigma_algebra_Inter.
apply Prod_Sigma_algebra_Part_compl_finite.
Qed.
End Algebra_Facts4.
Section Algebra_Facts5.
Context {U1 U2 : Type}.
Variable genU1 : (U1 → Prop) → Prop. Variable genU2 : (U2 → Prop) → Prop.
Lemma Algebra_Gen_Prod_Prod_Sigma_algebra_Incl :
Incl (Algebra (Gen_Prod genU1 genU2)) (Algebra (Prod_Sigma_algebra genU1 genU2)).
Proof.
apply Algebra_monot, Gen_Prod_is_Prod_Sigma_algebra.
Qed.
End Algebra_Facts5.
Section More_Facts.
Context {U : Type}.
Variable gen : (U → Prop) → Prop.
Lemma Algebra_Prop : ∀ P, Algebra gen (Prop_cst P).
Proof.
intros P; case (classic P); intros.
rewrite (subset_ext (Prop_cst P) fullset); [apply Algebra_wFull | easy].
rewrite (subset_ext (Prop_cst P) emptyset); [apply Algebra_wEmpty | easy].
Qed.
Lemma Lsyst_Prop : ∀ P, Lsyst gen (Prop_cst P).
Proof.
intros P; case (classic P); intros.
rewrite (subset_ext (Prop_cst P) fullset); [apply Lsyst_wFull | easy].
rewrite (subset_ext (Prop_cst P) emptyset); [apply Lsyst_wEmpty | easy].
Qed.
Lemma Sigma_algebra_Prop : ∀ P, Sigma_algebra gen (Prop_cst P).
Proof.
intros; apply Incl_Algebra_Sigma_algebra, Algebra_Prop.
Qed.
Lemma Sigma_algebra_correct :
∀ P : ((U → Prop) → Prop) → Prop,
IIncl is_Sigma_algebra P ↔ ∀ gen, P (Sigma_algebra gen).
Proof.
intros; split.
intros HP gen'; apply HP, Sigma_algebra_idem.
intros HP calS HcalS; rewrite <- HcalS; apply HP.
Qed.
Definition trivial_SA := pair (@emptyset U) fullset.
Lemma is_Sigma_algebra_trivial_SA : is_Sigma_algebra trivial_SA.
Proof.
apply Ext_equiv; split; try apply Sigma_algebra_Gen.
intros A HA; induction HA as [ | | A HA1 [HA2 | HA2] | A HA1 HA2]; try easy.
now left.
right; rewrite HA2; apply compl_empty.
left; rewrite HA2; apply compl_full.
case (classic (∃ n, A n = fullset)); intros H.
right; now apply union_seq_full.
left; apply union_seq_empty; intros n; destruct (HA2 n) as [HA2' | HA2']; try easy.
contradict H; now ∃ n.
Qed.
Definition discete_SA := @fullset (U → Prop).
Lemma is_Sigma_algebra_discrete_SA : is_Sigma_algebra discete_SA.
Proof.
apply Ext_equiv; split; try easy.
apply Sigma_algebra_Gen.
Qed.
End More_Facts.
Require Import sigma_algebra.
Section equiv_SA.
Context {E : Type}.
Variable gen : (E → Prop) → Prop.
Lemma measurable_Sigma_algebra : measurable gen = Sigma_algebra gen.
Proof.
apply subset_ext; intro; split; intros H; induction H.
apply Sigma_algebra_Gen; easy.
apply Sigma_algebra_wEmpty.
apply Sigma_algebra_Compl_rev; easy.
apply Sigma_algebra_Union_seq; easy.
apply measurable_gen; easy.
apply measurable_empty.
apply measurable_compl_rev; easy.
apply measurable_union_countable; easy.
Qed.
End equiv_SA.
Section equiv_GP.
Context {U1 U2 : Type}.
Variable genU1 : (U1 → Prop) → Prop.
Variable genU2 : (U2 → Prop) → Prop.
Lemma Gen_Prod_Gen_Product : Gen_Prod genU1 genU2 = Gen_Product genU1 genU2.
Proof.
apply subset_ext; intro; split; intros [A1 [A2 [HA1 [HA2 HA]]]];
∃ A1, A2; (split; [easy | split; [easy |]]).
rewrite HA; easy.
apply subset_ext; easy.
Qed.
End equiv_GP.