Positive Time Test Functions and Star Operations

This file defines test functions supported in the positive time region and implements the star operation (complex conjugation composed with time reflection) for test functions.

Main definitions

• HasPositiveTime: Predicate for spacetime points with positive time component
• positiveTimeSet: The set of all positive time points
• PositiveTimeTestFunction: Test functions supported in the positive time region
• starTestFunction: Star operation combining time reflection and complex conjugation
• starRingEnd_iteratedFDeriv_norm_eq: Helper lemma for norm preservation under star operation

Main results

• is_open_positiveTimeSet: The positive time set is open
• Star TestFunctionℂ: Star instance for complex test functions

def HasPositiveTime (x : SpaceTime) : Prop

A spacetime point has positive time if its time component is positive

Equations

• HasPositiveTime x = (getTimeComponent x > 0)

def positiveTimeSet : Set SpaceTime

The set of all spacetime points with positive time

Equations

• positiveTimeSet = {x : SpaceTime | HasPositiveTime x}

theorem is_open_positiveTimeSet : IsOpen positiveTimeSet

The positive time set is open

def PositiveTimeTestFunctions.submodule : Submodule ℝ TestFunction

Submodule of real-valued test functions supported in the positive time region

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev PositiveTimeTestFunction : Type

Type of real-valued test functions supported in the positive time region

Equations

• PositiveTimeTestFunction = ↥PositiveTimeTestFunctions.submodule

@[implicit_reducible]

noncomputable instance instAddCommMonoidPositiveTimeTestFunction : AddCommMonoid PositiveTimeTestFunction

Equations

• instAddCommMonoidPositiveTimeTestFunction = inferInstance

@[implicit_reducible]

noncomputable instance instAddCommGroupPositiveTimeTestFunction : AddCommGroup PositiveTimeTestFunction

Equations

• instAddCommGroupPositiveTimeTestFunction = inferInstance

theorem PositiveTimeTestFunction.sum_smul_mem {n : ℕ} (f : Fin n → PositiveTimeTestFunction) (c : Fin n → ℝ) : ∃ (g : PositiveTimeTestFunction), ↑g = ∑ i : Fin n, c i • ↑(f i)

Linear combinations of positive-time test functions are positive-time test functions.

def PositiveTimeTestFunctionsℂ.submodule : Submodule ℂ TestFunctionℂ

Submodule of complex-valued test functions supported in the positive time region. This is a ℂ-submodule since ℂ-scalar multiplication preserves support.

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev PositiveTimeTestFunctionℂ : Type

Type of complex-valued test functions supported in the positive time region

Equations

• PositiveTimeTestFunctionℂ = ↥PositiveTimeTestFunctionsℂ.submodule

@[implicit_reducible]

noncomputable instance instAddCommMonoidPositiveTimeTestFunctionℂ : AddCommMonoid PositiveTimeTestFunctionℂ

Equations

• instAddCommMonoidPositiveTimeTestFunctionℂ = inferInstance

@[implicit_reducible]

noncomputable instance instAddCommGroupPositiveTimeTestFunctionℂ : AddCommGroup PositiveTimeTestFunctionℂ

Equations

• instAddCommGroupPositiveTimeTestFunctionℂ = inferInstance

theorem PositiveTimeTestFunctionℂ.zero_on_nonpositive (f : PositiveTimeTestFunctionℂ) {x : SpaceTime} (hx : getTimeComponent x ≤ 0) : ↑f x = 0

theorem starRingEnd_iteratedFDeriv_norm_eq (g : TestFunctionℂ) (n : ℕ) (x : SpaceTime) : ‖iteratedFDeriv ℝ n (fun (x : SpaceTime) => (starRingEnd ℂ) (g x)) x‖ = ‖iteratedFDeriv ℝ n (⇑g) x‖

Helper lemma: starRingEnd ℂ commutes through derivatives and preserves norms

noncomputable def starTestFunction (f : TestFunctionℂ) : TestFunctionℂ

Star operation on test functions: time reflection followed by complex conjugation

Equations

• starTestFunction f = { toFun := fun (x : SpaceTime) => (starRingEnd ℂ) ((QFT.compTimeReflection f) x), smooth' := ⋯, decay' := ⋯ }

@[implicit_reducible]

noncomputable instance instStarTestFunctionℂ : Star TestFunctionℂ

Star instance for complex test functions

Equations

• instStarTestFunctionℂ = { star := fun (f : TestFunctionℂ) => starTestFunction f }

theorem PositiveTimeTestFunction.zero_on_nonpositive (f : PositiveTimeTestFunction) {x : SpaceTime} (hx : getTimeComponent x ≤ 0) : ↑f x = 0