LemmaStatement: AI-adaptedProof: AI-generatedPipeline-generatedprecheck pass

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.

Periodic heat-stencil eigenvalues and θ amplification factor

Statement

On the finite periodic rectangular $d$ -grid of Fully discrete θ heat finite-difference scheme, let $ℓ_{j} \in {0, \dots, N_{j} - 1}$ and

ϕ_{ℓ} (i) = \exp (2 π i \sum_{j = 1}^{d} \frac{ℓ_{j} i_{j}}{N_{j}}) .

Then $ϕ_{ℓ}$ is an eigenvector of $A_{h}^{p e r}$ with eigenvalue

λ_{ℓ} = 4 \sum_{j = 1}^{d} \frac{κ_{j}}{h_{j}^{2}} \sin^{2} (\frac{π ℓ_{j}}{N_{j}}) \geq 0.

For zero source, the $θ$ update multiplies this mode at each step by

g_{θ} (ℓ) = \frac{1 - (1 - θ) Δ t λ_{ℓ}}{1 + θ Δ t λ_{ℓ}} .

The displayed modes form a basis of the complexified grid space, so this factor describes the full periodic update.

Facts & Assumptions

Given: A finite periodic rectangular grid with $d \geq 1$ , $N_{j} \geq 2$ , $h_{j} = L_{j} / N_{j}$ , $κ_{j} > 0$ , and $θ \in [0, 1]$ as defined in Fully discrete θ heat finite-difference scheme.

[F1]

Fully discrete θ heat finite-difference scheme defines $A_{h}^{p e r}$ by periodic wraparound and the update $Δ t^{- 1} (U^{n + 1} - U^{n}) + A_{h}^{p e r} ((1 - θ) U^{n} + θ U^{n + 1}) = 0$ when the source is zero.

[F2]

The complex exponential obeys the addition law and has kernel $2 π i Z$ ; its Cartesian Euler formula gives unit modulus on imaginary arguments, and complex conjugation and modulus obey their field laws ( $\exp (z + w) = \exp z \exp w$ , and the complex exponential extends the real exponential, $\ker (\exp) = 2 π i Z$ , and $\exp z = \exp w$ exactly when $z - w \in 2 π i Z$ , $\exp (x + i y) = e^{x} (\cos y + i \sin y)$ , $∣ \exp (x + i y) ∣ = e^{x}$ , and $e^{i π} + 1 = 0$ , Conjugation is an involutive real-field automorphism, $z \overline{z} = ∣ z ∣^{2}$ , and modulus is definite, multiplicative, and subadditive).

[F3]

For real $a$ , $\cos (2 a) = 1 - 2 \sin^{2} (a)$ (Double-angle and quadratic power-reduction identities).

[F4]

For $N \geq 1$ and integer frequencies $k, m$ , the finite character sum $\sum_{r = 0}^{N - 1} \exp (2 π i (k - m) r / N)$ is $N$ if $k \equiv m (m o d N)$ and zero otherwise (Orthogonality of the characters $x \mapsto e^{2 π i k x / N}$ on $Z / N Z$ ).

[F5]

Finite sums may be reindexed and iterated over Cartesian-product index sets (Finite commutative-monoid sums are invariant under bijective reindexing, split over disjoint unions, and satisfy the finite Fubini rule).

[F6]

Finite Fourier inversion expands every complex function on $Z / N Z$ in its positive-exponent character modes, for each $N \geq 1$ (Finite Fourier inversion for the unitary transform on $Z / N Z$ ).

Proof

1.1F1F2F3algebra

Changing a representative $i_{j}$ by $N_{j}$ changes the exponent by the integer multiple $2 π i ℓ_{j}$ , so [F2] makes $ϕ_{ℓ}$ well-defined on the periodic grid. It is nonzero because $ϕ_{ℓ} (0) = 1$ . Put $β_{j} = 2 π ℓ_{j} / N_{j}$ . The addition law gives $ϕ_{ℓ} (i \pm e_{j}) = e^{\pm i β_{j}} ϕ_{ℓ} (i)$ , including wrapped indices. By [F2], $e^{i β_{j}}$ has modulus one and $e^{i β_{j}} e^{- i β_{j}} = 1$ , hence $e^{- i β_{j}} = \overline{e^{i β_{j}}}$ . The Cartesian Euler formula in [F2] and [F3] therefore give $2 - e^{i β_{j}} - e^{- i β_{j}} = 2 - 2 \cos β_{j} = 4 \sin^{2} (β_{j} / 2)$ . Substitution into [F1] yields the asserted eigenvalue on summing over $j$ ; it is nonnegative because each $κ_{j} / h_{j}^{2}$ is positive and each sine square is nonnegative.

1.2F2F4F5F6algebra

Put $P = \prod_{j = 1}^{d} N_{j} > 0$ . Repeated complex distributivity $a (b + c) = a b + a c$ moves a scalar through a finite sum. Applying this algebra law coordinate by coordinate, together with [F2] and the finite Fubini rule [F5], gives $\sum_{i \in G_{h}^{p e r}} ϕ_{ℓ} (i) \overline{ϕ_{m} (i)} = \prod_{j = 1}^{d} \sum_{r = 0}^{N_{j} - 1} \exp (2 π i (ℓ_{j} - m_{j}) r / N_{j})$ . By [F4] this is $P$ when $ℓ = m$ and zero otherwise: distinct index tuples have a coordinate whose two standard representatives are not congruent modulo $N_{j}$ . Thus the nonzero modes are orthogonal, also after multiplying the pairing by the positive grid weight $\prod_{j} h_{j}$ . Apply the published one-dimensional inversion formula [F6] successively to each of the $d$ coordinates of any grid vector. Finite Fubini [F5] and the same distributivity combine these expansions into a linear combination of the displayed product modes $ϕ_{ℓ}$ ; hence they span the complexified grid space. If a linear combination of them is zero, multiply it by $\overline{ϕ_{m}}$ and sum over the grid. The displayed pairing identity leaves $P$ times its $m$ th coefficient, so every coefficient is zero. The modes therefore form a basis.

2.1F1step 1.1algebra

Substituting $U^{n} = a_{n} ϕ_{ℓ}$ into the zero-source update gives $(a_{n + 1} - a_{n}) + Δ t λ_{ℓ} ((1 - θ) a_{n} + θ a_{n + 1}) = 0$ . Since $1 + θ Δ t λ_{ℓ} \geq 1$ , solving this scalar equation gives $a_{n + 1} = g_{θ} (ℓ) a_{n}$ .

3.1step 2.1step 1.2algebra∎

By step 1.2 every grid vector is a finite linear combination of these modes, and the update acts on each component by the factor from step 2.1. Thus the stated factors describe the full update.

Remarks

The calculation is for periodic grids. It does not establish stability of a finite Dirichlet matrix or of a variable-coefficient stencil.

Depends on

Used by

Dependency tree · two levels

54 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

Endre Süli, B6.1 Numerical Solution of Partial Differential Equations: A brief introduction to the theory of finite difference approximation of PDEs (standard reference, not scraped)
Benjamin Seibold, MIT 18.336, Lecture 14: Von Neumann Stability Analysis (Spring 2009) (standard reference, not scraped)
Martin Krosche, Hermann G. Matthies, and Oliver Kayser-Herold, Lecture Notes: Introduction to PDEs and Numerical Methods, Technical University Braunschweig, Revision 1.1 (2008), hosted by University of Jyväskylä (standard reference, not scraped)