Function.Periodic.int_mul_sub_eq
theorem Function.Periodic.int_mul_sub_eq :
∀ {α : Type u_1} {β : Type u_2} {f : α → β} {c x : α} [inst : Ring α],
Function.Periodic f c → ∀ (n : ℤ), f (↑n * c - x) = f (-x)
The theorem `Function.Periodic.int_mul_sub_eq` states that for any type `α` that forms a ring and any function `f` from `α` to another type `β`, if `f` is periodic with period `c`, then for every integer `n` and every value `x` in `α`, the value of `f` at `n * c - x` is the same as the value of `f` at `-x`. In other words, if a function is periodic, then scaling the period by an integer and subtracting any number from it results in a value that is the same as when the original number is negated.
More concisely: If `f` is a periodic function from a ring `α` to another type `β` with period `c`, then for all integers `n` and elements `x` in `α`, `f(n * c - x) = f(-x)`.
|
Function.Antiperiodic.periodic
theorem Function.Antiperiodic.periodic :
∀ {α : Type u_1} {β : Type u_2} {f : α → β} {c : α} [inst : AddMonoid α] [inst_1 : InvolutiveNeg β],
Function.Antiperiodic f c → Function.Periodic f (2 • c)
This theorem states that if a function is antiperiodic with an antiperiod `c`, it is also periodic with a period of `2 • c`. In other words, if a function `f` has the property that `f(x + c) = -f(x)` for all `x` (antiperiodic), then it also has the property that `f(x + 2c) = f(x)` for all `x` (periodic). This holds for any function `f` from a type `α` to a type `β`, where `α` is an additive monoid and `β` supports negation operation.
More concisely: If a function `f` from an additive monoid `α` to a type `β` supporting negation is antiperiodic with antiperiod `c`, then it is periodic with period `2 • c`.
|
Function.Antiperiodic.sub_eq
theorem Function.Antiperiodic.sub_eq :
∀ {α : Type u_1} {β : Type u_2} {f : α → β} {c : α} [inst : AddGroup α] [inst_1 : InvolutiveNeg β],
Function.Antiperiodic f c → ∀ (x : α), f (x - c) = -f x
The theorem `Function.Antiperiodic.sub_eq` states that for any types `α` and `β`, a function `f` from `α` to `β`, and a value `c` of type `α`, under the conditions that `α` forms an additive group and `β` has an involutive negation operation, if the function `f` is antiperiodic with antiperiod `c`, then for every `x` of type `α`, the value of `f` at `x - c` is equal to the negation of `f` at `x`. In simpler terms, if shifting the input of `f` by `c` results in the negation of `f`, then the same holds if we shift the input by `-c`.
More concisely: If `f` is an antiperiodic function from an additive group `α` to a type `β` with involutive negation, with antiperiod `c`, then `f(x - c) = -f(x)` for all `x` in `α`.
|
Function.Periodic.nat_mul
theorem Function.Periodic.nat_mul :
∀ {α : Type u_1} {β : Type u_2} {f : α → β} {c : α} [inst : Semiring α],
Function.Periodic f c → ∀ (n : ℕ), Function.Periodic f (↑n * c)
The theorem `Function.Periodic.nat_mul` states that for any arbitrary types `α` and `β`, given a function `f` from `α` to `β` and an element `c` of `α` such that `f` is periodic with period `c`, then for any natural number `n`, the function `f` is also periodic with period `n * c`. This is under the assumption that `α` is a semiring, which is a type with two associative binary operations where one operation distributes over the other, and the second operation has an identity element.
More concisely: If `f` is a periodic function of period `c` on semiring `α`, then `f` is also periodic with period `n * c`.
|
Function.Antiperiodic.sub_eq'
theorem Function.Antiperiodic.sub_eq' :
∀ {α : Type u_1} {β : Type u_2} {f : α → β} {c x : α} [inst : AddCommGroup α] [inst_1 : Neg β],
Function.Antiperiodic f c → f (c - x) = -f (-x)
The theorem `Function.Antiperiodic.sub_eq'` states that for any types `α` and `β`, any function `f` from `α` to `β`, and any elements `c` and `x` of `α` such that `α` is an additive commutative group and `β` has negation, if `f` is antiperiodic with antiperiod `c`, then the value of `f` at `c - x` is equal to the negation of `f` at `-x`. In other words, if `f` has the property that `f (x + c) = -f x` for all `x`, then `f (c - x) = -f (-x)` for all `x`. The theorem underlines an important symmetry property of antiperiodic functions.
More concisely: For any additive commutative group type `α`, any type `β` with negation, and any antiperiodic function `f` from `α` to `β` with antiperiod `c`, `f (c - x) = -f (-x)` for all `x` in `α`.
|
Function.Periodic.nsmul
theorem Function.Periodic.nsmul :
∀ {α : Type u_1} {β : Type u_2} {f : α → β} {c : α} [inst : AddMonoid α],
Function.Periodic f c → ∀ (n : ℕ), Function.Periodic f (n • c)
The theorem `Function.Periodic.nsmul` states that for any types `α` and `β`, any function `f` from `α` to `β`, and any element `c` of type `α` in an additive monoid, if `f` is periodic with period `c`, then `f` is also periodic with period `n•c` for any natural number `n`. Here, `n•c` denotes the result of adding `c` to itself `n` times.
More concisely: If `f` is a periodic function from type `α` to type `β` with period `c`, then `f` is also periodic with period `nc` for any natural number `n`.
|
Mathlib.Algebra.Periodic._auxLemma.1
theorem Mathlib.Algebra.Periodic._auxLemma.1 :
∀ {G : Type u_1} [inst : AddSemigroup G] (a b c : G), a + (b + c) = a + b + c
This theorem, `Mathlib.Algebra.Periodic._auxLemma.1`, stipulates that for any type `G` that forms an additive semigroup, the operation of addition has the associative property. Specifically, for any three elements `a`, `b`, and `c` of type `G`, the sum of `a` and the sum of `b` and `c` (`a + (b + c)`) is exactly the same as the sum of `a`, `b`, and `c` directly (`a + b + c`). In the language of mathematics, this corresponds to the familiar associative property $a + (b + c) = (a + b) + c$ for addition in a semigroup.
More concisely: The theorem `Mathlib.Algebra.Periodic._auxLemma.1` asserts that addition is associative in an additive semigroup. That is, for any additive semigroup `G`, and elements `a, b, c` in `G`, we have `a + (b + c) = (a + b) + c`.
|
Function.Periodic.eq
theorem Function.Periodic.eq :
∀ {α : Type u_1} {β : Type u_2} {f : α → β} {c : α} [inst : AddZeroClass α], Function.Periodic f c → f c = f 0 := by
sorry
The theorem `Function.Periodic.eq` states that for any types `α` and `β`, any function `f` from `α` to `β`, and any `c` of type `α`, given an instance of `AddZeroClass` for `α`, if the function `f` is periodic with period `c`, then the value of the function `f` at `c` is equal to the value of the function `f` at `0`. In mathematical terms, if `f` is a function such that `f(x + c) = f(x)` for all `x` in `α`, then `f(c) = f(0)`.
More concisely: If `f` is a periodic function of period `c` from type `α` to type `β`, then `f(c) = f(0)`.
|
Function.Antiperiodic.nat_mul_eq_of_eq_zero
theorem Function.Antiperiodic.nat_mul_eq_of_eq_zero :
∀ {α : Type u_1} {β : Type u_2} {f : α → β} {c : α} [inst : Semiring α] [inst_1 : NegZeroClass β],
Function.Antiperiodic f c → f 0 = 0 → ∀ (n : ℕ), f (↑n * c) = 0
The theorem `Function.Antiperiodic.nat_mul_eq_of_eq_zero` states that for any function `f` from a type `α` to a type `β`, and any value `c` of type `α`, given that the semiring structure is defined on `α` and the negation-zero class is defined on `β`, if `f` is antiperiodic with antiperiod `c` and `f` at zero equals zero, then for all natural numbers `n`, `f` at the product of `n` and `c` equals zero. In other words, if a function is antiperiodic at some point and equals zero at that point, then it will also equal zero at all points that are multiples of the antiperiod.
More concisely: If `f` is an Antiperiodic function from type `α` to type `β`, with antiperiod `c` and `f(c) = 0`, then `f(n * c) = 0` for all natural numbers `n`.
|
Function.Periodic.add_antiperiod_eq
theorem Function.Periodic.add_antiperiod_eq :
∀ {α : Type u_1} {β : Type u_2} {f : α → β} {c₁ c₂ : α} [inst : AddGroup α] [inst_1 : Neg β],
Function.Periodic f c₁ → Function.Antiperiodic f c₂ → f (c₁ + c₂) = -f 0
The theorem `Function.Periodic.add_antiperiod_eq` states that for any function `f` mapping from a type `α` to a type `β`, given two elements `c₁` and `c₂` of type `α` and assuming that the type `α` has a group structure under addition and the type `β` has a negation operation, if the function `f` is periodic with period `c₁` and antiperiodic with period `c₂`, then the value of the function at the point `c₁ + c₂` is equal to the negation of the value of the function at the origin (i.e., `f (c₁ + c₂) = -f 0`). In mathematical terms, this could be read as "For a function $f: \alpha \rightarrow \beta$, if $f$ is $c_1$-periodic and $c_2$-antiperiodic, then $f(c_1 + c_2) = -f(0)$".
More concisely: If a function $f:\alpha \rightarrow \beta$ is $\alpha$-periodic with period $c\_1$ and $\alpha$-antiperiodic with period $c\_2$, then $f(c\_1 + c\_2) = -f(0)$.
|
Function.Periodic.sub_eq
theorem Function.Periodic.sub_eq :
∀ {α : Type u_1} {β : Type u_2} {f : α → β} {c : α} [inst : AddGroup α],
Function.Periodic f c → ∀ (x : α), f (x - c) = f x
The theorem `Function.Periodic.sub_eq` states that for any function `f` mapping from a type `α` to another type `β`, being `periodic` with period `c` implies that for all `x` of type `α`, the value of `f` at `x - c` is equal to the value of `f` at `x`. Here, `α` is a type with an addition operation and an inverse operation (making it an AddGroup). This theorem essentially tells us that if a function repeats its values after adding a certain constant, it will also repeat its values after subtracting the same constant.
More concisely: If `f` is a periodic function on an additive group `α` with period `c`, then `f(x) = f(x - c)` for all `x` in `α`.
|
Function.Periodic.sub_antiperiod_eq
theorem Function.Periodic.sub_antiperiod_eq :
∀ {α : Type u_1} {β : Type u_2} {f : α → β} {c₁ c₂ : α} [inst : AddGroup α] [inst_1 : InvolutiveNeg β],
Function.Periodic f c₁ → Function.Antiperiodic f c₂ → f (c₁ - c₂) = -f 0
The theorem `Function.Periodic.sub_antiperiod_eq` states that for any types `α` and `β`, a function `f` from `α` to `β`, and any two elements `c₁` and `c₂` of `α`, given an additive group structure on `α` and a negation operation on `β` which is an involution, if `f` is periodic with period `c₁` and antiperiodic with antiperiod `c₂`, then the value of `f` at `c₁ - c₂` is the negation of the value of `f` at `0`. In other words, if a function is both periodic and antiperiodic with two different periods, then the function evaluated at the difference of these periods equals the negative of the function evaluated at zero.
More concisely: If a function from one type to another is periodic with period c₁ and antiperiodic with antiperiod c₂, then it holds that f(c₁ - c₂) = -f(0).
|
Function.Antiperiodic.neg
theorem Function.Antiperiodic.neg :
∀ {α : Type u_1} {β : Type u_2} {f : α → β} {c : α} [inst : AddGroup α] [inst_1 : InvolutiveNeg β],
Function.Antiperiodic f c → Function.Antiperiodic f (-c)
This theorem states that if a function `f` is antiperiodic with antiperiod `c`, then it is also antiperiodic with antiperiod `-c`. Specifically, for any types `α` and `β`, if `f` is a function from `α` to `β`, `c` is an element of `α`, `α` is an additive group and `β` has an operation of negation that is involutive (meaning that negating twice gives the original value), then if `f` satisfies the property that for every `x` in `α`, `f(x + c) = -f(x)`, it also satisfies the property that for every `x` in `α`, `f(x - c) = -f(x)`.
More concisely: If a function `f` from an additive group `α` to a negation-commutative type `β` is antiperiodic with antiperiod `c`, then it is also antiperiodic with antiperiod `-c` (i.e., for all `x` in `α`, `f(x + c) = -f(x)` implies `f(x - c) = -f(x)`).
|
Function.Periodic.exists_mem_Ico₀
theorem Function.Periodic.exists_mem_Ico₀ :
∀ {α : Type u_1} {β : Type u_2} {f : α → β} {c : α} [inst : LinearOrderedAddCommGroup α] [inst_1 : Archimedean α],
Function.Periodic f c → 0 < c → ∀ (x : α), ∃ y ∈ Set.Ico 0 c, f x = f y
This theorem states that if a function `f` is periodic with a positive period `c`, then for every value `x` we can find a `y` in the left-closed right-open interval from 0 to `c` (denoted `Ico 0 c`), such that `f(x) = f(y)`. In other words, within every period of the function, you can find a value that the function has already taken in the first instance of that period.
More concisely: Given a periodic function `f` with positive period `c`, there exists a `y` in the interval `Ico 0 c` such that `f(x) = f(y)` for all `x`.
|
Function.Periodic.not_injective
theorem Function.Periodic.not_injective :
∀ {R : Type u_4} {X : Type u_5} [inst : AddZeroClass R] {f : R → X} {c : R},
Function.Periodic f c → c ≠ 0 → ¬Function.Injective f
The theorem states that a periodic function `f`, which maps from a type `R` to a type `X`, on a semiring or, more generally, on an `AddZeroClass`, is not injective if its period `c` is non-zero. In other words, if a function `f` repeats its values after a non-zero period `c` (i.e., `f(x + c) = f(x)` for all `x`), then there exist at least two different inputs that map to the same output, thus the function is not injective. The `AddZeroClass R` context means that `R` has addition and zero operations satisfying the usual laws.
More concisely: A periodic function `f` from a semiring `R` to a type `X` with non-zero period `c` is not injective.
|
Function.Periodic.neg
theorem Function.Periodic.neg :
∀ {α : Type u_1} {β : Type u_2} {f : α → β} {c : α} [inst : AddGroup α],
Function.Periodic f c → Function.Periodic f (-c)
The theorem `Function.Periodic.neg` states that for any type `α` with an addition group structure, and any function `f` from `α` to another type `β`, if `f` is periodic with period `c`, then it is also periodic with period `-c`. In other words, if for all `x` in `α`, `f(x + c) = f(x)`, then `f(x - c) = f(x)`. It expresses the property of a periodic function that reversing the direction of its period does not alter its periodicity.
More concisely: If a function `f` from a type `α` to another type `β` with an additive group structure is periodic with period `c`, then it is also periodic with period `-c`.
|
Function.Periodic.sub_nat_mul_eq
theorem Function.Periodic.sub_nat_mul_eq :
∀ {α : Type u_1} {β : Type u_2} {f : α → β} {c x : α} [inst : Ring α],
Function.Periodic f c → ∀ (n : ℕ), f (x - ↑n * c) = f x
The theorem `Function.Periodic.sub_nat_mul_eq` states that for any type `α` with a ring structure, type `β`, and a function `f` from `α` to `β`, if `f` is periodic with period `c`, then for any natural number `n` and any element `x` of `α`, the value of `f` at `x - n * c` is equal to the value of `f` at `x`. In other words, subtracting any natural number multiple of the period from the input does not change the output of a periodic function.
More concisely: If `f` is a periodic function from a ring `α` to a type `β` with period `c`, then for all `x ∈ α` and `n ∈ ℕ`, `f(x - n * c) = f(x)`.
|
Function.Periodic.sub_int_mul_eq
theorem Function.Periodic.sub_int_mul_eq :
∀ {α : Type u_1} {β : Type u_2} {f : α → β} {c x : α} [inst : Ring α],
Function.Periodic f c → ∀ (n : ℤ), f (x - ↑n * c) = f x
The theorem `Function.Periodic.sub_int_mul_eq` states that for any types `α` and `β`, any function `f` from `α` to `β`, any elements `c` and `x` of type `α`, and any instance of `α` as a ring, if the function `f` is periodic with period `c`, then for any integer `n`, the value of the function `f` at the point `x - n*c` is equal to the value of the function at `x`. In simpler terms, it means that for a periodic function, subtracting any integer multiple of the period from the argument doesn't change the value of the function.
More concisely: For any types `α` and `β`, periodic function `f : α → β` with period `c`, and elements `x : α` and `n : ℤ`, `f (x - n*c) = f x`.
|
Function.Periodic.int_mul_eq
theorem Function.Periodic.int_mul_eq :
∀ {α : Type u_1} {β : Type u_2} {f : α → β} {c : α} [inst : Ring α],
Function.Periodic f c → ∀ (n : ℤ), f (↑n * c) = f 0
The theorem `Function.Periodic.int_mul_eq` asserts that for any type `α` which forms a ring, and any function `f` from `α` to an arbitrary type `β`, if `f` is periodic with period `c`, then for any integer `n`, the value of `f` at the product of `n` (coerced to `α`) and `c` is equal to `f` at zero. In other words, if a function is periodic, the value of the function at any integral multiple of the period is the same as the value of the function at zero.
More concisely: For any ring type `α` and periodic function `f` from `α` to a type `β`, the value `f (n * c)` equals `f 0` for all integers `n`, where `c` is the period of `f`.
|
Function.Antiperiodic.eq
theorem Function.Antiperiodic.eq :
∀ {α : Type u_1} {β : Type u_2} {f : α → β} {c : α} [inst : AddZeroClass α] [inst_1 : Neg β],
Function.Antiperiodic f c → f c = -f 0
The theorem `Function.Antiperiodic.eq` states that for any types `α` and `β`, any function `f` from `α` to `β`, and any value `c` of type `α`, given that `α` possesses a zero element with respect to addition (`AddZeroClass α`), and that `β` has a negation operation (`Neg β`), if `f` is antiperiodic with antiperiod `c` (which by definition signifies that for all `x` in `α`, `f (x + c) = -f x`), then `f c` is equal to the negation of `f` at zero, that is, `f c = -f 0`.
More concisely: If `α` is an additive group and `β` has negations, an antiperiodic function `f` from `α` to `β` with antiperiod `c` satisfies `f(c) = -f(0)`.
|
Function.Periodic.int_mul
theorem Function.Periodic.int_mul :
∀ {α : Type u_1} {β : Type u_2} {f : α → β} {c : α} [inst : Ring α],
Function.Periodic f c → ∀ (n : ℤ), Function.Periodic f (↑n * c)
The theorem `Function.Periodic.int_mul` states that for any type `α` and `β`, given a function `f` mapping `α` to `β`, a value `c` of type α, and an instance of `Ring α`, if the function `f` is periodic with period `c`, then for any integer `n`, the function `f` will also be periodic with period `n*c`. In mathematical terms, if `f(x+c) = f(x)` for all `x`, then `f(x+n*c) = f(x)` for all `x` and all integers `n`, where `f : α → β` and `c` and `x` are elements of a ring `α`.
More concisely: If a function `f : α → β` over a ring `α` is periodic with period `c`, then it is also periodic with period `n*c` for any integer `n`.
|
Function.Periodic.exists_mem_Ico
theorem Function.Periodic.exists_mem_Ico :
∀ {α : Type u_1} {β : Type u_2} {f : α → β} {c : α} [inst : LinearOrderedAddCommGroup α] [inst_1 : Archimedean α],
Function.Periodic f c → 0 < c → ∀ (x a : α), ∃ y ∈ Set.Ico a (a + c), f x = f y
The theorem `Function.Periodic.exists_mem_Ico` states that if a function `f` is periodic with a positive period `c`, then for any given `x` and `a` there exists a `y` in the left-closed right-open interval from `a` to `a + c` (denoted `Ico a (a + c)`), such that the value of `f` at `x` is equal to the value of `f` at `y`. This means, in the context of the function's periodicity, that there's always a point in every period interval where the function attains the same value as any other given point.
More concisely: Given a periodic function `f` with positive period `c`, there exists a point `y` in the interval `[a, a + c)` such that `f(x) = f(y)` for any `x`.
|
Function.Periodic.exists_mem_Ioc
theorem Function.Periodic.exists_mem_Ioc :
∀ {α : Type u_1} {β : Type u_2} {f : α → β} {c : α} [inst : LinearOrderedAddCommGroup α] [inst_1 : Archimedean α],
Function.Periodic f c → 0 < c → ∀ (x a : α), ∃ y ∈ Set.Ioc a (a + c), f x = f y
The theorem `Function.Periodic.exists_mem_Ioc` states that if a function `f` is periodic with a positive period `c`, then for any given `x` and `a`, there exists some `y` in the left-open right-closed interval from `a` to `a + c` (denoted as `Ioc a (a + c)`), such that the value of the function at `x` is equal to the value of the function at `y`. This assumes that the domain of `f` is a linearly ordered additive commutative group, and that we are working in an Archimedean field, which loosely speaking, means that there are no infinitely small or infinitely large elements.
More concisely: If `f` is a periodic function with period `c` defined over an Archimedean field, then for any `x` and `a`, there exists `y` in the interval `[a, a + c)` such that `f(x) = f(y)`.
|
Function.Periodic.sub_eq'
theorem Function.Periodic.sub_eq' :
∀ {α : Type u_1} {β : Type u_2} {f : α → β} {c x : α} [inst : AddCommGroup α],
Function.Periodic f c → f (c - x) = f (-x)
The theorem named `Function.Periodic.sub_eq'` states that, for any types `α` and `β`, and for any function `f` from `α` to `β` and elements `c` and `x` of `α`, if `α` forms an additive commutative group and the function `f` is periodic with period `c`, then the function evaluated at `c - x` equals the function evaluated at `-x`.
More concisely: For any additive commutative group type `α`, periodic function `f` from `α` to `β`, and elements `c`, `x` of `α`, if `f` has period `c`, then `f(c - x) = f(-x)`.
|
Function.Periodic.const_smul₀
theorem Function.Periodic.const_smul₀ :
∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → β} {c : α} [inst : AddCommMonoid α]
[inst_1 : DivisionSemiring γ] [inst_2 : Module γ α],
Function.Periodic f c → ∀ (a : γ), Function.Periodic (fun x => f (a • x)) (a⁻¹ • c)
This theorem states that if a function `f` is periodic with period `c`, then for any scalar `a`, the function obtained by scaling the argument of `f` by `a` is also periodic, with the period scaled by the inverse of `a`. This is formalized over a division semiring `γ`, a module `α` over `γ`, and an additive commutative monoid `α`, allowing scalar multiplication and division. The function `f` maps elements from `α` to another type `β`, and the periodicity of `f` is defined such that for all `x` in `α`, `f (x + c) = f x`.
More concisely: If `f` is a periodic function with period `c` over a division semiring `γ`, a module `α` over `γ`, and an additive commutative monoid `α`, then the scaled function `a → f(xa)` is periodic with period `c/a` for any scalar `a` in `γ`.
|
Function.Periodic.nat_mul_sub_eq
theorem Function.Periodic.nat_mul_sub_eq :
∀ {α : Type u_1} {β : Type u_2} {f : α → β} {c x : α} [inst : Ring α],
Function.Periodic f c → ∀ (n : ℕ), f (↑n * c - x) = f (-x)
The theorem `Function.Periodic.nat_mul_sub_eq` states that for any type `α` and `β`, any function `f` from `α` to `β`, any elements `c` and `x` of type `α`, and any natural number `n`, if `α` is a ring and `f` is a periodic function with period `c`, then `f` applied to the difference of the product of `n` and `c` and `x` is equal to `f` applied to the negation of `x`. In mathematical terms, it says that if `f` is a periodic function with period `c`, then for every natural number `n`, we have `f(n*c - x) = f(-x)`.
More concisely: If `f` is a periodic function on a ring with period `c`, then `f(nc - x) = f(-x)` for all natural numbers `n` and elements `x`.
|
Function.Periodic.nat_mul_eq
theorem Function.Periodic.nat_mul_eq :
∀ {α : Type u_1} {β : Type u_2} {f : α → β} {c : α} [inst : Semiring α],
Function.Periodic f c → ∀ (n : ℕ), f (↑n * c) = f 0
The theorem `Function.Periodic.nat_mul_eq` states that for any type `α` with a semiring structure, any type `β`, any function `f` from `α` to `β`, and any element `c` of `α`, if the function `f` is periodic with period `c`, then for all natural numbers `n`, the function evaluated at `n*c` (where `n*c` is the multiplication of the natural number `n` with `c`) is equal to the function evaluated at `0`. In mathematical terms, if `f(x + c) = f(x)` for all `x`, then `f(n*c) = f(0)` for all natural numbers `n`.
More concisely: If `f` is a periodic function with period `c` on a semiring `α`, then `f(n * c) = f(0)` for all natural numbers `n`.
|
Function.Periodic.zsmul
theorem Function.Periodic.zsmul :
∀ {α : Type u_1} {β : Type u_2} {f : α → β} {c : α} [inst : AddGroup α],
Function.Periodic f c → ∀ (n : ℤ), Function.Periodic f (n • c)
The theorem `Function.Periodic.zsmul` states that for any types `α` and `β`, any function `f` from `α` to `β`, any element `c` of `α`, and any integer `n`, if `f` is periodic with period `c` (i.e., for all `x` in `α`, `f(x + c) = f(x)`), then `f` is also periodic with period `n • c` (i.e., for all `x` in `α`, `f(x + n•c) = f(x)`). This is under the assumption that `α` forms an additive group. In simpler terms, if a function is periodic with a certain period, then it is also periodic with any integer multiple of that period.
More concisely: If `α` is an additive group, `f:` `α` `->` `β` is periodic with period `c` in `α`, then `f` is also periodic with period `n • c` for any integer `n`.
|
Function.Antiperiodic.const_smul₀
theorem Function.Antiperiodic.const_smul₀ :
∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → β} {c : α} [inst : AddCommMonoid α] [inst_1 : Neg β]
[inst_2 : DivisionSemiring γ] [inst_3 : Module γ α],
Function.Antiperiodic f c → ∀ {a : γ}, a ≠ 0 → Function.Antiperiodic (fun x => f (a • x)) (a⁻¹ • c)
The theorem `Function.Antiperiodic.const_smul₀` states that given types `α`, `β`, and `γ`, a function `f` from `α` to `β`, and a constant `c` of type `α`, under the conditions that `α` is an additive commutative monoid, `β` is equipped with a negation operation, `γ` is a division semiring, and `α` is a module over `γ`, if the function `f` is antiperiodic with antiperiod `c`, then for any nonzero element `a` of `γ`, the function resulting from applying `f` to the scalar multiple `a • x` is also antiperiodic, but with antiperiod `a⁻¹ • c`, where `•` denotes scalar multiplication and `a⁻¹` is the multiplicative inverse of `a`. In essence, this theorem relates the antiperiodicity of a function and a scaled version of that function.
More concisely: If `f : α -> β`, `α` an additive commutative monoid, `β` a negated semiring, `γ` a division semiring, `α` a `γ`-module, `c : α`, and `f` is antiperiodic with antiperiod `c`, then for any nonzero `a : γ`, the function `x => f (a • x)` is antiperiodic with antiperiod `a⁻¹ • c`.
|