Complex Test Function Linearity

This file contains lemmas about linearity properties of complex test functions and their pairings with field configurations.

Main Results:

Complex Arithmetic Helpers:

• re_of_complex_combination: Real part of complex linear combination
• im_of_complex_combination: Imaginary part of complex linear combination

Decomposition Linearity:

• ω_re_decompose_linear: ω-linearity of real component under complex operations
• ω_im_decompose_linear: ω-linearity of imaginary component under complex operations

Pairing Linearity:

• pairing_linear_combo: Key result showing distributionPairingℂReal is ℂ-linear in the test function argument

These results are essential for proving bilinearity of Schwinger functions and other quantum field theory constructions.

Main definitions

• toComplex: Embed real Schwartz functions into complex Schwartz functions
• toComplexCLM: The continuous ℝ-linear map version of toComplex

theorem ω_re_decompose_linear (ω : FieldConfiguration) (f g : TestFunctionℂ) (t s : ℂ) : ω (complexTestFunctionDecompose (t • f + s • g)).1 = t.re * ω (complexTestFunctionDecompose f).1 - t.im * ω (complexTestFunctionDecompose f).2 + s.re * ω (complexTestFunctionDecompose g).1 - s.im * ω (complexTestFunctionDecompose g).2

ω-linearity of the real component of the complex test-function decomposition under complex linear combinations. This follows from ℝ-linearity of ω and pointwise behavior of complex operations on Schwartz functions.

theorem ω_im_decompose_linear (ω : FieldConfiguration) (f g : TestFunctionℂ) (t s : ℂ) : ω (complexTestFunctionDecompose (t • f + s • g)).2 = t.re * ω (complexTestFunctionDecompose f).2 + t.im * ω (complexTestFunctionDecompose f).1 + s.re * ω (complexTestFunctionDecompose g).2 + s.im * ω (complexTestFunctionDecompose g).1

ω-linearity of the imaginary component of the complex test-function decomposition under complex linear combinations.

theorem pairing_linear_combo (ω : FieldConfiguration) (f g : TestFunctionℂ) (t s : ℂ) : distributionPairingℂReal ω (t • f + s • g) = t * distributionPairingℂReal ω f + s * distributionPairingℂReal ω g

Linearity of the complex pairing in the test-function argument.

Helper lemmas for real→complex Schwartz embedding

theorem Complex.norm_ofRealCLM : ‖ofRealCLM‖ = 1

The norm of the ℝ-linear embedding ℝ → ℂ is exactly 1.

theorem norm_compContinuousMultilinearMap_ofReal {n : ℕ} {E : Fin n → Type u_1} [(i : Fin n) → NormedAddCommGroup (E i)] [(i : Fin n) → NormedSpace ℝ (E i)] (m : ContinuousMultilinearMap ℝ E ℝ) : ‖Complex.ofRealCLM.compContinuousMultilinearMap m‖ = ‖m‖

Composing a continuous multilinear map (to ℝ) with the real→complex embedding preserves the operator norm, since the embedding is an isometry.

theorem iteratedFDeriv_ofReal_norm_eq (f : TestFunction) (n : ℕ) (x : SpaceTime) : ‖iteratedFDeriv ℝ n (fun (x : SpaceTime) => ↑(f x)) x‖ = ‖iteratedFDeriv ℝ n f.toFun x‖

The norm of the n-th iterated derivative of a Schwartz function composed with real→complex embedding equals the norm of the n-th iterated derivative of the original Schwartz function. This follows from the chain rule and the fact that the embedding is an isometry.

noncomputable def toComplex (f : TestFunction) : TestFunctionℂ

Embed a real test function as a complex-valued test function by coercing values via ℝ → ℂ.

Equations

• toComplex f = { toFun := fun (x : SpaceTime) => ↑(f x), smooth' := ⋯, decay' := ⋯ }

@[simp]

theorem toComplex_apply (f : TestFunction) (x : SpaceTime) : (toComplex f) x = ↑(f x)

@[simp]

theorem complex_testfunction_decompose_toComplex_fst (f : TestFunction) : (complexTestFunctionDecompose (toComplex f)).1 = f

@[simp]

theorem complex_testfunction_decompose_toComplex_snd (f : TestFunction) : (complexTestFunctionDecompose (toComplex f)).2 = 0

@[simp]

theorem toComplex_add (f g : TestFunction) : toComplex (f + g) = toComplex f + toComplex g

@[simp]

theorem toComplex_smul (c : ℝ) (f : TestFunction) : toComplex (c • f) = ↑c • toComplex f

noncomputable def toComplexCLM : TestFunction →L[ℝ] TestFunctionℂ

The embedding of real Schwartz functions into complex Schwartz functions is a continuous ℝ-linear map. This follows from SchwartzMap.mkCLM since:

1. The map is linear (toComplex_add, toComplex_smul)
2. The composition with ofRealCLM is smooth
3. Derivative norms are preserved (iteratedFDeriv_ofReal_norm_eq) so the Schwartz seminorm bounds are satisfied.

Equations

• toComplexCLM = SchwartzMap.mkCLM (fun (f : SchwartzMap SpaceTime ℝ) (x : SpaceTime) => ↑(f x)) toComplexCLM._proof_4 toComplexCLM._proof_5 toComplexCLM._proof_6 toComplexCLM._proof_7

@[simp]

theorem toComplexCLM_apply (f : TestFunction) : toComplexCLM f = toComplex f

@[simp]

theorem distributionPairingℂ_real_toComplex (ω : FieldConfiguration) (f : TestFunction) : distributionPairingℂReal ω (toComplex f) = ↑(distributionPairing ω f)

@[simp]

theorem GJGeneratingFunctionalℂ_toComplex (dμ_config : MeasureTheory.ProbabilityMeasure FieldConfiguration) (f : TestFunction) : GJGeneratingFunctionalℂ dμ_config (toComplex f) = GJGeneratingFunctional dμ_config f

Pointwise conjugation on complex Schwartz functions

For a complex-valued Schwartz function f : E → ℂ, we define the pointwise conjugate conjSchwartz f := fun x ↦ conj (f x). This is again a Schwartz function because conjugation is a continuous ℝ-linear map on ℂ.

noncomputable def conjSchwartz {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (f : SchwartzMap E ℂ) : SchwartzMap E ℂ

Pointwise conjugation of a complex Schwartz function. (conjSchwartz f)(x) = conj(f(x))

This is defined using the continuous ℝ-linear equivalence Complex.conjCLE : ℂ ≃L[ℝ] ℂ. Since conjugation is smooth and an isometry, it preserves all Schwartz seminorms.

Equations

• conjSchwartz f = { toFun := fun (x : E) => (starRingEnd ℂ) (f x), smooth' := ⋯, decay' := ⋯ }

@[simp]

theorem conjSchwartz_apply {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (f : SchwartzMap E ℂ) (x : E) : (conjSchwartz f) x = (starRingEnd ℂ) (f x)

@[simp]

theorem conjSchwartz_conjSchwartz {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (f : SchwartzMap E ℂ) : conjSchwartz (conjSchwartz f) = f

Conjugation is involutive: conj(conj(f)) = f

theorem distributionPairingℂ_real_conj (ω : FieldConfiguration) (f : TestFunctionℂ) : (starRingEnd ℂ) (distributionPairingℂReal ω f) = distributionPairingℂReal ω (conjSchwartz f)

Key identity: For a real-valued distribution ω, conjugating the pairing equals pairing with the conjugated test function.

conj(⟨ω, f⟩) = ⟨ω, conj(f)⟩

This follows from:

• ⟨ω, f⟩ = ⟨ω, f_re⟩ + i⟨ω, f_im⟩
• conj(⟨ω, f⟩) = ⟨ω, f_re⟩ - i⟨ω, f_im⟩
• ⟨ω, conj(f)⟩ = ⟨ω, conj(f)_re⟩ + i⟨ω, conj(f)_im⟩
• conj(f)_re = f_re and conj(f)_im = -f_im