Left and right limits #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
We define the (strict) left and right limits of a function.
left_lim f xis the strict left limit offatx(usingf xas a garbage value ifxis isolated to its left).right_lim f xis the strict right limit offatx(usingf xas a garbage value ifxis isolated to its right).
We develop a comprehensive API for monotone functions. Notably,
monotone.continuous_at_iff_left_lim_eq_right_limstates that a monotone function is continuous at a point if and only if its left and right limits coincide.monotone.countable_not_continuous_atasserts that a monotone function taking values in a second-countable space has at most countably many discontinuity points.
We also port the API to antitone functions.
TODO #
Prove corresponding stronger results for strict_mono and strict_anti functions.
@[irreducible]
noncomputable
def
function.left_lim
{α : Type u_1}
{β : Type u_2}
[linear_order α]
[topological_space β]
(f : α → β)
(a : α) :
β
Let f : α → β be a function from a linear order α to a topological_space β, and
let a : α. The limit strictly to the left of f at a, denoted with left_lim f a, is defined
by using the order topology on α. If a is isolated to its left or the function has no left
limit, we use f a instead to guarantee a good behavior in most cases.
Equations
- function.left_lim f a = let _inst_3 : topological_space α := preorder.topology α in ite (nhds_within a (set.Iio a) = ⊥ ∨ ¬∃ (y : β), filter.tendsto f (nhds_within a (set.Iio a)) (nhds y)) (f a) (lim (nhds_within a (set.Iio a)) f)
noncomputable
def
function.right_lim
{α : Type u_1}
{β : Type u_2}
[linear_order α]
[topological_space β]
(f : α → β)
(a : α) :
β
Let f : α → β be a function from a linear order α to a topological_space β, and
let a : α. The limit strictly to the right of f at a, denoted with right_lim f a, is defined
by using the order topology on α. If a is isolated to its right or the function has no right
limit, , we use f a instead to guarantee a good behavior in most cases.
Equations
- function.right_lim f a = function.left_lim f a
theorem
left_lim_eq_of_tendsto
{α : Type u_1}
{β : Type u_2}
[linear_order α]
[topological_space β]
[hα : topological_space α]
[h'α : order_topology α]
[t2_space β]
{f : α → β}
{a : α}
{y : β}
(h : nhds_within a (set.Iio a) ≠ ⊥)
(h' : filter.tendsto f (nhds_within a (set.Iio a)) (nhds y)) :
function.left_lim f a = y
theorem
left_lim_eq_of_eq_bot
{α : Type u_1}
{β : Type u_2}
[linear_order α]
[topological_space β]
[hα : topological_space α]
[h'α : order_topology α]
(f : α → β)
{a : α}
(h : nhds_within a (set.Iio a) = ⊥) :
function.left_lim f a = f a
theorem
monotone.left_lim_eq_Sup
{α : Type u_1}
{β : Type u_2}
[linear_order α]
[conditionally_complete_linear_order β]
[topological_space β]
[order_topology β]
{f : α → β}
(hf : monotone f)
{x : α}
[topological_space α]
[order_topology α]
(h : nhds_within x (set.Iio x) ≠ ⊥) :
function.left_lim f x = has_Sup.Sup (f '' set.Iio x)
theorem
monotone.left_lim_le
{α : Type u_1}
{β : Type u_2}
[linear_order α]
[conditionally_complete_linear_order β]
[topological_space β]
[order_topology β]
{f : α → β}
(hf : monotone f)
{x y : α}
(h : x ≤ y) :
function.left_lim f x ≤ f y
theorem
monotone.le_left_lim
{α : Type u_1}
{β : Type u_2}
[linear_order α]
[conditionally_complete_linear_order β]
[topological_space β]
[order_topology β]
{f : α → β}
(hf : monotone f)
{x y : α}
(h : x < y) :
f x ≤ function.left_lim f y
@[protected]
theorem
monotone.left_lim
{α : Type u_1}
{β : Type u_2}
[linear_order α]
[conditionally_complete_linear_order β]
[topological_space β]
[order_topology β]
{f : α → β}
(hf : monotone f) :
theorem
monotone.le_right_lim
{α : Type u_1}
{β : Type u_2}
[linear_order α]
[conditionally_complete_linear_order β]
[topological_space β]
[order_topology β]
{f : α → β}
(hf : monotone f)
{x y : α}
(h : x ≤ y) :
f x ≤ function.right_lim f y
theorem
monotone.right_lim_le
{α : Type u_1}
{β : Type u_2}
[linear_order α]
[conditionally_complete_linear_order β]
[topological_space β]
[order_topology β]
{f : α → β}
(hf : monotone f)
{x y : α}
(h : x < y) :
function.right_lim f x ≤ f y
@[protected]
theorem
monotone.right_lim
{α : Type u_1}
{β : Type u_2}
[linear_order α]
[conditionally_complete_linear_order β]
[topological_space β]
[order_topology β]
{f : α → β}
(hf : monotone f) :
theorem
monotone.left_lim_le_right_lim
{α : Type u_1}
{β : Type u_2}
[linear_order α]
[conditionally_complete_linear_order β]
[topological_space β]
[order_topology β]
{f : α → β}
(hf : monotone f)
{x y : α}
(h : x ≤ y) :
function.left_lim f x ≤ function.right_lim f y
theorem
monotone.right_lim_le_left_lim
{α : Type u_1}
{β : Type u_2}
[linear_order α]
[conditionally_complete_linear_order β]
[topological_space β]
[order_topology β]
{f : α → β}
(hf : monotone f)
{x y : α}
(h : x < y) :
function.right_lim f x ≤ function.left_lim f y
theorem
monotone.tendsto_left_lim
{α : Type u_1}
{β : Type u_2}
[linear_order α]
[conditionally_complete_linear_order β]
[topological_space β]
[order_topology β]
{f : α → β}
(hf : monotone f)
[topological_space α]
[order_topology α]
(x : α) :
filter.tendsto f (nhds_within x (set.Iio x)) (nhds (function.left_lim f x))
theorem
monotone.tendsto_left_lim_within
{α : Type u_1}
{β : Type u_2}
[linear_order α]
[conditionally_complete_linear_order β]
[topological_space β]
[order_topology β]
{f : α → β}
(hf : monotone f)
[topological_space α]
[order_topology α]
(x : α) :
filter.tendsto f (nhds_within x (set.Iio x)) (nhds_within (function.left_lim f x) (set.Iic (function.left_lim f x)))
theorem
monotone.tendsto_right_lim
{α : Type u_1}
{β : Type u_2}
[linear_order α]
[conditionally_complete_linear_order β]
[topological_space β]
[order_topology β]
{f : α → β}
(hf : monotone f)
[topological_space α]
[order_topology α]
(x : α) :
filter.tendsto f (nhds_within x (set.Ioi x)) (nhds (function.right_lim f x))
theorem
monotone.tendsto_right_lim_within
{α : Type u_1}
{β : Type u_2}
[linear_order α]
[conditionally_complete_linear_order β]
[topological_space β]
[order_topology β]
{f : α → β}
(hf : monotone f)
[topological_space α]
[order_topology α]
(x : α) :
filter.tendsto f (nhds_within x (set.Ioi x)) (nhds_within (function.right_lim f x) (set.Ici (function.right_lim f x)))
theorem
monotone.continuous_within_at_Iio_iff_left_lim_eq
{α : Type u_1}
{β : Type u_2}
[linear_order α]
[conditionally_complete_linear_order β]
[topological_space β]
[order_topology β]
{f : α → β}
(hf : monotone f)
{x : α}
[topological_space α]
[order_topology α] :
continuous_within_at f (set.Iio x) x ↔ function.left_lim f x = f x
A monotone function is continuous to the left at a point if and only if its left limit coincides with the value of the function.
theorem
monotone.continuous_within_at_Ioi_iff_right_lim_eq
{α : Type u_1}
{β : Type u_2}
[linear_order α]
[conditionally_complete_linear_order β]
[topological_space β]
[order_topology β]
{f : α → β}
(hf : monotone f)
{x : α}
[topological_space α]
[order_topology α] :
continuous_within_at f (set.Ioi x) x ↔ function.right_lim f x = f x
A monotone function is continuous to the right at a point if and only if its right limit coincides with the value of the function.
theorem
monotone.continuous_at_iff_left_lim_eq_right_lim
{α : Type u_1}
{β : Type u_2}
[linear_order α]
[conditionally_complete_linear_order β]
[topological_space β]
[order_topology β]
{f : α → β}
(hf : monotone f)
{x : α}
[topological_space α]
[order_topology α] :
continuous_at f x ↔ function.left_lim f x = function.right_lim f x
A monotone function is continuous at a point if and only if its left and right limits coincide.
theorem
monotone.countable_not_continuous_within_at_Ioi
{α : Type u_1}
{β : Type u_2}
[linear_order α]
[conditionally_complete_linear_order β]
[topological_space β]
[order_topology β]
{f : α → β}
(hf : monotone f)
[topological_space α]
[order_topology α]
[topological_space.second_countable_topology β] :
{x : α | ¬continuous_within_at f (set.Ioi x) x}.countable
In a second countable space, the set of points where a monotone function is not right-continuous
is at most countable. Superseded by countable_not_continuous_at which gives the two-sided
version.
theorem
monotone.countable_not_continuous_within_at_Iio
{α : Type u_1}
{β : Type u_2}
[linear_order α]
[conditionally_complete_linear_order β]
[topological_space β]
[order_topology β]
{f : α → β}
(hf : monotone f)
[topological_space α]
[order_topology α]
[topological_space.second_countable_topology β] :
{x : α | ¬continuous_within_at f (set.Iio x) x}.countable
In a second countable space, the set of points where a monotone function is not left-continuous
is at most countable. Superseded by countable_not_continuous_at which gives the two-sided
version.
theorem
monotone.countable_not_continuous_at
{α : Type u_1}
{β : Type u_2}
[linear_order α]
[conditionally_complete_linear_order β]
[topological_space β]
[order_topology β]
{f : α → β}
(hf : monotone f)
[topological_space α]
[order_topology α]
[topological_space.second_countable_topology β] :
{x : α | ¬continuous_at f x}.countable
In a second countable space, the set of points where a monotone function is not continuous is at most countable.
theorem
antitone.le_left_lim
{α : Type u_1}
{β : Type u_2}
[linear_order α]
[conditionally_complete_linear_order β]
[topological_space β]
[order_topology β]
{f : α → β}
(hf : antitone f)
{x y : α}
(h : x ≤ y) :
f y ≤ function.left_lim f x
theorem
antitone.left_lim_le
{α : Type u_1}
{β : Type u_2}
[linear_order α]
[conditionally_complete_linear_order β]
[topological_space β]
[order_topology β]
{f : α → β}
(hf : antitone f)
{x y : α}
(h : x < y) :
function.left_lim f y ≤ f x
@[protected]
theorem
antitone.left_lim
{α : Type u_1}
{β : Type u_2}
[linear_order α]
[conditionally_complete_linear_order β]
[topological_space β]
[order_topology β]
{f : α → β}
(hf : antitone f) :
theorem
antitone.right_lim_le
{α : Type u_1}
{β : Type u_2}
[linear_order α]
[conditionally_complete_linear_order β]
[topological_space β]
[order_topology β]
{f : α → β}
(hf : antitone f)
{x y : α}
(h : x ≤ y) :
function.right_lim f y ≤ f x
theorem
antitone.le_right_lim
{α : Type u_1}
{β : Type u_2}
[linear_order α]
[conditionally_complete_linear_order β]
[topological_space β]
[order_topology β]
{f : α → β}
(hf : antitone f)
{x y : α}
(h : x < y) :
f y ≤ function.right_lim f x
@[protected]
theorem
antitone.right_lim
{α : Type u_1}
{β : Type u_2}
[linear_order α]
[conditionally_complete_linear_order β]
[topological_space β]
[order_topology β]
{f : α → β}
(hf : antitone f) :
theorem
antitone.right_lim_le_left_lim
{α : Type u_1}
{β : Type u_2}
[linear_order α]
[conditionally_complete_linear_order β]
[topological_space β]
[order_topology β]
{f : α → β}
(hf : antitone f)
{x y : α}
(h : x ≤ y) :
function.right_lim f y ≤ function.left_lim f x
theorem
antitone.left_lim_le_right_lim
{α : Type u_1}
{β : Type u_2}
[linear_order α]
[conditionally_complete_linear_order β]
[topological_space β]
[order_topology β]
{f : α → β}
(hf : antitone f)
{x y : α}
(h : x < y) :
function.left_lim f y ≤ function.right_lim f x
theorem
antitone.tendsto_left_lim
{α : Type u_1}
{β : Type u_2}
[linear_order α]
[conditionally_complete_linear_order β]
[topological_space β]
[order_topology β]
{f : α → β}
(hf : antitone f)
[topological_space α]
[order_topology α]
(x : α) :
filter.tendsto f (nhds_within x (set.Iio x)) (nhds (function.left_lim f x))
theorem
antitone.tendsto_left_lim_within
{α : Type u_1}
{β : Type u_2}
[linear_order α]
[conditionally_complete_linear_order β]
[topological_space β]
[order_topology β]
{f : α → β}
(hf : antitone f)
[topological_space α]
[order_topology α]
(x : α) :
filter.tendsto f (nhds_within x (set.Iio x)) (nhds_within (function.left_lim f x) (set.Ici (function.left_lim f x)))
theorem
antitone.tendsto_right_lim
{α : Type u_1}
{β : Type u_2}
[linear_order α]
[conditionally_complete_linear_order β]
[topological_space β]
[order_topology β]
{f : α → β}
(hf : antitone f)
[topological_space α]
[order_topology α]
(x : α) :
filter.tendsto f (nhds_within x (set.Ioi x)) (nhds (function.right_lim f x))
theorem
antitone.tendsto_right_lim_within
{α : Type u_1}
{β : Type u_2}
[linear_order α]
[conditionally_complete_linear_order β]
[topological_space β]
[order_topology β]
{f : α → β}
(hf : antitone f)
[topological_space α]
[order_topology α]
(x : α) :
filter.tendsto f (nhds_within x (set.Ioi x)) (nhds_within (function.right_lim f x) (set.Iic (function.right_lim f x)))
theorem
antitone.continuous_within_at_Iio_iff_left_lim_eq
{α : Type u_1}
{β : Type u_2}
[linear_order α]
[conditionally_complete_linear_order β]
[topological_space β]
[order_topology β]
{f : α → β}
(hf : antitone f)
{x : α}
[topological_space α]
[order_topology α] :
continuous_within_at f (set.Iio x) x ↔ function.left_lim f x = f x
An antitone function is continuous to the left at a point if and only if its left limit coincides with the value of the function.
theorem
antitone.continuous_within_at_Ioi_iff_right_lim_eq
{α : Type u_1}
{β : Type u_2}
[linear_order α]
[conditionally_complete_linear_order β]
[topological_space β]
[order_topology β]
{f : α → β}
(hf : antitone f)
{x : α}
[topological_space α]
[order_topology α] :
continuous_within_at f (set.Ioi x) x ↔ function.right_lim f x = f x
An antitone function is continuous to the right at a point if and only if its right limit coincides with the value of the function.
theorem
antitone.continuous_at_iff_left_lim_eq_right_lim
{α : Type u_1}
{β : Type u_2}
[linear_order α]
[conditionally_complete_linear_order β]
[topological_space β]
[order_topology β]
{f : α → β}
(hf : antitone f)
{x : α}
[topological_space α]
[order_topology α] :
continuous_at f x ↔ function.left_lim f x = function.right_lim f x
An antitone function is continuous at a point if and only if its left and right limits coincide.
theorem
antitone.countable_not_continuous_at
{α : Type u_1}
{β : Type u_2}
[linear_order α]
[conditionally_complete_linear_order β]
[topological_space β]
[order_topology β]
{f : α → β}
(hf : antitone f)
[topological_space α]
[order_topology α]
[topological_space.second_countable_topology β] :
{x : α | ¬continuous_at f x}.countable
In a second countable space, the set of points where an antitone function is not continuous is at most countable.