Topological facts about Int.floor, Int.ceil and Int.fract

This file proves statements about limits and continuity of functions involving floor, ceil and fract.

Main declarations

• tendsto_floor_atTop, tendsto_floor_atBot, tendsto_ceil_atTop, tendsto_ceil_atBot: Int.floor and Int.ceil tend to +-∞ in +-∞.
• continuousOn_floor: Int.floor is continuous on Ico n (n + 1), because constant.
• continuousOn_ceil: Int.ceil is continuous on Ioc n (n + 1), because constant.
• continuousOn_fract: Int.fract is continuous on Ico n (n + 1).
• ContinuousOn.comp_fract: Precomposing a continuous function satisfying f 0 = f 1 with Int.fract yields another continuous function.

theorem FloorSemiring.tendsto_mul_pow_div_factorial_sub_atTop {K : Type u_1} [Field K] [LinearOrder K] [IsStrictOrderedRing K] [FloorSemiring K] [TopologicalSpace K] [OrderTopology K] (a c : K) (d : ℕ) : Filter.Tendsto (fun (n : ℕ) => a * c ^ n / ↑(n - d).factorial) Filter.atTop (nhds 0)

theorem FloorSemiring.tendsto_pow_div_factorial_atTop {K : Type u_1} [Field K] [LinearOrder K] [IsStrictOrderedRing K] [FloorSemiring K] [TopologicalSpace K] [OrderTopology K] (c : K) : Filter.Tendsto (fun (n : ℕ) => c ^ n / ↑n.factorial) Filter.atTop (nhds 0)

theorem tendsto_floor_atTop {α : Type u_1} [Ring α] [LinearOrder α] [FloorRing α] [IsStrictOrderedRing α] : Filter.Tendsto Int.floor Filter.atTop Filter.atTop

theorem tendsto_floor_atBot {α : Type u_1} [Ring α] [LinearOrder α] [FloorRing α] [IsStrictOrderedRing α] : Filter.Tendsto Int.floor Filter.atBot Filter.atBot

theorem tendsto_ceil_atTop {α : Type u_1} [Ring α] [LinearOrder α] [FloorRing α] [IsStrictOrderedRing α] : Filter.Tendsto Int.ceil Filter.atTop Filter.atTop

theorem tendsto_ceil_atBot {α : Type u_1} [Ring α] [LinearOrder α] [FloorRing α] [IsStrictOrderedRing α] : Filter.Tendsto Int.ceil Filter.atBot Filter.atBot

theorem continuousOn_floor {α : Type u_1} [Ring α] [LinearOrder α] [FloorRing α] [TopologicalSpace α] (n : ℤ) : ContinuousOn (fun (x : α) => ↑⌊x⌋) (Set.Ico (↑n) (↑n + 1))

theorem continuousOn_ceil {α : Type u_1} [Ring α] [LinearOrder α] [FloorRing α] [TopologicalSpace α] (n : ℤ) : ContinuousOn (fun (x : α) => ↑⌈x⌉) (Set.Ioc (↑n - 1) ↑n)

theorem tendsto_floor_right_pure_floor {α : Type u_1} [Ring α] [LinearOrder α] [FloorRing α] [TopologicalSpace α] [OrderClosedTopology α] (x : α) : Filter.Tendsto Int.floor (nhdsWithin x (Set.Ici x)) (pure ⌊x⌋)

theorem tendsto_floor_right_pure {α : Type u_1} [Ring α] [LinearOrder α] [FloorRing α] [TopologicalSpace α] [IsStrictOrderedRing α] [OrderClosedTopology α] (n : ℤ) : Filter.Tendsto Int.floor (nhdsWithin (↑n) (Set.Ici ↑n)) (pure n)

theorem tendsto_ceil_left_pure_ceil {α : Type u_1} [Ring α] [LinearOrder α] [FloorRing α] [TopologicalSpace α] [IsStrictOrderedRing α] [OrderClosedTopology α] (x : α) : Filter.Tendsto Int.ceil (nhdsWithin x (Set.Iic x)) (pure ⌈x⌉)

theorem tendsto_ceil_left_pure {α : Type u_1} [Ring α] [LinearOrder α] [FloorRing α] [TopologicalSpace α] [IsStrictOrderedRing α] [OrderClosedTopology α] (n : ℤ) : Filter.Tendsto Int.ceil (nhdsWithin (↑n) (Set.Iic ↑n)) (pure n)

theorem tendsto_floor_left_pure_ceil_sub_one {α : Type u_1} [Ring α] [LinearOrder α] [FloorRing α] [TopologicalSpace α] [IsStrictOrderedRing α] [OrderClosedTopology α] (x : α) : Filter.Tendsto Int.floor (nhdsWithin x (Set.Iio x)) (pure (⌈x⌉ - 1))

theorem tendsto_floor_left_pure_sub_one {α : Type u_1} [Ring α] [LinearOrder α] [FloorRing α] [TopologicalSpace α] [IsStrictOrderedRing α] [OrderClosedTopology α] (n : ℤ) : Filter.Tendsto Int.floor (nhdsWithin (↑n) (Set.Iio ↑n)) (pure (n - 1))

theorem tendsto_ceil_right_pure_floor_add_one {α : Type u_1} [Ring α] [LinearOrder α] [FloorRing α] [TopologicalSpace α] [OrderClosedTopology α] (x : α) : Filter.Tendsto Int.ceil (nhdsWithin x (Set.Ioi x)) (pure (⌊x⌋ + 1))

theorem tendsto_ceil_right_pure_add_one {α : Type u_1} [Ring α] [LinearOrder α] [FloorRing α] [TopologicalSpace α] [IsStrictOrderedRing α] [OrderClosedTopology α] (n : ℤ) : Filter.Tendsto Int.ceil (nhdsWithin (↑n) (Set.Ioi ↑n)) (pure (n + 1))

theorem tendsto_floor_right {α : Type u_1} [Ring α] [LinearOrder α] [FloorRing α] [TopologicalSpace α] [IsStrictOrderedRing α] [OrderClosedTopology α] (n : ℤ) : Filter.Tendsto (fun (x : α) => ↑⌊x⌋) (nhdsWithin (↑n) (Set.Ici ↑n)) (nhdsWithin (↑n) (Set.Ici ↑n))

theorem tendsto_floor_right' {α : Type u_1} [Ring α] [LinearOrder α] [FloorRing α] [TopologicalSpace α] [IsStrictOrderedRing α] [OrderClosedTopology α] (n : ℤ) : Filter.Tendsto (fun (x : α) => ↑⌊x⌋) (nhdsWithin (↑n) (Set.Ici ↑n)) (nhds ↑n)

theorem tendsto_ceil_left {α : Type u_1} [Ring α] [LinearOrder α] [FloorRing α] [TopologicalSpace α] [IsStrictOrderedRing α] [OrderClosedTopology α] (n : ℤ) : Filter.Tendsto (fun (x : α) => ↑⌈x⌉) (nhdsWithin (↑n) (Set.Iic ↑n)) (nhdsWithin (↑n) (Set.Iic ↑n))

theorem tendsto_ceil_left' {α : Type u_1} [Ring α] [LinearOrder α] [FloorRing α] [TopologicalSpace α] [IsStrictOrderedRing α] [OrderClosedTopology α] (n : ℤ) : Filter.Tendsto (fun (x : α) => ↑⌈x⌉) (nhdsWithin (↑n) (Set.Iic ↑n)) (nhds ↑n)

theorem tendsto_floor_left {α : Type u_1} [Ring α] [LinearOrder α] [FloorRing α] [TopologicalSpace α] [IsStrictOrderedRing α] [OrderClosedTopology α] (n : ℤ) : Filter.Tendsto (fun (x : α) => ↑⌊x⌋) (nhdsWithin (↑n) (Set.Iio ↑n)) (nhdsWithin (↑n - 1) (Set.Iic (↑n - 1)))

theorem tendsto_ceil_right {α : Type u_1} [Ring α] [LinearOrder α] [FloorRing α] [TopologicalSpace α] [IsStrictOrderedRing α] [OrderClosedTopology α] (n : ℤ) : Filter.Tendsto (fun (x : α) => ↑⌈x⌉) (nhdsWithin (↑n) (Set.Ioi ↑n)) (nhdsWithin (↑n + 1) (Set.Ici (↑n + 1)))

theorem tendsto_floor_left' {α : Type u_1} [Ring α] [LinearOrder α] [FloorRing α] [TopologicalSpace α] [IsStrictOrderedRing α] [OrderClosedTopology α] (n : ℤ) : Filter.Tendsto (fun (x : α) => ↑⌊x⌋) (nhdsWithin (↑n) (Set.Iio ↑n)) (nhds (↑n - 1))

theorem tendsto_ceil_right' {α : Type u_1} [Ring α] [LinearOrder α] [FloorRing α] [TopologicalSpace α] [IsStrictOrderedRing α] [OrderClosedTopology α] (n : ℤ) : Filter.Tendsto (fun (x : α) => ↑⌈x⌉) (nhdsWithin (↑n) (Set.Ioi ↑n)) (nhds (↑n + 1))

theorem continuousOn_fract {α : Type u_1} [Ring α] [LinearOrder α] [FloorRing α] [TopologicalSpace α] [IsTopologicalAddGroup α] (n : ℤ) : ContinuousOn Int.fract (Set.Ico (↑n) (↑n + 1))

theorem continuousAt_fract {α : Type u_1} [Ring α] [LinearOrder α] [FloorRing α] [TopologicalSpace α] [OrderClosedTopology α] [IsTopologicalAddGroup α] {x : α} (h : x ≠ ↑⌊x⌋) : ContinuousAt Int.fract x

theorem tendsto_fract_left' {α : Type u_1} [Ring α] [LinearOrder α] [FloorRing α] [TopologicalSpace α] [IsStrictOrderedRing α] [OrderClosedTopology α] [IsTopologicalAddGroup α] (n : ℤ) : Filter.Tendsto Int.fract (nhdsWithin (↑n) (Set.Iio ↑n)) (nhds 1)

theorem tendsto_fract_left {α : Type u_1} [Ring α] [LinearOrder α] [FloorRing α] [TopologicalSpace α] [IsStrictOrderedRing α] [OrderClosedTopology α] [IsTopologicalAddGroup α] (n : ℤ) : Filter.Tendsto Int.fract (nhdsWithin (↑n) (Set.Iio ↑n)) (nhdsWithin 1 (Set.Iio 1))

theorem tendsto_fract_right' {α : Type u_1} [Ring α] [LinearOrder α] [FloorRing α] [TopologicalSpace α] [IsStrictOrderedRing α] [OrderClosedTopology α] [IsTopologicalAddGroup α] (n : ℤ) : Filter.Tendsto Int.fract (nhdsWithin (↑n) (Set.Ici ↑n)) (nhds 0)

theorem tendsto_fract_right {α : Type u_1} [Ring α] [LinearOrder α] [FloorRing α] [TopologicalSpace α] [IsStrictOrderedRing α] [OrderClosedTopology α] [IsTopologicalAddGroup α] (n : ℤ) : Filter.Tendsto Int.fract (nhdsWithin (↑n) (Set.Ici ↑n)) (nhdsWithin 0 (Set.Ici 0))

theorem ContinuousOn.comp_fract' {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Ring α] [LinearOrder α] [FloorRing α] [TopologicalSpace α] [IsStrictOrderedRing α] [OrderTopology α] [TopologicalSpace β] [TopologicalSpace γ] {f : β → α → γ} (h : ContinuousOn (Function.uncurry f) (Set.univ ×ˢ Set.Icc 0 1)) (hf : ∀ (s : β), f s 0 = f s 1) : Continuous fun (st : β × α) => f st.1 (Int.fract st.2)

Do not use this, use ContinuousOn.comp_fract instead.

theorem ContinuousOn.comp_fract {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Ring α] [LinearOrder α] [FloorRing α] [TopologicalSpace α] [IsStrictOrderedRing α] [OrderTopology α] [TopologicalSpace β] [TopologicalSpace γ] {s : β → α} {f : β → α → γ} (h : ContinuousOn (Function.uncurry f) (Set.univ ×ˢ Set.Icc 0 1)) (hs : Continuous s) (hf : ∀ (s : β), f s 0 = f s 1) : Continuous fun (x : β) => f x (Int.fract (s x))

theorem ContinuousOn.comp_fract'' {α : Type u_1} {β : Type u_2} [Ring α] [LinearOrder α] [FloorRing α] [TopologicalSpace α] [IsStrictOrderedRing α] [OrderTopology α] [TopologicalSpace β] {f : α → β} (h : ContinuousOn f (Set.Icc 0 1)) (hf : f 0 = f 1) : Continuous (f ∘ Int.fract)

A special case of ContinuousOn.comp_fract.