Library Waterproof.Libs.Analysis.ContinuityDomainR
From Stdlib Require Import Reals.Reals.
Require Import Notations.Common.
Require Import Notations.Reals.
Require Import Notations.Sets.
Require Import Chains.
Require Import Tactics.
Require Import Waterproof.Automation.
Waterproof Enable Automation RealsAndIntegers.
Waterproof Enable Automation Intuition.
Open Scope R_scope.
Definitions
Definition is_accumulation_point (a : R) :=
∀ ε > 0, ∃ x ∈ R, 0 < |x - a| < ε.
Definition is_isolated_point (a : R) :=
∃ ε > 0, ∀ x ∈ R, |x - a| = 0 ∨ (ε ≤ |x - a|).
Definition limit_in_point (f : R → R) (a : R) (q : R) :=
∀ ε > 0, ∃ δ > 0, ∀ x ∈ R, (0 < |x - a| < δ) ⇒ (|(f x) - q| < ε).
Definition is_continuous_in (f : R → R) (a : R) :=
((is_accumulation_point a) ∧ (limit_in_point f a (f a))) ∨ (is_isolated_point a).
Lemma every_point_in_R_acc_point_R (a : R) :
is_accumulation_point a.
Proof.
We need to show that ∀ r > 0, ∃ x ∈ R, 0 < | x - a | < r.
Take r > 0.
Choose x := a + r/2.
* Indeed, x ∈ ℝ.
* We need to show that 0 < | x - a | < r.
unfold gt_op, R_gt_type in *.
It holds that | x - a | < r.
It holds that | x - a | > 0.
We conclude that 0 < | x - a | < r.
Qed.
Theorem alt_char_continuity (h : R → R) (a : R) :
is_continuous_in h a ⇔ ∀ ε > 0, ∃ δ > 0,
(∀ x ∈ R, 0 < | x - a | < δ ⇒ | h(x) - h(a) | < ε).
Proof.
We show both directions.
* We need to show that is_continuous_in(h, a) ⇨ ∀ ε > 0, ∃ δ > 0, ∀ x ∈ ℝ,
0 < |x - a| < δ ⇨ |h(x) - h(a)| < ε.
Assume that is_continuous_in h a.
Either is_accumulation_point a ∧ limit_in_point h a (h a) or is_isolated_point a.
+ Case is_accumulation_point a ∧ limit_in_point h a (h a).
Take ε > 0.
It holds that ∃ δ1 > 0, ∀ x ∈ R,
(0 < |x - a| < δ1) ⇒ (|(h x) - (h a)| < ε).
Obtain such a δ1.
Choose δ := δ1.
- Indeed, δ > 0.
- We conclude that ∀ x ∈ ℝ,
0 < |x - a| < δ ⇨ |h(x) - h(a)| < ε.
+ Case (is_isolated_point a).
It holds that ∃ ε > 0, ∀ x ∈ ℝ, |x - a| = 0 ∨ ε ≤ |x - a|.
Obtain such an ε.
It holds that ε > 0.
Define z := a + ε / 2.
It holds that |z - a| = 0 \/ ε ≤ | z - a | as (ii).
destruct ii.
- It holds that | z - a | > 0.
Contradiction.
- It holds that | z - a| < ε.
Contradiction.
* We need to show that (∀ ε > 0, ∃ δ > 0, ∀ x ∈ ℝ,
0 < |x - a| < δ ⇨ |h(x) - h(a)| < ε) ⇨ is_continuous_in(h, a).
Assume that ∀ ε > 0, ∃ δ > 0, ∀ x ∈ ℝ,
0 < |x - a| < δ ⇨ |h(x) - h(a)| < ε .
unfold is_continuous_in.
We need to show that is_accumulation_point(a) ∧ limit_in_point(h, a, h(a)) ∨ is_isolated_point(a).
It suffices to show that is_accumulation_point(a) ∧ limit_in_point(h, a, h(a)).
We show both statements.
+ By every_point_in_R_acc_point_R we conclude that is_accumulation_point a.
+ We conclude that limit_in_point(h, a, h a).
Qed.
#[export] Hint Resolve -> alt_char_continuity : wp_reals.
#[export] Hint Resolve <- alt_char_continuity : wp_reals.
∀ ε > 0, ∃ x ∈ R, 0 < |x - a| < ε.
Definition is_isolated_point (a : R) :=
∃ ε > 0, ∀ x ∈ R, |x - a| = 0 ∨ (ε ≤ |x - a|).
Definition limit_in_point (f : R → R) (a : R) (q : R) :=
∀ ε > 0, ∃ δ > 0, ∀ x ∈ R, (0 < |x - a| < δ) ⇒ (|(f x) - q| < ε).
Definition is_continuous_in (f : R → R) (a : R) :=
((is_accumulation_point a) ∧ (limit_in_point f a (f a))) ∨ (is_isolated_point a).
Lemma every_point_in_R_acc_point_R (a : R) :
is_accumulation_point a.
Proof.
We need to show that ∀ r > 0, ∃ x ∈ R, 0 < | x - a | < r.
Take r > 0.
Choose x := a + r/2.
* Indeed, x ∈ ℝ.
* We need to show that 0 < | x - a | < r.
unfold gt_op, R_gt_type in *.
It holds that | x - a | < r.
It holds that | x - a | > 0.
We conclude that 0 < | x - a | < r.
Qed.
Theorem alt_char_continuity (h : R → R) (a : R) :
is_continuous_in h a ⇔ ∀ ε > 0, ∃ δ > 0,
(∀ x ∈ R, 0 < | x - a | < δ ⇒ | h(x) - h(a) | < ε).
Proof.
We show both directions.
* We need to show that is_continuous_in(h, a) ⇨ ∀ ε > 0, ∃ δ > 0, ∀ x ∈ ℝ,
0 < |x - a| < δ ⇨ |h(x) - h(a)| < ε.
Assume that is_continuous_in h a.
Either is_accumulation_point a ∧ limit_in_point h a (h a) or is_isolated_point a.
+ Case is_accumulation_point a ∧ limit_in_point h a (h a).
Take ε > 0.
It holds that ∃ δ1 > 0, ∀ x ∈ R,
(0 < |x - a| < δ1) ⇒ (|(h x) - (h a)| < ε).
Obtain such a δ1.
Choose δ := δ1.
- Indeed, δ > 0.
- We conclude that ∀ x ∈ ℝ,
0 < |x - a| < δ ⇨ |h(x) - h(a)| < ε.
+ Case (is_isolated_point a).
It holds that ∃ ε > 0, ∀ x ∈ ℝ, |x - a| = 0 ∨ ε ≤ |x - a|.
Obtain such an ε.
It holds that ε > 0.
Define z := a + ε / 2.
It holds that |z - a| = 0 \/ ε ≤ | z - a | as (ii).
destruct ii.
- It holds that | z - a | > 0.
Contradiction.
- It holds that | z - a| < ε.
Contradiction.
* We need to show that (∀ ε > 0, ∃ δ > 0, ∀ x ∈ ℝ,
0 < |x - a| < δ ⇨ |h(x) - h(a)| < ε) ⇨ is_continuous_in(h, a).
Assume that ∀ ε > 0, ∃ δ > 0, ∀ x ∈ ℝ,
0 < |x - a| < δ ⇨ |h(x) - h(a)| < ε .
unfold is_continuous_in.
We need to show that is_accumulation_point(a) ∧ limit_in_point(h, a, h(a)) ∨ is_isolated_point(a).
It suffices to show that is_accumulation_point(a) ∧ limit_in_point(h, a, h(a)).
We show both statements.
+ By every_point_in_R_acc_point_R we conclude that is_accumulation_point a.
+ We conclude that limit_in_point(h, a, h a).
Qed.
#[export] Hint Resolve -> alt_char_continuity : wp_reals.
#[export] Hint Resolve <- alt_char_continuity : wp_reals.
Notations
Notation "a 'is' 'an' '_accumulation' 'point_'" := (is_accumulation_point a) (at level 69).
Notation "a 'is' 'an' 'accumulation' 'point'" := (is_accumulation_point a) (at level 69, only parsing).
Local Ltac2 unfold_acc_point (statement : constr) := eval unfold is_accumulation_point in $statement.
Ltac2 Notation "Expand" "the" "definition" "of" "accumulation" "point" x(opt(seq("in", constr))) :=
wp_unfold unfold_acc_point (Some "accumulation point") true true x.
Ltac2 Notation "_internal_" "Expand" "the" "definition" "of" "accumulation" "point" x(opt(seq("in", constr))) :=
wp_unfold unfold_acc_point (Some "accumulation point") false true x.
Notation "a 'is' 'an' '_isolated' 'point_'" := (is_isolated_point a) (at level 69).
Notation "a 'is' 'an' 'isolated' 'point'" := (is_isolated_point a) (at level 69, only parsing).
Local Ltac2 unfold_isol_point (statement : constr) := eval unfold is_isolated_point in $statement.
Ltac2 Notation "Expand" "the" "definition" "of" "isolated" "point" x(opt(seq("in", constr))) :=
wp_unfold unfold_isol_point (Some "isolated point") true true x.
Ltac2 Notation "_internal_" "Expand" "the" "definition" "of" "isolated" "point" x(opt(seq("in", constr))) :=
wp_unfold unfold_isol_point (Some "isolated point") false true x.
Notation "'_limit_' 'of' f 'in' a 'is' L" := (limit_in_point f a L) (at level 69).
Notation "'limit' 'of' f 'in' a 'is' L" := (limit_in_point f a L) (at level 69, only parsing).
Local Ltac2 unfold_lim_in_point (statement : constr) := eval unfold limit_in_point in $statement.
Ltac2 Notation "Expand" "the" "definition" "of" "limit" x(opt(seq("in", constr))) :=
wp_unfold unfold_lim_in_point (Some "limit") true true x.
Ltac2 Notation "_internal_" "Expand" "the" "definition" "of" "limit" x(opt(seq("in", constr))) :=
wp_unfold unfold_lim_in_point (Some "limit") false true x.
Notation "f 'is' '_continuous_' 'in' a" := (is_continuous_in f a) (at level 69).
Notation "f 'is' 'continuous' 'in' a" := (is_continuous_in f a) (at level 69, only parsing).
Local Ltac2 unfold_is_cont (statement : constr) := eval unfold is_continuous_in in $statement.
Ltac2 Notation "Expand" "the" "definition" "of" "continuous" x(opt(seq("in", constr))) :=
wp_unfold unfold_is_cont (Some "continuous") true true x.
Ltac2 Notation "_internal_" "Expand" "the" "definition" "of" "continuous" x(opt(seq("in", constr))) :=
wp_unfold unfold_is_cont (Some "continuous") false true x.
Close Scope R_scope.
Notation "a 'is' 'an' 'accumulation' 'point'" := (is_accumulation_point a) (at level 69, only parsing).
Local Ltac2 unfold_acc_point (statement : constr) := eval unfold is_accumulation_point in $statement.
Ltac2 Notation "Expand" "the" "definition" "of" "accumulation" "point" x(opt(seq("in", constr))) :=
wp_unfold unfold_acc_point (Some "accumulation point") true true x.
Ltac2 Notation "_internal_" "Expand" "the" "definition" "of" "accumulation" "point" x(opt(seq("in", constr))) :=
wp_unfold unfold_acc_point (Some "accumulation point") false true x.
Notation "a 'is' 'an' '_isolated' 'point_'" := (is_isolated_point a) (at level 69).
Notation "a 'is' 'an' 'isolated' 'point'" := (is_isolated_point a) (at level 69, only parsing).
Local Ltac2 unfold_isol_point (statement : constr) := eval unfold is_isolated_point in $statement.
Ltac2 Notation "Expand" "the" "definition" "of" "isolated" "point" x(opt(seq("in", constr))) :=
wp_unfold unfold_isol_point (Some "isolated point") true true x.
Ltac2 Notation "_internal_" "Expand" "the" "definition" "of" "isolated" "point" x(opt(seq("in", constr))) :=
wp_unfold unfold_isol_point (Some "isolated point") false true x.
Notation "'_limit_' 'of' f 'in' a 'is' L" := (limit_in_point f a L) (at level 69).
Notation "'limit' 'of' f 'in' a 'is' L" := (limit_in_point f a L) (at level 69, only parsing).
Local Ltac2 unfold_lim_in_point (statement : constr) := eval unfold limit_in_point in $statement.
Ltac2 Notation "Expand" "the" "definition" "of" "limit" x(opt(seq("in", constr))) :=
wp_unfold unfold_lim_in_point (Some "limit") true true x.
Ltac2 Notation "_internal_" "Expand" "the" "definition" "of" "limit" x(opt(seq("in", constr))) :=
wp_unfold unfold_lim_in_point (Some "limit") false true x.
Notation "f 'is' '_continuous_' 'in' a" := (is_continuous_in f a) (at level 69).
Notation "f 'is' 'continuous' 'in' a" := (is_continuous_in f a) (at level 69, only parsing).
Local Ltac2 unfold_is_cont (statement : constr) := eval unfold is_continuous_in in $statement.
Ltac2 Notation "Expand" "the" "definition" "of" "continuous" x(opt(seq("in", constr))) :=
wp_unfold unfold_is_cont (Some "continuous") true true x.
Ltac2 Notation "_internal_" "Expand" "the" "definition" "of" "continuous" x(opt(seq("in", constr))) :=
wp_unfold unfold_is_cont (Some "continuous") false true x.
Close Scope R_scope.