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

Definition 5.2.1 (Inner product): for f, g ∈ C(ℝ/ℤ;ℂ) (modeled as continuous, ℤ-periodic functions ℝ → ℂ), define ⟪f, g⟫ = ∫ x in [0,1], f x * conj (g x) dx.

Equations

• periodicInnerProduct f g = ∫ (x : ℝ) in Set.Icc 0 1, ↑f x * star (↑g x)

def periodicOrthogonal (f g : { h : ℝ → ℂ // Continuous h ∧ Function.Periodic h 1 }) : Prop

Orthogonality for continuous, 1-periodic complex-valued functions.

Equations

• periodicOrthogonal f g = (periodicInnerProduct f g = 0)

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

The L^2 metric on continuous, 1-periodic complex-valued functions.

Equations

• periodicL2Metric f g = √(∫ (x : ℝ) in Set.Icc 0 1, ‖↑f x - ↑g x‖ ^ 2)

noncomputable def periodicOrthogonalityAndL2Metric : ({ h : ℝ → ℂ // Continuous h ∧ Function.Periodic h 1 } → { h : ℝ → ℂ // Continuous h ∧ Function.Periodic h 1 } → Prop) × ({ h : ℝ → ℂ // Continuous h ∧ Function.Periodic h 1 } → { h : ℝ → ℂ // Continuous h ∧ Function.Periodic h 1 } → ℝ)

Definition 5.2.2 (Orthogonality and the L^2 metric): for f, g ∈ C(ℝ/ℤ;ℂ) (modeled as continuous, 1-periodic functions ℝ → ℂ), (i) f and g are orthogonal iff ⟪f, g⟫ = 0; and (ii) d_{L^2}(f,g) = (∫_[0,1] ‖f(x) - g(x)‖^2 dx)^(1/2).

Equations

• periodicOrthogonalityAndL2Metric = (periodicOrthogonal, periodicL2Metric)

def periodicL2ConvergesTo (fSeq : ℕ → { h : ℝ → ℂ // Continuous h ∧ Function.Periodic h 1 }) (f : { h : ℝ → ℂ // Continuous h ∧ Function.Periodic h 1 }) : Prop

Definition 5.2.3 (L^2-convergence): for a sequence (f_n) in C(ℝ/ℤ;ℂ) and f ∈ C(ℝ/ℤ;ℂ), (f_n) converges to f in L^2 when d_{L^2}(f_n, f) → 0 as n → ∞.

Equations

• periodicL2ConvergesTo fSeq f = Filter.Tendsto (fun (n : ℕ) => periodicL2Metric (fSeq n) f) Filter.atTop (nhds 0)

theorem continuous_periodic_constOne : (Continuous fun (x : ℝ) => 1) ∧ Function.Periodic (fun (x : ℝ) => 1) 1

The constant function x ↦ 1 is continuous and 1-periodic.

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

The function x ↦ exp(2πix) is continuous and 1-periodic.

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

The 1-periodic function induced by the constant function x ↦ 1.

Equations

• constOnePeriodicFunction = ⟨fun (x : ℝ) => 1, continuous_periodic_constOne⟩

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

The 1-periodic function induced by x ↦ exp(2πix).

Equations

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

theorem helperForExample_5_2_3_integrand_rewrite (x : ℝ) : 1 * star (Complex.exp (2 * ↑Real.pi * Complex.I * ↑x)) = Complex.exp (-(2 * ↑Real.pi * Complex.I) * ↑x)

Helper for Example 5.2.3: rewrite the integrand as an exponential with negative coefficient.

theorem helperForExample_5_2_3_coeff_ne_zero : -(2 * ↑Real.pi * Complex.I) ≠ 0

Helper for Example 5.2.3: the exponential coefficient is nonzero.

theorem helperForExample_5_2_3_exp_neg_twoPiI_eq_one : Complex.exp (-(2 * ↑Real.pi * Complex.I)) = 1

Helper for Example 5.2.3: the endpoint value exp(-2πi) equals 1.

theorem helperForExample_5_2_3_interval_integral_exp_neg_twoPiI : ∫ (x : ℝ) in Set.Icc 0 1, Complex.exp (-(2 * ↑Real.pi * Complex.I) * ↑x) = 0

Helper for Example 5.2.3: the relevant exponential integral on [0,1] vanishes.

theorem periodicInnerProduct_constOne_expTwoPiI : periodicInnerProduct constOnePeriodicFunction expTwoPiIPeriodicFunction = 0

Example 5.2.3: let f(x) = 1 and g(x) = exp(2πix). Then ⟪f, g⟫ = 0.

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

The L^2 norm on continuous, 1-periodic complex-valued functions induced by the inner product ⟪f, g⟫ = ∫_[0,1] f \overline{g}.

Equations

• periodicL2Norm f = √(periodicInnerProduct f f).re

theorem helperForExample_5_2_6_pointwise_selfInner_integrand_eq_one (x : ℝ) : Complex.exp (2 * ↑Real.pi * Complex.I * ↑x) * star (Complex.exp (2 * ↑Real.pi * Complex.I * ↑x)) = 1

Helper for Example 5.2.6: the self-inner-product integrand is identically 1.

theorem helperForExample_5_2_6_innerProduct_self_eq_one : periodicInnerProduct expTwoPiIPeriodicFunction expTwoPiIPeriodicFunction = 1

Helper for Example 5.2.6: the self-inner product of exp(2πix) equals 1.

theorem helperForExample_5_2_6_realpart_selfInner_eq_one : (periodicInnerProduct expTwoPiIPeriodicFunction expTwoPiIPeriodicFunction).re = 1

Helper for Example 5.2.6: the real part of the self-inner product is 1.

theorem expTwoPiIPeriodicFunction_l2Norm_eq_one : periodicL2Norm expTwoPiIPeriodicFunction = 1

Example 5.2.6: for f(x) = exp(2πix), one has ‖f‖_2 = 1.

theorem helperForLemma_5_2_7a_re_eq_intervalIntegral_normSq (f : { h : ℝ → ℂ // Continuous h ∧ Function.Periodic h 1 }) : (periodicInnerProduct f f).re = ∫ (x : ℝ) in 0..1, Complex.normSq (↑f x)

Helper for Lemma 5.2.7a: rewrite Re ⟪f,f⟫ as an interval integral of normSq.

theorem helperForLemma_5_2_7a_exists_nonzero_in_unit_interval (f : { h : ℝ → ℂ // Continuous h ∧ Function.Periodic h 1 }) (hne : ↑f ≠ 0) : ∃ x ∈ Set.Icc 0 1, ↑f x ≠ 0

Helper for Lemma 5.2.7a: a nonzero periodic function is nonzero at some point of the unit interval.

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

Helper for Lemma 5.2.7a: if a periodic function is nonzero, then Re ⟪f,f⟫ is strictly positive.

theorem helperForLemma_5_2_7a_re_eq_zero_iff_fun_zero (f : { h : ℝ → ℂ // Continuous h ∧ Function.Periodic h 1 }) : (periodicInnerProduct f f).re = 0 ↔ ↑f = 0

Helper for Lemma 5.2.7a: vanishing real part of the self-inner product is equivalent to the function being zero.

theorem helperForLemma_5_2_7a_l2_eq_zero_iff_re_eq_zero (f : { h : ℝ → ℂ // Continuous h ∧ Function.Periodic h 1 }) : periodicL2Norm f = 0 ↔ (periodicInnerProduct f f).re = 0

Helper for Lemma 5.2.7a: ‖f‖_2 = 0 is equivalent to vanishing real part of the self-inner product.

theorem periodicL2Norm_eq_zero_iff (f : { h : ℝ → ℂ // Continuous h ∧ Function.Periodic h 1 }) : periodicL2Norm f = 0 ↔ ↑f = 0

Lemma 5.2.7a (Basic properties of ‖·‖_2 (a), non-degeneracy): for f ∈ C(ℝ/ℤ; ℂ) (modeled as a continuous, 1-periodic function ℝ → ℂ), ‖f‖_2 = 0 iff f is the zero function.

theorem helperForLemma_5_2_7b_memLp_two_restrict_Icc (u : { h : ℝ → ℂ // Continuous h ∧ Function.Periodic h 1 }) : MeasureTheory.MemLp (fun (x : ℝ) => ↑u x) 2 (MeasureTheory.volume.restrict (Set.Icc 0 1))

Helper for Lemma 5.2.7b: continuity on [0,1] gives L² membership on the restricted measure.

theorem helperForLemma_5_2_7b_pointwise_norm_mul_star (f g : { h : ℝ → ℂ // Continuous h ∧ Function.Periodic h 1 }) (x : ℝ) : ‖↑f x * star (↑g x)‖ = ‖↑f x‖ * ‖↑g x‖

Helper for Lemma 5.2.7b: pointwise norm of the inner-product integrand factors.

theorem helperForLemma_5_2_7b_holder_norm_on_Icc (f g : { h : ℝ → ℂ // Continuous h ∧ Function.Periodic h 1 }) : ∫ (x : ℝ) in Set.Icc 0 1, ‖↑f x‖ * ‖↑g x‖ ≤ (∫ (x : ℝ) in Set.Icc 0 1, ‖↑f x‖ ^ 2) ^ (1 / 2) * (∫ (x : ℝ) in Set.Icc 0 1, ‖↑g x‖ ^ 2) ^ (1 / 2)

Helper for Lemma 5.2.7b: Hölder with p = q = 2 on [0,1] for norm-products.

theorem helperForLemma_5_2_7b_rhs_factor_eq_periodicL2Norm (u : { h : ℝ → ℂ // Continuous h ∧ Function.Periodic h 1 }) : (∫ (x : ℝ) in Set.Icc 0 1, ‖↑u x‖ ^ 2) ^ (1 / 2) = periodicL2Norm u

Helper for Lemma 5.2.7b: each Hölder L² factor is exactly periodicL2Norm.

theorem periodicInnerProduct_abs_le_periodicL2Norm_mul (f g : { h : ℝ → ℂ // Continuous h ∧ Function.Periodic h 1 }) : ‖periodicInnerProduct f g‖ ≤ periodicL2Norm f * periodicL2Norm g

Lemma 5.2.7b (Basic properties of ‖·‖_2 (b), Cauchy--Schwarz): for f, g ∈ C(ℝ/ℤ; ℂ) (modeled as continuous, 1-periodic functions ℝ → ℂ), |⟪f, g⟫| ≤ ‖f‖_2 ‖g‖_2.

theorem helperForLemma_5_2_5a_pointwise_swap_to_conj (f g : { h : ℝ → ℂ // Continuous h ∧ Function.Periodic h 1 }) (x : ℝ) : ↑g x * star (↑f x) = star (↑f x * star (↑g x))

Helper for Lemma 5.2.5a: swapping the two arguments in the integrand gives its complex conjugate pointwise.

theorem helperForLemma_5_2_5a_conj_of_setIntegral_Icc (f g : { h : ℝ → ℂ // Continuous h ∧ Function.Periodic h 1 }) : ∫ (x : ℝ) in Set.Icc 0 1, star (↑f x * star (↑g x)) = star (∫ (x : ℝ) in Set.Icc 0 1, ↑f x * star (↑g x))

Helper for Lemma 5.2.5a: conjugation commutes with integration over [0,1].

theorem periodicInnerProduct_hermitian (f g : { h : ℝ → ℂ // Continuous h ∧ Function.Periodic h 1 }) : periodicInnerProduct g f = star (periodicInnerProduct f g)

Lemma 5.2.5a (Properties of the inner product (a), Hermitian): if f, g ∈ C(ℝ/ℤ; ℂ) (modeled as continuous, 1-periodic functions ℝ → ℂ), then ⟪g, f⟫ = \overline{⟪f, g⟫}.

theorem helperForLemma_5_2_5b_self_eq_setIntegral_normSq (f : { h : ℝ → ℂ // Continuous h ∧ Function.Periodic h 1 }) : periodicInnerProduct f f = ∫ (x : ℝ) in Set.Icc 0 1, ↑(Complex.normSq (↑f x))

Helper for Lemma 5.2.5b: rewrite ⟪f,f⟫ as the integral of normSq.

theorem helperForLemma_5_2_5b_re_eq_intervalIntegral_normSq (f : { h : ℝ → ℂ // Continuous h ∧ Function.Periodic h 1 }) : (periodicInnerProduct f f).re = ∫ (x : ℝ) in 0..1, Complex.normSq (↑f x)

Helper for Lemma 5.2.5b: the real part of ⟪f,f⟫ is an interval integral of normSq.

theorem helperForLemma_5_2_5b_exists_nonzero_in_unit_interval (f : { h : ℝ → ℂ // Continuous h ∧ Function.Periodic h 1 }) (hne : ↑f ≠ 0) : ∃ x ∈ Set.Icc 0 1, ↑f x ≠ 0

Helper for Lemma 5.2.5b: a nonzero periodic function is nonzero at some point in one fundamental domain.

theorem helperForLemma_5_2_5b_re_pos_of_exists_nonzero_in_unit_interval (f : { h : ℝ → ℂ // Continuous h ∧ Function.Periodic h 1 }) (hExists : ∃ x ∈ Set.Icc 0 1, ↑f x ≠ 0) : 0 < (periodicInnerProduct f f).re

Helper for Lemma 5.2.5b: a nonzero value on [0,1] forces strict positivity of Re ⟪f,f⟫.

theorem helperForLemma_5_2_5b_self_im_eq_zero (f : { h : ℝ → ℂ // Continuous h ∧ Function.Periodic h 1 }) : (periodicInnerProduct f f).im = 0

Helper for Lemma 5.2.5b: the imaginary part of ⟪f,f⟫ vanishes.

theorem periodicInnerProduct_positivity (f : { h : ℝ → ℂ // Continuous h ∧ Function.Periodic h 1 }) : 0 ≤ (periodicInnerProduct f f).re ∧ (periodicInnerProduct f f).im = 0 ∧ (periodicInnerProduct f f = 0 ↔ ↑f = 0)

Lemma 5.2.5b (Properties of the inner product (b), Positivity): if f ∈ C(ℝ/ℤ; ℂ) (modeled as a continuous, 1-periodic function ℝ → ℂ), then ⟪f, f⟫ is real and nonnegative, and ⟪f, f⟫ = 0 iff f is the zero function.

theorem continuous_periodic_add (f g : { h : ℝ → ℂ // Continuous h ∧ Function.Periodic h 1 }) : Continuous (↑f + ↑g) ∧ Function.Periodic (↑f + ↑g) 1

The sum of two continuous, 1-periodic complex-valued functions is continuous and 1-periodic.

theorem continuous_periodic_smul (c : ℂ) (f : { h : ℝ → ℂ // Continuous h ∧ Function.Periodic h 1 }) : Continuous (c • ↑f) ∧ Function.Periodic (c • ↑f) 1

A scalar multiple of a continuous, 1-periodic complex-valued function is continuous and 1-periodic.

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

The pointwise sum in C(ℝ/ℤ; ℂ) modeled as continuous, 1-periodic functions ℝ → ℂ.

Equations

• addPeriodicFunction f g = ⟨↑f + ↑g, ⋯⟩

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

Scalar multiplication in C(ℝ/ℤ; ℂ) modeled as continuous, 1-periodic functions ℝ → ℂ.

Equations

• smulPeriodicFunction c f = ⟨c • ↑f, ⋯⟩

theorem helperForLemma_5_2_7c_pointwise_add_self_integrand_expand (f g : { h : ℝ → ℂ // Continuous h ∧ Function.Periodic h 1 }) (x : ℝ) : (↑f + ↑g) x * star ((↑f + ↑g) x) = ↑f x * star (↑f x) + ↑f x * star (↑g x) + ↑g x * star (↑f x) + ↑g x * star (↑g x)

Helper for Lemma 5.2.7c: pointwise expansion of (f + g) * conj (f + g).

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

Helper for Lemma 5.2.7c: expansion of ⟪f + g, f + g⟫ into diagonal and cross terms.

theorem helperForLemma_5_2_7c_re_self_eq_sq_l2Norm (u : { h : ℝ → ℂ // Continuous h ∧ Function.Periodic h 1 }) : (periodicInnerProduct u u).re = periodicL2Norm u ^ 2

Helper for Lemma 5.2.7c: diagonal terms satisfy Re ⟪u, u⟫ = ‖u‖_2^2.

theorem helperForLemma_5_2_7c_cross_re_sum_le_two_mul (f g : { h : ℝ → ℂ // Continuous h ∧ Function.Periodic h 1 }) : (periodicInnerProduct f g).re + (periodicInnerProduct g f).re ≤ 2 * (periodicL2Norm f * periodicL2Norm g)

Helper for Lemma 5.2.7c: the real parts of the cross terms are bounded by 2 ‖f‖_2 ‖g‖_2.

theorem helperForLemma_5_2_7c_re_addSelf_le_sq_sum (f g : { h : ℝ → ℂ // Continuous h ∧ Function.Periodic h 1 }) : (periodicInnerProduct (addPeriodicFunction f g) (addPeriodicFunction f g)).re ≤ (periodicL2Norm f + periodicL2Norm g) ^ 2

Helper for Lemma 5.2.7c: the real part of ⟪f+g, f+g⟫ is bounded by (‖f‖_2 + ‖g‖_2)^2.

theorem periodicL2Norm_add_le (f g : { h : ℝ → ℂ // Continuous h ∧ Function.Periodic h 1 }) : periodicL2Norm (addPeriodicFunction f g) ≤ periodicL2Norm f + periodicL2Norm g

Lemma 5.2.7c (Basic properties of ‖·‖_2 (c), triangle inequality): for f, g ∈ C(ℝ/ℤ; ℂ) (modeled as continuous, 1-periodic functions ℝ → ℂ), ‖f + g‖_2 ≤ ‖f‖_2 + ‖g‖_2.

theorem helperForLemma_5_2_7d_swap_inner_eq_zero_of_orthogonal (f g : { h : ℝ → ℂ // Continuous h ∧ Function.Periodic h 1 }) (hfg : periodicInnerProduct f g = 0) : periodicInnerProduct g f = 0

Helper for Lemma 5.2.7d: orthogonality is preserved when swapping arguments by Hermitian symmetry.

theorem helperForLemma_5_2_7d_cross_re_sum_eq_zero_of_orthogonal (f g : { h : ℝ → ℂ // Continuous h ∧ Function.Periodic h 1 }) (hfg : periodicInnerProduct f g = 0) : (periodicInnerProduct f g).re + (periodicInnerProduct g f).re = 0

Helper for Lemma 5.2.7d: the sum of the real parts of the two cross terms vanishes under orthogonality.

theorem helperForLemma_5_2_7d_re_addSelf_eq_sq_sum_of_orthogonal (f g : { h : ℝ → ℂ // Continuous h ∧ Function.Periodic h 1 }) (hfg : periodicInnerProduct f g = 0) : (periodicInnerProduct (addPeriodicFunction f g) (addPeriodicFunction f g)).re = periodicL2Norm f ^ 2 + periodicL2Norm g ^ 2

Helper for Lemma 5.2.7d: the real part of ⟪f+g, f+g⟫ equals the sum of the squared L^2 norms when ⟪f, g⟫ = 0.

theorem periodicL2Norm_pythagoras (f g : { h : ℝ → ℂ // Continuous h ∧ Function.Periodic h 1 }) (hfg : periodicInnerProduct f g = 0) : periodicL2Norm (addPeriodicFunction f g) ^ 2 = periodicL2Norm f ^ 2 + periodicL2Norm g ^ 2

Lemma 5.2.7d (Basic properties of ‖·‖_2 (d), Pythagoras): for f, g ∈ C(ℝ/ℤ; ℂ) (modeled as continuous, 1-periodic functions ℝ → ℂ), if ⟪f, g⟫ = 0, then ‖f + g‖_2^2 = ‖f‖_2^2 + ‖g‖_2^2.

theorem helperForLemma_5_2_7e_pointwise_normSq_smul (c : ℂ) (f : { h : ℝ → ℂ // Continuous h ∧ Function.Periodic h 1 }) (x : ℝ) : Complex.normSq (↑(smulPeriodicFunction c f) x) = ‖c‖ ^ 2 * Complex.normSq (↑f x)

Helper for Lemma 5.2.7e: pointwise scaling of normSq under scalar multiplication.

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

Helper for Lemma 5.2.7e: nonnegativity of the real part of ⟪f,f⟫.

theorem helperForLemma_5_2_7e_re_inner_self_smul (c : ℂ) (f : { h : ℝ → ℂ // Continuous h ∧ Function.Periodic h 1 }) : (periodicInnerProduct (smulPeriodicFunction c f) (smulPeriodicFunction c f)).re = ‖c‖ ^ 2 * (periodicInnerProduct f f).re

Helper for Lemma 5.2.7e: the real part of ⟪cf,cf⟫ scales by ‖c‖².

theorem helperForLemma_5_2_7e_sqrt_mul_sq_norm (c : ℂ) {t : ℝ} (ht : 0 ≤ t) : √(‖c‖ ^ 2 * t) = ‖c‖ * √t

Helper for Lemma 5.2.7e: pull ‖c‖² out of a square root.

theorem periodicL2Norm_smul (c : ℂ) (f : { h : ℝ → ℂ // Continuous h ∧ Function.Periodic h 1 }) : periodicL2Norm (smulPeriodicFunction c f) = ‖c‖ * periodicL2Norm f

Lemma 5.2.7e (Basic properties of ‖·‖_2 (e), homogeneity): for f ∈ C(ℝ/ℤ; ℂ) (modeled as a continuous, 1-periodic function ℝ → ℂ) and c ∈ ℂ, ‖cf‖_2 = ‖c‖ ‖f‖_2.

theorem helperForLemma_5_2_5c_integrableOn_mul_star (u v : { h : ℝ → ℂ // Continuous h ∧ Function.Periodic h 1 }) : MeasureTheory.IntegrableOn (fun (x : ℝ) => ↑u x * star (↑v x)) (Set.Icc 0 1) MeasureTheory.volume

Helper for Lemma 5.2.5c: the product integrand defining ⟪u, v⟫ is integrable on [0,1].

theorem helperForLemma_5_2_5c_addIntegrand_expand (f g h : { h : ℝ → ℂ // Continuous h ∧ Function.Periodic h 1 }) (x : ℝ) : (↑f + ↑g) x * star (↑h x) = ↑f x * star (↑h x) + ↑g x * star (↑h x)

Helper for Lemma 5.2.5c: expand the additive integrand pointwise.

theorem helperForLemma_5_2_5c_smulIntegrand_factor (c : ℂ) (f g : { h : ℝ → ℂ // Continuous h ∧ Function.Periodic h 1 }) (x : ℝ) : (c • ↑f) x * star (↑g x) = c * (↑f x * star (↑g x))

Helper for Lemma 5.2.5c: factor a scalar from the first-slot integrand.