def IsPeriodicWithPeriod (L : ℝ) (f : ℝ → ℂ) : Prop

Definition 5.1.1: Let L > 0. A function f : ℝ → ℂ is periodic with period L if for every x : ℝ, one has f (x + L) = f x.

Equations

• IsPeriodicWithPeriod L f = (0 < L ∧ Function.Periodic f L)

def IsZPeriodic (f : ℝ → ℂ) : Prop

Definition 5.1.2 (ℤ-periodic and Lℤ-periodic): A function f : ℝ → ℂ is ℤ-periodic iff it is 1-periodic, i.e. f (x + 1) = f x for all x : ℝ.

Equations

• IsZPeriodic f = Function.Periodic f 1

@[reducible, inline]

abbrev IsLZPeriodic (L : ℝ) (f : ℝ → ℂ) : Prop

A function is Lℤ-periodic when it is periodic with positive period L.

Equations

• IsLZPeriodic L f = IsPeriodicWithPeriod L f

noncomputable def integerPart (x : ℝ) : ℤ

Definition 5.1.3 (Integer part and fractional part): for x : ℝ, [x] is the unique integer k : ℤ such that k ≤ x < k + 1.

Equations

• integerPart x = ⌊x⌋

noncomputable def fractionalPart (x : ℝ) : ℝ

The fractional part of x : ℝ, defined by {x} = x - [x].

Equations

• fractionalPart x = x - ↑(integerPart x)

theorem helperForExample_5_1_2_realToComplex_periodic {g : ℝ → ℝ} {T : ℝ} (hg : Function.Periodic g T) : Function.Periodic (fun (x : ℝ) => ↑(g x)) T

Helper for Example 5.1.2: periodicity is preserved when viewing a real-valued periodic function as complex-valued via coercion.

theorem helperForExample_5_1_2_base_periodic_trig_exp : Function.Periodic (fun (x : ℝ) => ↑(Real.sin x)) (2 * Real.pi) ∧ Function.Periodic (fun (x : ℝ) => ↑(Real.cos x)) (2 * Real.pi) ∧ Function.Periodic (fun (x : ℝ) => Complex.exp (↑x * Complex.I)) (2 * Real.pi)

Helper for Example 5.1.2: base 2π-periodicity for sin, cos, and x ↦ exp(ix) in the ℝ → ℂ setting.

theorem helperForExample_5_1_2_periodic_mul_int_right {f : ℝ → ℂ} {L : ℝ} (hf : Function.Periodic f L) (k : ℤ) : Function.Periodic f (L * ↑k)

Helper for Example 5.1.2: if f is L-periodic, then it is periodic with period Lk for every integer k.

theorem helperForExample_5_1_2_identity_not_periodic_with_positive_period : ¬∃ (L : ℝ), IsPeriodicWithPeriod L fun (x : ℝ) => ↑x

Helper for Example 5.1.2: the identity map x ↦ x (viewed as ℝ → ℂ) is not periodic with any positive period.

theorem helperForExample_5_1_2_constant_one_isPeriodicWithPeriod (L : ℝ) (hL : 0 < L) : IsPeriodicWithPeriod L fun (x : ℝ) => 1

Helper for Example 5.1.2: the constant function 1 is periodic with every positive period.

theorem periodicity_examples_basic : (IsPeriodicWithPeriod (2 * Real.pi) fun (x : ℝ) => ↑(Real.sin x)) ∧ (IsPeriodicWithPeriod (2 * Real.pi) fun (x : ℝ) => ↑(Real.cos x)) ∧ (IsPeriodicWithPeriod (2 * Real.pi) fun (x : ℝ) => Complex.exp (↑x * Complex.I)) ∧ (∀ (k : ℤ), Function.Periodic (fun (x : ℝ) => ↑(Real.sin x)) (2 * Real.pi * ↑k)) ∧ (∀ (k : ℤ), Function.Periodic (fun (x : ℝ) => ↑(Real.cos x)) (2 * Real.pi * ↑k)) ∧ (∀ (k : ℤ), Function.Periodic (fun (x : ℝ) => Complex.exp (↑x * Complex.I)) (2 * Real.pi * ↑k)) ∧ (¬∃ (L : ℝ), IsPeriodicWithPeriod L fun (x : ℝ) => ↑x) ∧ ∀ (L : ℝ), 0 < L → IsPeriodicWithPeriod L fun (x : ℝ) => 1

Example 5.1.2: sin x, cos x, and exp(ix) are 2π-periodic, hence periodic with period 2πk for every integer k; the identity function is not periodic with positive period, while the constant function 1 is L-periodic for every L > 0.

theorem helperForCorollary_5_1_1_intShift_ofPeriodic {L : ℝ} {f : ℝ → ℂ} (hLper : Function.Periodic f L) (x : ℝ) (k : ℤ) : f (x + ↑k * L) = f x

Helper for Corollary 5.1.1: integer multiples of a period are also periods.

theorem helperForCorollary_5_1_1_intShift_ofIsPeriodicWithPeriod {L : ℝ} {f : ℝ → ℂ} (hIsPer : IsPeriodicWithPeriod L f) (x : ℝ) (k : ℤ) : f (x + ↑k * L) = f x

Helper for Corollary 5.1.1: IsPeriodicWithPeriod implies integer-shift invariance by L.

theorem helperForCorollary_5_1_1_unitPeriodSpecialization {f : ℝ → ℂ} (hIsPer1 : IsPeriodicWithPeriod 1 f) (x : ℝ) (k : ℤ) : f (x + ↑k) = f x

Helper for Corollary 5.1.1: specialization to unit period gives k-shift invariance.

theorem periodic_integer_shift_invariance : (∀ {L : ℝ} {f : ℝ → ℂ}, IsPeriodicWithPeriod L f → ∀ (x : ℝ) (k : ℤ), f (x + ↑k * L) = f x) ∧ ∀ {f : ℝ → ℂ}, IsPeriodicWithPeriod 1 f → ∀ (x : ℝ) (k : ℤ), f (x + ↑k) = f x

Corollary 5.1.1 (kL-shift invariance): If f : ℝ → ℂ is L-periodic, then f (x + kL) = f x for all x : ℝ and k : ℤ. In particular, if f is 1-periodic, then f (x + k) = f x for all k : ℤ.

noncomputable def squareWave : ℝ → ℂ

The square-wave function on ℝ, defined by its fractional part: value 1 on the first half of each unit interval and 0 on the second half.

Equations

• squareWave x = if x - ↑⌊x⌋ < 1 / 2 then 1 else 0

theorem zPeriodic_trig_modes_and_squareWave (n : ℤ) : (IsZPeriodic fun (x : ℝ) => ↑(Real.cos (2 * Real.pi * ↑n * x))) ∧ (IsZPeriodic fun (x : ℝ) => ↑(Real.sin (2 * Real.pi * ↑n * x))) ∧ (IsZPeriodic fun (x : ℝ) => Complex.exp (2 * ↑Real.pi * ↑↑n * ↑x * Complex.I)) ∧ IsZPeriodic squareWave

Example 5.1.4: For n : ℤ, the functions x ↦ cos(2πnx), x ↦ sin(2πnx), and x ↦ exp(2πinx) are all ℤ-periodic (equivalently 1-periodic). Another ℤ-periodic function is the square wave.

theorem helperForLemma_5_1_5a_boundedRange_of_continuous_periodic {f : ℝ → ℂ} (hf_cont : Continuous f) (hf_per : IsZPeriodic f) : Bornology.IsBounded (Set.range f)

Helper for Lemma 5.1.5a: a continuous ℤ-periodic function has bounded range.

theorem helperForLemma_5_1_5a_exists_uniform_norm_bound_of_boundedRange {f : ℝ → ℂ} (hbounded : Bornology.IsBounded (Set.range f)) : ∃ (C : ℝ), ∀ (x : ℝ), ‖f x‖ ≤ C

Helper for Lemma 5.1.5a: bounded range gives a uniform bound on values.

theorem isZPeriodic_continuous_bounded {f : ℝ → ℂ} (hf_cont : Continuous f) (hf_per : IsZPeriodic f) : ∃ (C : ℝ), ∀ (x : ℝ), ‖f x‖ ≤ C

Lemma 5.1.5a (Basic properties of C(ℝ/ℤ;ℂ) (a), Boundedness): if f : ℝ → ℂ is continuous and ℤ-periodic, then f is bounded.

theorem helperForLemma_5_1_5b_add_closed {f g : ℝ → ℂ} (hf : Continuous f ∧ IsZPeriodic f) (hg : Continuous g ∧ IsZPeriodic g) : Continuous (f + g) ∧ IsZPeriodic (f + g)

Helper for Lemma 5.1.5b: closure of continuous ℤ-periodic functions under addition.

theorem helperForLemma_5_1_5b_sub_closed {f g : ℝ → ℂ} (hf : Continuous f ∧ IsZPeriodic f) (hg : Continuous g ∧ IsZPeriodic g) : Continuous (f - g) ∧ IsZPeriodic (f - g)

Helper for Lemma 5.1.5b: closure of continuous ℤ-periodic functions under subtraction.

theorem helperForLemma_5_1_5b_mul_closed {f g : ℝ → ℂ} (hf : Continuous f ∧ IsZPeriodic f) (hg : Continuous g ∧ IsZPeriodic g) : Continuous (f * g) ∧ IsZPeriodic (f * g)

Helper for Lemma 5.1.5b: closure of continuous ℤ-periodic functions under multiplication.

theorem helperForLemma_5_1_5b_smul_closed {f : ℝ → ℂ} (c : ℂ) (hf : Continuous f ∧ IsZPeriodic f) : Continuous (c • f) ∧ IsZPeriodic (c • f)

Helper for Lemma 5.1.5b: closure of continuous ℤ-periodic functions under scalar multiplication.

theorem isZPeriodic_continuous_add_sub_mul_smul {f g : ℝ → ℂ} (hf : Continuous f ∧ IsZPeriodic f) (hg : Continuous g ∧ IsZPeriodic g) (c : ℂ) : (Continuous (f + g) ∧ IsZPeriodic (f + g)) ∧ (Continuous (f - g) ∧ IsZPeriodic (f - g)) ∧ (Continuous (f * g) ∧ IsZPeriodic (f * g)) ∧ Continuous (c • f) ∧ IsZPeriodic (c • f)

Lemma 5.1.5b (Basic properties of C(ℝ/ℤ;ℂ) (b), vector space and algebra properties): if f, g : ℝ → ℂ are continuous and ℤ-periodic, then f + g, f - g, and f * g are continuous and ℤ-periodic; and for any scalar c : ℂ, c • f is continuous and ℤ-periodic.

theorem helperForLemma_5_1_5c_continuous_of_uniform_limit {f : ℝ → ℂ} {u : ℕ → ℝ → ℂ} (hlim : TendstoUniformly u f Filter.atTop) (hcont : ∀ (n : ℕ), Continuous (u n)) : Continuous f

Helper for Lemma 5.1.5c: a uniform limit of eventually continuous maps is continuous.

theorem helperForLemma_5_1_5c_eventuallyEq_shifted_sequence {u : ℕ → ℝ → ℂ} (hper : ∀ (n : ℕ), IsZPeriodic (u n)) (x : ℝ) : (fun (n : ℕ) => u n (x + 1)) =ᶠ[Filter.atTop] fun (n : ℕ) => u n x

Helper for Lemma 5.1.5c: periodicity of each approximant gives eventual equality of shifted evaluation sequences.

theorem helperForLemma_5_1_5c_shift_eq_of_uniform_limit {f : ℝ → ℂ} {u : ℕ → ℝ → ℂ} (hlim : TendstoUniformly u f Filter.atTop) (hper : ∀ (n : ℕ), IsZPeriodic (u n)) (x : ℝ) : f (x + 1) = f x

Helper for Lemma 5.1.5c: the uniform limit inherits the unit-shift identity.

theorem helperForLemma_5_1_5c_isZPeriodic_of_uniform_limit {f : ℝ → ℂ} {u : ℕ → ℝ → ℂ} (hlim : TendstoUniformly u f Filter.atTop) (hper : ∀ (n : ℕ), IsZPeriodic (u n)) : IsZPeriodic f

Helper for Lemma 5.1.5c: a uniform limit of ℤ-periodic functions is ℤ-periodic.

theorem isZPeriodic_continuous_of_tendstoUniformly {f : ℝ → ℂ} {u : ℕ → ℝ → ℂ} (hcont : ∀ (n : ℕ), Continuous (u n)) (hper : ∀ (n : ℕ), IsZPeriodic (u n)) (hlim : TendstoUniformly u f Filter.atTop) : Continuous f ∧ IsZPeriodic f

Lemma 5.1.5c (Basic properties of C(ℝ/ℤ;ℂ) (c), closure under uniform limits): if (fₙ) is a sequence of continuous ℤ-periodic functions converging uniformly to f, then f is continuous and ℤ-periodic.