theorem periodicInnerProduct_linearity_first (f g h : { h : ℝ → ℂ // Continuous h ∧ Function.Periodic h 1 }) (c : ℂ) : periodicInnerProduct (addPeriodicFunction f g) h = periodicInnerProduct f h + periodicInnerProduct g h ∧ periodicInnerProduct (smulPeriodicFunction c f) g = c * periodicInnerProduct f g

Lemma 5.2.5c (Properties of the inner product (c), linearity in the first variable): for f, g, h ∈ C(ℝ/ℤ; ℂ) and c ∈ ℂ, ⟪f + g, h⟫ = ⟪f, h⟫ + ⟪g, h⟫ and ⟪cf, g⟫ = c ⟪f, g⟫.

theorem helperForLemma_5_2_5d_star_swap (u v : { h : ℝ → ℂ // Continuous h ∧ Function.Periodic h 1 }) : star (periodicInnerProduct u v) = periodicInnerProduct v u

Helper for Lemma 5.2.5d: taking the star of periodicInnerProduct u v swaps the arguments.

theorem periodicInnerProduct_antilinearity_second (f g h : { h : ℝ → ℂ // Continuous h ∧ Function.Periodic h 1 }) (c : ℂ) : periodicInnerProduct f (addPeriodicFunction g h) = periodicInnerProduct f g + periodicInnerProduct f h ∧ periodicInnerProduct f (smulPeriodicFunction c g) = star c * periodicInnerProduct f g

Lemma 5.2.5d (Properties of the inner product (d), antilinearity in the second variable): for f, g, h ∈ C(ℝ/ℤ; ℂ) and c ∈ ℂ, ⟪f, g + h⟫ = ⟪f, g⟫ + ⟪f, h⟫ and ⟪f, cg⟫ = \overline{c} ⟪f, g⟫.

noncomputable def periodicLInftyNorm (f : { h : ℝ → ℂ // Continuous h ∧ Function.Periodic h 1 }) : ℝ

The L^∞ norm on continuous, 1-periodic complex-valued functions, taken as the supremum of ‖f(x)‖ on [0,1].

Equations

• periodicLInftyNorm f = sSup (Set.range fun (x : ↑(Set.Icc 0 1)) => ‖↑f ↑x‖)

theorem helperForExercise_5_2_3_zero_mem_Icc : 0 ∈ Set.Icc 0 1

Helper for Exercise 5.2.3: 0 belongs to the fundamental interval [0,1].

theorem helperForExercise_5_2_3_lInftyRange_bddAbove (f : { h : ℝ → ℂ // Continuous h ∧ Function.Periodic h 1 }) : BddAbove (Set.range fun (x : ↑(Set.Icc 0 1)) => ‖↑f ↑x‖)

Helper for Exercise 5.2.3: the L^∞-range set is bounded above.

theorem helperForExercise_5_2_3_lInftyRange_nonempty (f : { h : ℝ → ℂ // Continuous h ∧ Function.Periodic h 1 }) : (Set.range fun (x : ↑(Set.Icc 0 1)) => ‖↑f ↑x‖).Nonempty

Helper for Exercise 5.2.3: the L^∞-range set is nonempty.

theorem helperForExercise_5_2_3_lInfty_nonneg (f : { h : ℝ → ℂ // Continuous h ∧ Function.Periodic h 1 }) : 0 ≤ periodicLInftyNorm f

Helper for Exercise 5.2.3: the periodic L^∞ norm is nonnegative.

theorem helperForExercise_5_2_3_normSq_le_lInftySq (f : { h : ℝ → ℂ // Continuous h ∧ Function.Periodic h 1 }) (x : ℝ) (hx : x ∈ Set.Icc 0 1) : Complex.normSq (↑f x) ≤ periodicLInftyNorm f ^ 2

Helper for Exercise 5.2.3: pointwise normSq is bounded by ‖f‖^2_{L^∞} on [0,1].

theorem helperForExercise_5_2_3_nonzero_implies_l2_pos (f : { h : ℝ → ℂ // Continuous h ∧ Function.Periodic h 1 }) (hne : ↑f ≠ 0) : 0 < periodicL2Norm f

Helper for Exercise 5.2.3: a nonzero periodic continuous function has strictly positive L^2 norm.

theorem helperForExercise_5_2_3_l2_le_lInfty (f : { h : ℝ → ℂ // Continuous h ∧ Function.Periodic h 1 }) : periodicL2Norm f ≤ periodicLInftyNorm f

Helper for Exercise 5.2.3: always ‖f‖_2 ≤ ‖f‖_{L^∞}.

theorem helperForExercise_5_2_3_complexNorm_ofReal (A : ℝ) : ‖↑A‖ = |A|

Helper for Exercise 5.2.3: for real scalars, ‖A‖ as a complex norm is |A|.

theorem helperForExercise_5_2_3_lInfty_smul_exp (c : ℂ) : periodicLInftyNorm (smulPeriodicFunction c expTwoPiIPeriodicFunction) = ‖c‖

Helper for Exercise 5.2.3: scaling exp(2πix) by c gives L^∞ norm ‖c‖.

theorem helperForExercise_5_2_3_exists_exact_norms_on_diagonal (A : ℝ) (hA : 0 < A) : ∃ (f : { h : ℝ → ℂ // Continuous h ∧ Function.Periodic h 1 }), ↑f ≠ 0 ∧ periodicL2Norm f = A ∧ periodicLInftyNorm f = A

Helper for Exercise 5.2.3: diagonal converse case A = B.

theorem helperForExercise_5_2_3_choose_parameters_for_ratio (r : ℝ) (hr0 : 0 < r) (hr1 : r < 1) : ∃ (N : ℕ), 1 ≤ N ∧ ∃ (t : ℝ), 0 ≤ t ∧ t ≤ 1 ∧ t ^ 2 + (1 - t) ^ 2 / ↑N = r

Helper for Exercise 5.2.3: choose N,t with t^2 + (1 - t)^2 / N = r for any 0 < r < 1.

theorem continuous_periodic_expMode (n : ℤ) : (Continuous fun (x : ℝ) => Complex.exp (↑n * (2 * ↑Real.pi * Complex.I) * ↑x)) ∧ Function.Periodic (fun (x : ℝ) => Complex.exp (↑n * (2 * ↑Real.pi * Complex.I) * ↑x)) 1

Helper for Exercise 5.2.3: the Fourier mode x ↦ exp(2πinx) is continuous and 1-periodic for every integer frequency n.

noncomputable def expModePeriodicFunction (n : ℤ) : { h : ℝ → ℂ // Continuous h ∧ Function.Periodic h 1 }

Helper for Exercise 5.2.3: integer Fourier modes as periodic continuous functions.

Equations

• expModePeriodicFunction n = ⟨fun (x : ℝ) => Complex.exp (↑n * (2 * ↑Real.pi * Complex.I) * ↑x), ⋯⟩

theorem helperForExercise_5_2_3_expMode_norm_eq_one (n : ℤ) (x : ℝ) : ‖↑(expModePeriodicFunction n) x‖ = 1

Helper for Exercise 5.2.3: every Fourier mode has unit pointwise magnitude.

theorem helperForExercise_5_2_3_expMode_inner (m n : ℤ) : periodicInnerProduct (expModePeriodicFunction m) (expModePeriodicFunction n) = if m = n then 1 else 0

Helper for Exercise 5.2.3: Fourier modes have orthonormal inner products on [0,1].

theorem helperForExercise_5_2_3_expMode_l2Sq_eq_one (n : ℤ) : periodicL2Norm (expModePeriodicFunction n) ^ 2 = 1

Helper for Exercise 5.2.3: every Fourier mode has L^2 norm squared equal to 1.

noncomputable def sumExpModes : ℕ → { h : ℝ → ℂ // Continuous h ∧ Function.Periodic h 1 }

Helper for Exercise 5.2.3: partial sums of positive Fourier modes.

Equations

• sumExpModes 0 = smulPeriodicFunction 0 (expModePeriodicFunction 0)
• sumExpModes N.succ = addPeriodicFunction (sumExpModes N) (expModePeriodicFunction (↑N + 1))

theorem helperForExercise_5_2_3_sumExpModes_inner_of_lt (N k : ℕ) (hk : N < k) : periodicInnerProduct (sumExpModes N) (expModePeriodicFunction ↑k) = 0

Helper for Exercise 5.2.3: sumExpModes N is orthogonal to any higher mode.

theorem helperForExercise_5_2_3_sumExpModes_inner_next (N : ℕ) : periodicInnerProduct (sumExpModes N) (expModePeriodicFunction (↑N + 1)) = 0

Helper for Exercise 5.2.3: sumExpModes N is orthogonal to the next mode.

theorem helperForExercise_5_2_3_constMode_inner_sumExpModes (N : ℕ) : periodicInnerProduct (expModePeriodicFunction 0) (sumExpModes N) = 0

Helper for Exercise 5.2.3: constant mode is orthogonal to sumExpModes N.

theorem helperForExercise_5_2_3_sumExpModes_l2Sq (N : ℕ) : periodicL2Norm (sumExpModes N) ^ 2 = ↑N

Helper for Exercise 5.2.3: sumExpModes N has exact L^2 norm square N.

theorem helperForExercise_5_2_3_sumExpModes_value_zero (N : ℕ) : ↑(sumExpModes N) 0 = ↑N

Helper for Exercise 5.2.3: value of sumExpModes N at 0 is exactly N.

theorem helperForExercise_5_2_3_sumExpModes_norm_le (N : ℕ) (x : ℝ) : ‖↑(sumExpModes N) x‖ ≤ ↑N

Helper for Exercise 5.2.3: pointwise bound for partial Fourier sums.

noncomputable def averageExpModesPeriodicFunction (N : ℕ) : { h : ℝ → ℂ // Continuous h ∧ Function.Periodic h 1 }

Helper for Exercise 5.2.3: normalized average of the first N positive Fourier modes.

Equations

• averageExpModesPeriodicFunction N = smulPeriodicFunction (1 / ↑↑N) (sumExpModes N)

theorem helperForExercise_5_2_3_average_modes_profile (N : ℕ) (hN : 1 ≤ N) : ∃ (g : { h : ℝ → ℂ // Continuous h ∧ Function.Periodic h 1 }), periodicInnerProduct (expModePeriodicFunction 0) g = 0 ∧ periodicL2Norm g ^ 2 = 1 / ↑N ∧ periodicLInftyNorm g = 1 ∧ ↑g 0 = 1

Helper for Exercise 5.2.3: exact profile of the normalized mode average, including orthogonality to the constant mode, exact L^2 square, exact L^∞, and value at 0.

theorem helperForExercise_5_2_3_blend_profile (N : ℕ) (hN : 1 ≤ N) (t : ℝ) (ht0 : 0 ≤ t) (ht1 : t ≤ 1) : ∃ (u : { h : ℝ → ℂ // Continuous h ∧ Function.Periodic h 1 }), periodicLInftyNorm u = 1 ∧ periodicL2Norm u ^ 2 = t ^ 2 + (1 - t) ^ 2 / ↑N ∧ ↑u 0 = 1

Helper for Exercise 5.2.3: exact blended profile with prescribed t^2 + (1 - t)^2 / N, unit L^∞, and value 1 at zero.

theorem helperForExercise_5_2_3_exists_exact_norms_strict (A B : ℝ) (hA : 0 < A) (hAB : A < B) : ∃ (f : { h : ℝ → ℂ // Continuous h ∧ Function.Periodic h 1 }), ↑f ≠ 0 ∧ periodicL2Norm f = A ∧ periodicLInftyNorm f = B

Helper for Exercise 5.2.3: strict converse case A < B.

theorem exercise_5_2_3 : (∀ (f : { h : ℝ → ℂ // Continuous h ∧ Function.Periodic h 1 }), ↑f ≠ 0 → 0 < periodicL2Norm f ∧ periodicL2Norm f ≤ periodicLInftyNorm f) ∧ ∀ (A B : ℝ), 0 < A → A ≤ B → ∃ (f : { h : ℝ → ℂ // Continuous h ∧ Function.Periodic h 1 }), ↑f ≠ 0 ∧ periodicL2Norm f = A ∧ periodicLInftyNorm f = B

Exercise 5.2.3: if f ∈ C(ℝ/ℤ; ℂ) is non-zero, then 0 < ‖f‖_2 ≤ ‖f‖_{L^∞}; conversely, for real numbers 0 < A ≤ B, there exists a non-zero f ∈ C(ℝ/ℤ; ℂ) with ‖f‖_2 = A and ‖f‖_{L^∞} = B.