LemmaStatement: AI-adaptedProof: AI-adaptedPipeline-generatedprecheck passjudge pass (gpt-6.1-sol)

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Period averages of products of real parts of complex exponentials

Statement

Let $ω > 0$ and $T : = 2 π / ω > 0$ .

Scalar form. Let $a, d \in C$ . Then

$\frac{1}{T} \int_{0}^{T} Re (a e^{- i ω t}) Re (d e^{- i ω t}) d t = \frac{1}{2} Re (a \overline{d}) .$

Vector forms. Let $a, d \in C^{3}$ , write the same symbols for the componentwise complex-bilinear extensions of the Euclidean inner product and of the cross product of The Euclidean inner product $⟨ x, y ⟩ = \sum_{k < n} x_{k} y_{k}$ on $R^{n}$ and The cross product in $R^{3}$ to $C^{3}$ , and let $Re$ act componentwise. In coordinate formulas, $ϵ_{i j k}$ is $+ 1$ for even permutations of $(1, 2, 3)$ , $- 1$ for odd permutations and zero for repeated indices; all displayed repeated-index sums run from 1 to 3. Then

$\frac{1}{T} \int_{0}^{T} ⟨ Re (a e^{- i ω t}), Re (d e^{- i ω t}) ⟩ d t = \frac{1}{2} Re (⟨ a, \overline{d} ⟩), \frac{1}{T} \int_{0}^{T} Re (a e^{- i ω t}) \times Re (d e^{- i ω t}) d t = \frac{1}{2} Re (a \times \overline{d}),$

the integrals of the real vector-valued integrands being componentwise. The real-valued functions $Re (a e^{- i ω t})$ are the time-dependent factors of the plane-wave fields of Complex plane-wave fields: real parts of complex exponentials at a fixed position, with the phase absorbed into $a$ and $d$ ; no electromagnetic interpretation is asserted. Real quadratic expressions may not be replaced by complex quadratic expressions without conjugation: the average is not $\frac{1}{2} Re (a d)$ in general. For $a = d = 1 + i$ the proved average is $\frac{1}{2} ∣ 1 + i ∣^{2} = 1$ , whereas $\frac{1}{2} Re ((1 + i)^{2}) = 0$ .

Facts & Assumptions

Given: A real $ω > 0$ , $T = 2 π / ω$ ; complex numbers $a, d \in C$ and, in the vector forms, $a, d \in C^{3}$ with the componentwise conventions of the Statement.

[F1]

Complex exponential and its calculus: $\exp z = \sum_{n \geq 0} z^{n} / n!$ has $\exp 0 = 1$ , is entire with $\exp^{'} = \exp$ , and satisfies the addition law $\exp (z + w) = \exp z \exp w$ ; for real $x, y$ one has $\exp (x + i y) = e^{x} (\cos y + i \sin y)$ and $∣ \exp (x + i y) ∣ = e^{x}$ , so $∣ e^{i θ} ∣ = 1$ for real $θ$ (The complex exponential by its power series, The complex exponential is entire and its complex derivative is itself, $\exp (z + w) = \exp z \exp w$ , and the complex exponential extends the real exponential, $\exp (x + i y) = e^{x} (\cos y + i \sin y)$ , $∣ \exp (x + i y) ∣ = e^{x}$ , and $e^{i π} + 1 = 0$ ).

[F2]

Coordinates, conjugation and modulus: $z = a + b i$ has $Re z = a$ , $Im z = b$ , $\overline{z} = a - b i$ (Real and imaginary parts, complex conjugation, and modulus); conjugation is a real-field automorphism with $\overline{z + w} = \overline{z} + \overline{w}$ , $\overline{z w} = \overline{z} \overline{w}$ , $\overline{\overline{z}} = z$ , and $z \overline{z} = ∣ z ∣^{2}$ (Conjugation is an involutive real-field automorphism, $z \overline{z} = ∣ z ∣^{2}$ , and modulus is definite, multiplicative, and subadditive); in particular $\overline{i} = - i$ , $\overline{r} = r$ for real $r$ , and the field axioms of $C = R [x] / (x^{2} + 1)$ is a field, every element is uniquely $a + b i$ , and every nonzero element has inverse $(a - b i) / (a^{2} + b^{2})$ hold. Consequently, for real $θ$ , $e^{i θ} e^{- i θ} = e^{0} = 1$ by [F1] and $∣ e^{i θ} ∣ = 1$ by [F1], so $\overline{e^{i θ}} = \overline{e^{i θ}} \cdot e^{i θ} e^{- i θ} = ∣ e^{i θ} ∣^{2} e^{- i θ} = e^{- i θ}$ ; replacing $θ$ by $- θ$ gives $\overline{e^{- i θ}} = e^{i θ}$ .

[F3]

Kernel of the exponential: $\ker (\exp) = 2 π i Z$ , so $e^{2 π i n} = 1$ for every $n \in Z$ ; in particular $e^{- 4 π i} = 1$ ( $\ker (\exp) = 2 π i Z$ , and $\exp z = \exp w$ exactly when $z - w \in 2 π i Z$ ).

[F4]

Real and imaginary parts of differentiable paths: identifying $C$ with $R^{2}$ , the maps $Re, Im : C \to R$ are real-linear, so for a differentiable path $z : J \to C$ on an interval $J$ the functions $t \mapsto Re z (t)$ and $t \mapsto Im z (t)$ are differentiable with derivatives $Re z^{'} (t)$ and $Im z^{'} (t)$ by the chain rule (The chain rule for total derivatives: $D (g \circ f) (a) = D g (f (a)) \circ D f (a)$ , Sums, scalar multiples, products and quotients: $(f + g)^{'} (c) = f^{'} (c) + g^{'} (c)$ , $(α f)^{'} (c) = α f^{'} (c)$ , $(f g)^{'} (c) = f^{'} (c) g (c) + f (c) g^{'} (c)$ , and $(f / g)^{'} (c) = (f^{'} (c) g (c) - f (c) g^{'} (c)) / g (c)^{2}$ when $g (c) \neq 0$ ); in particular $\frac{d}{d t} e^{- 2 i ω t} = - 2 i ω e^{- 2 i ω t}$ , since $t \mapsto - 2 i ω t$ is real-linear with derivative $- 2 i ω$ and $\exp^{'} = \exp$ by [F1].

[F5]

Fundamental theorem of calculus: if $G : [α, β] \to R$ is continuous on $[α, β]$ and differentiable on $(α, β)$ , and $f$ is Riemann integrable on $[α, β]$ with $f = G^{'}$ on $(α, β)$ , then $\int_{α}^{β} f = G (β) - G (α)$ (Newton–Leibniz needs only continuity on $[a, b]$ , differentiability on $(a, b)$ , and a Riemann-integrable extension of the interior derivative).

[F6]

Additivity of the real part: $Re (u + v) = Re u + Re v$ for $u, v \in C$ , hence the same for every finite sum, and $Re (λ u) = λ Re u$ for real $λ$ ; these are the coordinate rules of the real-linear map $Re$ of [F2].

Proof

technique · direct; expand each real part with $\operatorname{Re}z=(z+\overline z)/2$, exhibit an explicit antiderivative whose real part has the integrand as derivative, and evaluate it by the fundamental theorem using the period $2\pi i$ of the exponential

1.1givenF2F6algebra

Scalar algebraic identity. Let $a, d \in C$ and $t \in R$ . By [F2], $Re (a e^{- i ω t}) = \frac{1}{2} (a e^{- i ω t} + \overline{a} \overline{e^{- i ω t}}) = \frac{1}{2} (a e^{- i ω t} + \overline{a} e^{i ω t})$ , and likewise $Re (d e^{- i ω t}) = \frac{1}{2} (d e^{- i ω t} + \overline{d} e^{i ω t})$ . Multiplying the two real expressions and using the conjugation rules of [F2] throughout gives $4 Re (a e^{- i ω t}) Re (d e^{- i ω t}) = a d e^{- 2 i ω t} + a \overline{d} + \overline{a} d + \overline{a} \overline{d} e^{2 i ω t}$ . Since $\overline{a d e^{- 2 i ω t}} = \overline{a} \overline{d} e^{2 i ω t}$ and $\overline{a \overline{d}} = \overline{a} d$ by [F2], the first and fourth terms are conjugate, as are the second and third, so the last display equals $2 Re (a d e^{- 2 i ω t}) + 2 Re (a \overline{d}) = 2 Re (a d e^{- 2 i ω t} + a \overline{d})$ by [F6]; hence $Re (a e^{- i ω t}) Re (d e^{- i ω t}) = \frac{1}{2} Re (a d e^{- 2 i ω t} + a \overline{d})$ .

2.1step 1.1F1F4algebra

Antiderivative. Define $Φ (t) : = \frac{a d e^{- 2 i ω t}}{- 2 i ω} + a \overline{d} t$ for $t \in R$ ; the division is by the nonzero complex number $- 2 i ω$ , and $Φ$ is differentiable with $Φ^{'} (t) = a d e^{- 2 i ω t} + a \overline{d}$ by [F1], [F4] and the algebra of derivatives: the derivative of $e^{- 2 i ω t}$ is $- 2 i ω e^{- 2 i ω t}$ because $\exp^{'} = \exp$ ([F1]) and the parameter map is real-linear. Hence the real function $G : = Re Φ$ is continuous on $[0, T]$ and differentiable on $(0, T)$ with derivative $G^{'} (t) = Re Φ^{'} (t) = Re (a d e^{- 2 i ω t} + a \overline{d}) = 2 Re (a e^{- i ω t}) Re (d e^{- i ω t})$ by [F4] and step 1.1; in particular $G^{'}$ is continuous, hence Riemann integrable on $[0, T]$ .

3.1step 2.1F3F5F6algebra

Scalar identity. Since $2 ω T = 4 π$ , the kernel computation of [F3] gives $e^{- 2 i ω T} = e^{- 4 π i} = 1$ ; therefore $Φ (T) = \frac{a d}{- 2 i ω} + a \overline{d} T$ and $Φ (0) = \frac{a d}{- 2 i ω}$ , so $Φ (T) - Φ (0) = a \overline{d} T$ . The fundamental theorem [F5] applied to $G$ and $G^{'}$ gives $\int_{0}^{T} G^{'} = G (T) - G (0) = Re (Φ (T) - Φ (0)) = T Re (a \overline{d})$ by [F6]. Since $G^{'} = 2 Re (a e^{- i ω t}) Re (d e^{- i ω t})$ by step 2.1, dividing the identity $\int_{0}^{T} G^{'} = T Re (a \overline{d})$ by $2 T > 0$ gives the scalar form of the Statement.

4.1step 2.1step 3.1F5F6algebra∎

Vector forms. Let $a, d \in C^{3}$ and $F (t) : = Re (a e^{- i ω t})$ , $G (t) : = Re (d e^{- i ω t})$ . For every $j, k \in {1, 2, 3}$ , the already proved scalar identity of step 3.1 gives $T^{- 1} \int_{0}^{T} F_{j} (t) G_{k} (t) d t = \frac{1}{2} Re (a_{j} \overline{d_{k}})$ . The coordinate inner product and cross product use finite sums: $⟨ F, G ⟩ = \sum_{j = 1}^{3} F_{j} G_{j}$ and $(F \times G)_{i} = \sum_{j, k = 1}^{3} ϵ_{i j k} F_{j} G_{k}$ . Each product has the explicit real antiderivative constructed in step 2.1 for its pair $(a_{j}, d_{k})$ ; summing those finitely many antiderivatives and applying [F5] proves that their integrals sum with the same coefficients. Hence $T^{- 1} \int_{0}^{T} ⟨ F, G ⟩ d t = \frac{1}{2} Re \sum_{j = 1}^{3} a_{j} \overline{d_{j}} = \frac{1}{2} Re ⟨ a, \overline{d} ⟩$ , and $T^{- 1} \int_{0}^{T} (F \times G)_{i} d t = \frac{1}{2} Re \sum_{j, k = 1}^{3} ϵ_{i j k} a_{j} \overline{d_{k}} = \frac{1}{2} Re (a \times \overline{d})_{i}$ by real linearity of [F6]. This proves both componentwise vector formulas, including all zero amplitudes.

Remarks

The conjugation in $\frac{1}{2} Re (a \overline{d})$ is essential and cannot be absorbed into the amplitudes: at $t = 0$ with $a = d = 1 + i$ one has $Re (a) Re (d) = 1$ while $\frac{1}{2} Re (a d) = \frac{1}{2} Re (2 i) = 0$ , so the real quadratic form and the complex square differ even pointwise.
The proof uses no choice principle: only the power-series exponential, its kernel, the fundamental theorem and real-linear algebra of $Re$ enter, and the integrand is a continuous real function on a compact interval.

Period averages of products of real parts of complex exponentials

Statement

Facts & Assumptions

Proof

Remarks

Depends on

Dependency tree · 2 levels

Sources