Library Subsets.Subset_charac
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 characteristic (or indicator) functions of subsets.
This module may be used through the import of Subsets.Subsets,
Subsets.Subsets_wDep, Algebra.Algebra_wDep, Lebesgue.Lebesgue_p_wDep, or
Lebesgue.Bochner.Bochner_wDep, where it is exported.
Brief description
Used logic axioms
- classic, the weak form of excluded middle;
- fun_ext, an alias for functional_extensionality.
Usage
From Requisite Require Import stdlib_wR ssr.
From Logic Require Import logic_compl.
From Subsets Require Import Subset Subset_dec.
Open Scope R_scope.
Section Base_Def.
Context {U : Type}.
Indicator/characteristic function.
Variable A : U → Prop.
Definition charac : (U → Prop) → U → R :=
fun A x ⇒ match in_dec A x with
| left _ ⇒ 1
| right _ ⇒ 0
end.
End Base_Def.
Section Prop_Facts0.
Context {U : Type}.
Variable A : U → Prop.
Lemma charac_or : ∀ x, charac A x = 0 ∨ charac A x = 1.
Proof.
intros x; unfold charac; case (in_dec A x); intros _; [right | left]; easy.
Qed.
Lemma charac_ge_0 : ∀ x, 0 ≤ charac A x.
Proof. intros x; case (charac_or x); intros H; rewrite H; lra. Qed.
Lemma charac_le_1 : ∀ x, charac A x ≤ 1.
Proof. intros x; case (charac_or x); intros H; rewrite H; lra. Qed.
Lemma charac_is_1 : ∀ x, A x → charac A x = 1.
Proof. intros x; unfold charac; now case (in_dec A x). Qed.
Lemma charac_1 : ∀ x, charac A x = 1 → A x.
Proof.
intros x; unfold charac; case (in_dec A x); try easy.
intros _ L; contradict L; lra.
Qed.
Lemma charac_in_equiv : ∀ x, charac A x = 1 ↔ A x.
Proof. intros; split; [apply charac_1 | apply charac_is_1]. Qed.
Lemma charac_is_0 : ∀ x, compl A x → charac A x = 0.
Proof. intros x; unfold charac; now case (in_dec A x). Qed.
Lemma charac_0 : ∀ x, charac A x = 0 → compl A x.
Proof.
intros x; unfold charac; case (in_dec A x); try easy.
intros _ L; contradict L; lra.
Qed.
Lemma charac_out_equiv : ∀ x, charac A x = 0 ↔ compl A x.
Proof. intros; split; [apply charac_0 | apply charac_is_0]. Qed.
End Prop_Facts0.
Section Prop_Facts1.
Context {U : Type}.
Variable A B : U → Prop.
Lemma charac_le : incl A B → ∀ x, charac A x ≤ charac B x.
Proof.
intros H x.
case (charac_or A x); intros HAx;
case (charac_or B x); intros HBx; rewrite HAx HBx; try lra.
rewrite charac_in_equiv in HAx.
rewrite charac_out_equiv in HBx.
contradict H; intuition.
Qed.
Lemma charac_ext : same A B → ∀ x, charac A x = charac B x.
Proof. intros H; apply subset_ext in H; now rewrite H. Qed.
End Prop_Facts1.
Section Prop_Facts2.
Context {U : Type}.
Lemma charac_emptyset : ∀ (x : U), charac emptyset x = 0.
Proof. intros; now rewrite charac_out_equiv. Qed.
Lemma charac_fullset : ∀ (x : U), charac fullset x = 1.
Proof. intros; now rewrite charac_in_equiv. Qed.
Lemma charac_empty :
∀ (A : U → Prop), empty A → ∀ x, charac A x = 0.
Proof.
intros A H; rewrite empty_emptyset in H; rewrite H; apply charac_emptyset.
Qed.
Lemma charac_full :
∀ (A : U → Prop), full A → ∀ x, charac A x = 1.
Proof.
intros A H; rewrite full_fullset in H; rewrite H; apply charac_fullset.
Qed.
Lemma charac_compl :
∀ (A : U → Prop) x, charac (compl A) x = 1 - charac A x.
Proof.
intros A x.
case (charac_or A x); intros Hx; rewrite Hx.
now rewrite Rminus_0_r charac_in_equiv -charac_out_equiv.
now rewrite Rminus_diag charac_out_equiv compl_invol -charac_in_equiv.
Qed.
Lemma charac_inter :
∀ (A B : U → Prop) x, charac (inter A B) x = charac A x × charac B x.
Proof.
intros A B x.
case (charac_or A x); intros HAx; rewrite HAx.
rewrite Rmult_0_l charac_out_equiv compl_inter;
now apply union_ub_l, charac_out_equiv.
case (charac_or B x); intros HBx; rewrite HBx.
rewrite Rmult_0_r charac_out_equiv compl_inter;
now apply union_ub_r, charac_out_equiv.
rewrite Rmult_1_r charac_in_equiv; split; now apply charac_in_equiv.
Qed.
Lemma charac_union :
∀ (A B : U → Prop) x,
charac (union A B) x = charac A x + charac B x - charac A x × charac B x.
Proof.
intros A B x; rewrite <- (compl_invol (union _ _)), compl_union.
rewrite charac_compl charac_inter 2!charac_compl; ring.
Qed.
Lemma charac_disj :
∀ (A B : U → Prop), disj A B → ∀ x, charac A x × charac B x = 0.
Proof.
intros A B H x; rewrite <- charac_inter, charac_out_equiv.
rewrite disj_equiv_def in H; now rewrite H.
Qed.
Lemma charac_diff :
∀ (A B : U → Prop) x,
charac (diff A B) x = charac A x - charac A x × charac B x.
Proof.
intros; rewrite diff_equiv_def_inter charac_inter charac_compl; ring.
Qed.
Lemma charac_sym_diff :
∀ (A B : U → Prop) x,
charac (sym_diff A B) x =
charac A x + charac B x - 2 × charac A x × charac B x.
Proof.
intros A B x; rewrite sym_diff_equiv_def_diff.
rewrite charac_diff -charac_inter.
replace (inter (union A B) (inter A B)) with (inter A B).
rewrite charac_union charac_inter; ring.
rewrite inter_union_distr_r.
rewrite -inter_assoc inter_idem inter_comm.
now rewrite -inter_assoc inter_idem union_idem.
Qed.
Lemma charac_partition :
∀ (A B C : U → Prop),
partition A B C → ∀ x, charac A x = charac B x + charac C x.
Proof.
intros A B C [H1 H2] x.
rewrite H1 charac_union charac_disj; try easy; ring.
Qed.
Lemma charac_inj : injective (@charac U).
Proof.
move=>> H; apply subset_ext_equiv; split; move=>> Hx; apply charac_1;
[rewrite -H | rewrite H]; apply charac_is_1; easy.
Qed.
Lemma charac_comp :
∀ {V : Type} (f : U → V) (A : V → Prop),
charac (fun x ⇒ A (f x)) = fun x ⇒ charac A (f x).
Proof.
intros V f A; apply fun_ext; intros x;
destruct (classic (A (f x))) as [Hx | Hx];
[rewrite !charac_is_1 | rewrite !charac_is_0]; easy.
Qed.
End Prop_Facts2.