|
| 1 | +/- |
| 2 | +Copyright (c) 2021 Benjamin Davidson. All rights reserved. |
| 3 | +Released under Apache 2.0 license as described in the file LICENSE. |
| 4 | +Authors: Benjamin Davidson |
| 5 | +-/ |
| 6 | +import Mathlib.Algebra.Field.Opposite |
| 7 | +import Mathlib.Algebra.Module.Opposite |
| 8 | +import Mathlib.Algebra.Order.Archimedean.Basic |
| 9 | +import Mathlib.Algebra.Ring.Periodic |
| 10 | + |
| 11 | +/-! |
| 12 | +# Periodic functions |
| 13 | +
|
| 14 | +This file proves facts about periodic and antiperiodic functions from and to a field. |
| 15 | +
|
| 16 | +## Main definitions |
| 17 | +
|
| 18 | +* `Function.Periodic`: A function `f` is *periodic* if `∀ x, f (x + c) = f x`. |
| 19 | + `f` is referred to as periodic with period `c` or `c`-periodic. |
| 20 | +
|
| 21 | +* `Function.Antiperiodic`: A function `f` is *antiperiodic* if `∀ x, f (x + c) = -f x`. |
| 22 | + `f` is referred to as antiperiodic with antiperiod `c` or `c`-antiperiodic. |
| 23 | +
|
| 24 | +Note that any `c`-antiperiodic function will necessarily also be `2 • c`-periodic. |
| 25 | +
|
| 26 | +## Tags |
| 27 | +
|
| 28 | +period, periodic, periodicity, antiperiodic |
| 29 | +-/ |
| 30 | + |
| 31 | +assert_not_exists TwoSidedIdeal |
| 32 | + |
| 33 | +variable {α β γ : Type*} {f g : α → β} {c c₁ c₂ x : α} |
| 34 | + |
| 35 | +open Set |
| 36 | + |
| 37 | +namespace Function |
| 38 | + |
| 39 | +/-! ### Periodicity -/ |
| 40 | + |
| 41 | +protected theorem Periodic.const_smul₀ [AddCommMonoid α] [DivisionSemiring γ] [Module γ α] |
| 42 | + (h : Periodic f c) (a : γ) : Periodic (fun x => f (a • x)) (a⁻¹ • c) := fun x => by |
| 43 | + by_cases ha : a = 0 |
| 44 | + · simp only [ha, zero_smul] |
| 45 | + · simpa only [smul_add, smul_inv_smul₀ ha] using h (a • x) |
| 46 | + |
| 47 | +protected theorem Periodic.const_mul [DivisionSemiring α] (h : Periodic f c) (a : α) : |
| 48 | + Periodic (fun x => f (a * x)) (a⁻¹ * c) := |
| 49 | + Periodic.const_smul₀ h a |
| 50 | + |
| 51 | +theorem Periodic.const_inv_smul₀ [AddCommMonoid α] [DivisionSemiring γ] [Module γ α] |
| 52 | + (h : Periodic f c) (a : γ) : Periodic (fun x => f (a⁻¹ • x)) (a • c) := by |
| 53 | + simpa only [inv_inv] using h.const_smul₀ a⁻¹ |
| 54 | + |
| 55 | +theorem Periodic.const_inv_mul [DivisionSemiring α] (h : Periodic f c) (a : α) : |
| 56 | + Periodic (fun x => f (a⁻¹ * x)) (a * c) := |
| 57 | + h.const_inv_smul₀ a |
| 58 | + |
| 59 | +theorem Periodic.mul_const [DivisionSemiring α] (h : Periodic f c) (a : α) : |
| 60 | + Periodic (fun x => f (x * a)) (c * a⁻¹) := |
| 61 | + h.const_smul₀ (MulOpposite.op a) |
| 62 | + |
| 63 | +theorem Periodic.mul_const' [DivisionSemiring α] (h : Periodic f c) (a : α) : |
| 64 | + Periodic (fun x => f (x * a)) (c / a) := by simpa only [div_eq_mul_inv] using h.mul_const a |
| 65 | + |
| 66 | +theorem Periodic.mul_const_inv [DivisionSemiring α] (h : Periodic f c) (a : α) : |
| 67 | + Periodic (fun x => f (x * a⁻¹)) (c * a) := |
| 68 | + h.const_inv_smul₀ (MulOpposite.op a) |
| 69 | + |
| 70 | +theorem Periodic.div_const [DivisionSemiring α] (h : Periodic f c) (a : α) : |
| 71 | + Periodic (fun x => f (x / a)) (c * a) := by simpa only [div_eq_mul_inv] using h.mul_const_inv a |
| 72 | + |
| 73 | +/-- If a function `f` is `Periodic` with positive period `c`, then for all `x` there exists some |
| 74 | + `y ∈ Ico 0 c` such that `f x = f y`. -/ |
| 75 | +theorem Periodic.exists_mem_Ico₀ [LinearOrderedAddCommGroup α] [Archimedean α] (h : Periodic f c) |
| 76 | + (hc : 0 < c) (x) : ∃ y ∈ Ico 0 c, f x = f y := |
| 77 | + let ⟨n, H, _⟩ := existsUnique_zsmul_near_of_pos' hc x |
| 78 | + ⟨x - n • c, H, (h.sub_zsmul_eq n).symm⟩ |
| 79 | + |
| 80 | +/-- If a function `f` is `Periodic` with positive period `c`, then for all `x` there exists some |
| 81 | + `y ∈ Ico a (a + c)` such that `f x = f y`. -/ |
| 82 | +theorem Periodic.exists_mem_Ico [LinearOrderedAddCommGroup α] [Archimedean α] (h : Periodic f c) |
| 83 | + (hc : 0 < c) (x a) : ∃ y ∈ Ico a (a + c), f x = f y := |
| 84 | + let ⟨n, H, _⟩ := existsUnique_add_zsmul_mem_Ico hc x a |
| 85 | + ⟨x + n • c, H, (h.zsmul n x).symm⟩ |
| 86 | + |
| 87 | +/-- If a function `f` is `Periodic` with positive period `c`, then for all `x` there exists some |
| 88 | + `y ∈ Ioc a (a + c)` such that `f x = f y`. -/ |
| 89 | +theorem Periodic.exists_mem_Ioc [LinearOrderedAddCommGroup α] [Archimedean α] (h : Periodic f c) |
| 90 | + (hc : 0 < c) (x a) : ∃ y ∈ Ioc a (a + c), f x = f y := |
| 91 | + let ⟨n, H, _⟩ := existsUnique_add_zsmul_mem_Ioc hc x a |
| 92 | + ⟨x + n • c, H, (h.zsmul n x).symm⟩ |
| 93 | + |
| 94 | +theorem Periodic.image_Ioc [LinearOrderedAddCommGroup α] [Archimedean α] (h : Periodic f c) |
| 95 | + (hc : 0 < c) (a : α) : f '' Ioc a (a + c) = range f := |
| 96 | + (image_subset_range _ _).antisymm <| range_subset_iff.2 fun x => |
| 97 | + let ⟨y, hy, hyx⟩ := h.exists_mem_Ioc hc x a |
| 98 | + ⟨y, hy, hyx.symm⟩ |
| 99 | + |
| 100 | +theorem Periodic.image_Icc [LinearOrderedAddCommGroup α] [Archimedean α] (h : Periodic f c) |
| 101 | + (hc : 0 < c) (a : α) : f '' Icc a (a + c) = range f := |
| 102 | + (image_subset_range _ _).antisymm <| h.image_Ioc hc a ▸ image_subset _ Ioc_subset_Icc_self |
| 103 | + |
| 104 | +theorem Periodic.image_uIcc [LinearOrderedAddCommGroup α] [Archimedean α] (h : Periodic f c) |
| 105 | + (hc : c ≠ 0) (a : α) : f '' uIcc a (a + c) = range f := by |
| 106 | + cases hc.lt_or_lt with |
| 107 | + | inl hc => |
| 108 | + rw [uIcc_of_ge (add_le_of_nonpos_right hc.le), ← h.neg.image_Icc (neg_pos.2 hc) (a + c), |
| 109 | + add_neg_cancel_right] |
| 110 | + | inr hc => rw [uIcc_of_le (le_add_of_nonneg_right hc.le), h.image_Icc hc] |
| 111 | + |
| 112 | +/-! ### Antiperiodicity -/ |
| 113 | + |
| 114 | +theorem Antiperiodic.add_nat_mul_eq [Semiring α] [Ring β] (h : Antiperiodic f c) (n : ℕ) : |
| 115 | + f (x + n * c) = (-1) ^ n * f x := by |
| 116 | + simpa only [nsmul_eq_mul, zsmul_eq_mul, Int.cast_pow, Int.cast_neg, |
| 117 | + Int.cast_one] using h.add_nsmul_eq n |
| 118 | + |
| 119 | +theorem Antiperiodic.sub_nat_mul_eq [Ring α] [Ring β] (h : Antiperiodic f c) (n : ℕ) : |
| 120 | + f (x - n * c) = (-1) ^ n * f x := by |
| 121 | + simpa only [nsmul_eq_mul, zsmul_eq_mul, Int.cast_pow, Int.cast_neg, |
| 122 | + Int.cast_one] using h.sub_nsmul_eq n |
| 123 | + |
| 124 | +theorem Antiperiodic.nat_mul_sub_eq [Ring α] [Ring β] (h : Antiperiodic f c) (n : ℕ) : |
| 125 | + f (n * c - x) = (-1) ^ n * f (-x) := by |
| 126 | + simpa only [nsmul_eq_mul, zsmul_eq_mul, Int.cast_pow, Int.cast_neg, |
| 127 | + Int.cast_one] using h.nsmul_sub_eq n |
| 128 | + |
| 129 | +theorem Antiperiodic.const_smul₀ [AddCommMonoid α] [Neg β] [DivisionSemiring γ] [Module γ α] |
| 130 | + (h : Antiperiodic f c) {a : γ} (ha : a ≠ 0) : Antiperiodic (fun x => f (a • x)) (a⁻¹ • c) := |
| 131 | + fun x => by simpa only [smul_add, smul_inv_smul₀ ha] using h (a • x) |
| 132 | + |
| 133 | +theorem Antiperiodic.const_mul [DivisionSemiring α] [Neg β] (h : Antiperiodic f c) {a : α} |
| 134 | + (ha : a ≠ 0) : Antiperiodic (fun x => f (a * x)) (a⁻¹ * c) := |
| 135 | + h.const_smul₀ ha |
| 136 | + |
| 137 | +theorem Antiperiodic.const_inv_smul₀ [AddCommMonoid α] [Neg β] [DivisionSemiring γ] [Module γ α] |
| 138 | + (h : Antiperiodic f c) {a : γ} (ha : a ≠ 0) : Antiperiodic (fun x => f (a⁻¹ • x)) (a • c) := by |
| 139 | + simpa only [inv_inv] using h.const_smul₀ (inv_ne_zero ha) |
| 140 | + |
| 141 | +theorem Antiperiodic.const_inv_mul [DivisionSemiring α] [Neg β] (h : Antiperiodic f c) {a : α} |
| 142 | + (ha : a ≠ 0) : Antiperiodic (fun x => f (a⁻¹ * x)) (a * c) := |
| 143 | + h.const_inv_smul₀ ha |
| 144 | + |
| 145 | +theorem Antiperiodic.mul_const [DivisionSemiring α] [Neg β] (h : Antiperiodic f c) {a : α} |
| 146 | + (ha : a ≠ 0) : Antiperiodic (fun x => f (x * a)) (c * a⁻¹) := |
| 147 | + h.const_smul₀ <| (MulOpposite.op_ne_zero_iff a).mpr ha |
| 148 | + |
| 149 | +theorem Antiperiodic.mul_const' [DivisionSemiring α] [Neg β] (h : Antiperiodic f c) {a : α} |
| 150 | + (ha : a ≠ 0) : Antiperiodic (fun x => f (x * a)) (c / a) := by |
| 151 | + simpa only [div_eq_mul_inv] using h.mul_const ha |
| 152 | + |
| 153 | +theorem Antiperiodic.mul_const_inv [DivisionSemiring α] [Neg β] (h : Antiperiodic f c) {a : α} |
| 154 | + (ha : a ≠ 0) : Antiperiodic (fun x => f (x * a⁻¹)) (c * a) := |
| 155 | + h.const_inv_smul₀ <| (MulOpposite.op_ne_zero_iff a).mpr ha |
| 156 | + |
| 157 | +theorem Antiperiodic.div_inv [DivisionSemiring α] [Neg β] (h : Antiperiodic f c) {a : α} |
| 158 | + (ha : a ≠ 0) : Antiperiodic (fun x => f (x / a)) (c * a) := by |
| 159 | + simpa only [div_eq_mul_inv] using h.mul_const_inv ha |
| 160 | + |
| 161 | +end Function |
| 162 | + |
| 163 | +theorem Int.fract_periodic (α) [LinearOrderedRing α] [FloorRing α] : |
| 164 | + Function.Periodic Int.fract (1 : α) := fun a => mod_cast Int.fract_add_int a 1 |
0 commit comments