Hardy-space and weak-PDE interfaces for one-dimensional scattering with memory

Definition

frame_2026_scattering_interfaces

by ShouqiaoWang · Aug 26, 2026 · Mathlib c5ea003 (Lean v4.30.0)

fourier-analysisharmonic-analysisoperator-theorypartial-differential-equationsscattering-theorywave-equations

This bundle gives concrete function-space semantics for the scattering theorem. A Medium records a complex coefficient $a(x,t)$ , positive localization radii $R,T$ , positive decay $\gamma$ , rectangular support, spatial measurability, and uniform smoothness in time. Frequency signals are holomorphic upper-half-plane functions represented by canonical zero extension. The bundle defines the weighted Hardy energy $E_\alpha$ , the source class $(z+i)^{-1}\mathcal H_\alpha$ , the target class $z^{-1}\mathcal H_\alpha$ , and local Hardy control for frequency fields.

The coefficient Fourier transform, memory multiplier $z/(z+i\gamma)$ , frequency convolution $A_M(x)$ , and weak equation $D_x^2-z^2+A_M(x)$ are explicit integrals and test-function identities. Integrability and measurability predicates guard every Bochner integral. Exterior frequency data are the exact incoming, reflected, and transmitted plane-wave formulas, and frequency uniqueness uses almost-everywhere equality in $x$ on each upper-half-plane slice.

For the time problem, an energy field contains its value and weak time and space derivatives, finite $L^2$ energy on every time slice, $H^1$ continuity of the value, and $L^2$ continuity of the time derivative. The causal exponential-memory term and the weak spacetime equation are defined directly. Admissible time data are smooth compactly supported signals supported in $(R,\infty)$ ; the Fourier–Laplace transform uses the convention $\widehat g(z)=\int e^{izt}g(t)\,dt$ . The bundle finally defines graded boundedness of one common frequency operator, Fourier intertwining with a time operator, and the combined proposition containing the conclusions of Theorems 1.1 and 1.2. No PDE, analyticity, scattering, or uniqueness condition is supplied as a freely chosen predicate.

Definition code

import Mathlib

/-!
# Concrete interfaces for one-dimensional scattering with memory

The carriers in this file are actual complex-valued functions.  Frequency
signals are functions on the open upper half-plane (represented canonically
by zero extension to its complement), frequency solutions are functions of
position and upper-half-plane frequency, and time solutions are finite-energy
fields with specified weak derivatives.  In particular, none of the PDE,
Hardy, Fourier, or exterior-data conditions is a freely chosen predicate.

We use the Fourier convention of the source:
`hat g z = integral t, exp (i z t) * g t`; hence the inverse transform carries
`exp (-i z t) / (2*pi)`.  The operator `D` in the paper is `-i * partial`.
-/

noncomputable section

open scoped ENNReal NNReal
open Filter MeasureTheory Set

namespace ScatteringInterfaces

/-! ## The medium -/

/-- A coefficient supported in the closed rectangle `[-R,R] x [-T,T]`. -/
def SupportedInRectangle (a : ℝ → ℝ → ℂ) (R T : ℝ) : Prop :=
  ∀ x t, R < |x| ∨ T < |t| → a x t = 0

/-- Smoothness in time, with every time derivative bounded uniformly in both
space and time.  The bound may depend on the derivative order. -/
def UniformlyTimeSmooth (a : ℝ → ℝ → ℂ) : Prop :=
  (∀ x, ContDiff ℝ ⊤ (a x)) ∧
    ∀ k : ℕ, ∃ C : ℝ, 0 ≤ C ∧
      ∀ x t, ‖iteratedDeriv k (a x) t‖ ≤ C

/-- Strong measurability of every spatial slice. -/
def SpatiallyMeasurable (a : ℝ → ℝ → ℂ) : Prop :=
  ∀ t, StronglyMeasurable (fun x => a x t)

/-- The data in equation (1.1).  Its laws are precisely coefficient
regularity/localization assumptions, not scattering conclusions. -/
structure Medium where
  coefficient : ℝ → ℝ → ℂ
  spatialRadius : ℝ
  timeRadius : ℝ
  memoryDecay : ℝ
  spatialRadius_pos : 0 < spatialRadius
  timeRadius_pos : 0 < timeRadius
  memoryDecay_pos : 0 < memoryDecay
  support : SupportedInRectangle coefficient spatialRadius timeRadius
  measurable : SpatiallyMeasurable coefficient
  timeSmooth : UniformlyTimeSmooth coefficient

/-- The zero coefficient is an explicit inhabitant of the hypothesis class.
This witnesses that `Medium` itself is not an empty interface. -/
def freeMedium : Medium := by
  refine
    { coefficient := fun _ _ => 0
      spatialRadius := 1
      timeRadius := 1
      memoryDecay := 1
      spatialRadius_pos := by norm_num
      timeRadius_pos := by norm_num
      memoryDecay_pos := by norm_num
      support := ?_
      measurable := ?_
      timeSmooth := ?_ }
  · simp [SupportedInRectangle]
  · intro t
    exact stronglyMeasurable_const
  · constructor
    · intro x
      fun_prop
    · intro k
      refine ⟨0, le_rfl, ?_⟩
      intro x t
      simp

/-! ## Frequency functions and Hardy spaces -/

/-- The open upper half-plane. -/
def upperHalfPlane : Set ℂ := {z | 0 < z.im}

/-- Functions on the upper half-plane, represented uniquely as functions on
`ℂ` which vanish off the upper half-plane.  The canonical zero extension
prevents values outside the physical frequency domain from destroying
uniqueness of solutions. -/
def upperFunctionSubmodule : Submodule ℂ (ℂ → ℂ) where
  carrier := {f | ∀ z, z ∉ upperHalfPlane → f z = 0}
  zero_mem' := by simp
  add_mem' := by
    intro f g hf hg z hz
    simp [hf z hz, hg z hz]
  smul_mem' := by
    intro c f hf z hz
    simp [hf z hz]

/-- A scalar frequency signal on `Im z > 0`. -/
abbrev FrequencySignal : Type := upperFunctionSubmodule

/-- A frequency-domain field `u(x,z)`, `x in ℝ`, `Im z > 0`. -/
abbrev FrequencyField : Type := ℝ → FrequencySignal

/-- A scalar time signal. -/
abbrev TimeSignal : Type := ℝ → ℂ

/-- A spacetime field, with the time variable first. -/
abbrev TimeField : Type := ℝ → ℝ → ℂ

/-- The point `frequency + i*sigma` on a positive horizontal line. -/
def verticalPoint (sigma : {s : ℝ // 0 < s}) (frequency : ℝ) : ℂ :=
  (frequency : ℂ) + Complex.I * (sigma.1 : ℂ)

lemma verticalPoint_mem (sigma : {s : ℝ // 0 < s}) (frequency : ℝ) :
    verticalPoint sigma frequency ∈ upperHalfPlane := by
  simp [verticalPoint, upperHalfPlane, sigma.2]

/-- The weighted squared `L^2` norm on one horizontal line from (1.3). -/
noncomputable def verticalHardyEnergy (alpha : ℝ) (f : FrequencySignal)
    (sigma : {s : ℝ // 0 < s}) : ℝ≥0∞ :=
  ENNReal.ofReal (Real.exp (-2 * sigma.1 * alpha)) *
    ∫⁻ frequency : ℝ,
      ENNReal.ofReal (‖f.1 (verticalPoint sigma frequency)‖ ^ 2)

/-- The squared Hardy norm, expressed as the supremum over positive
horizontal lines.  `ENNReal` makes non-integrability equal to `infinity`
rather than silently assigning integral zero. -/
noncomputable def hardySqNorm (alpha : ℝ) (f : FrequencySignal) : ℝ≥0∞ :=
  ⨆ sigma : {s : ℝ // 0 < s}, verticalHardyEnergy alpha f sigma

/-- Membership in the weighted Hardy space `H_alpha` of (1.3). -/
def MemHardy (alpha : ℝ) (f : FrequencySignal) : Prop :=
  DifferentiableOn ℂ f.1 upperHalfPlane ∧ hardySqNorm alpha f < ⊤

/-- Multiplication by `z+i`, used to realize `(omega+i)^(-1) H_alpha`. -/
def incomingLift (f : FrequencySignal) : FrequencySignal :=
  ⟨fun z => (z + Complex.I) * f.1 z, by
    intro z hz
    simp [f.2 z hz]⟩

/-- Multiplication by `z`, used to realize `omega^(-1) H_alpha`. -/
def outgoingLift (f : FrequencySignal) : FrequencySignal :=
  ⟨fun z => z * f.1 z, by
    intro z hz
    simp [f.2 z hz]⟩

/-- The source space `(omega+i)^(-1) H_alpha`. -/
def MemIncomingHardy (alpha : ℝ) (f : FrequencySignal) : Prop :=
  MemHardy alpha (incomingLift f)

/-- The target space `omega^(-1) H_alpha`. -/
def MemOutgoingHardy (alpha : ℝ) (f : FrequencySignal) : Prop :=
  MemHardy alpha (outgoingLift f)

/-- Local-in-space vertical energy of `z*u(x,z)` on `[-radius,radius]`. -/
noncomputable def localVerticalEnergy (alpha : ℝ) (u : FrequencyField)
    (radius : ℝ) (sigma : {s : ℝ // 0 < s}) : ℝ≥0∞ :=
  ENNReal.ofReal (Real.exp (-2 * sigma.1 * alpha)) *
    ∫⁻ frequency : ℝ,
      ∫⁻ x : ℝ in Set.Icc (-radius) radius,
        ENNReal.ofReal
          (‖(outgoingLift (u x)).1 (verticalPoint sigma frequency)‖ ^ 2)

/-- The squared local Hardy norm on a bounded spatial interval. -/
noncomputable def localHardySqNorm (alpha : ℝ) (u : FrequencyField)
    (radius : ℝ) : ℝ≥0∞ :=
  ⨆ sigma : {s : ℝ // 0 < s}, localVerticalEnergy alpha u radius sigma

/-- The concrete meaning of `omega^(-1) H_{infinity,loc}`: holomorphy in
frequency and membership in one weighted local Hardy layer on every bounded
spatial interval. -/
def FrequencyLocal (u : FrequencyField) : Prop :=
  (∀ x, DifferentiableOn ℂ (u x).1 upperHalfPlane) ∧
    (∀ z, z ∈ upperHalfPlane →
      AEStronglyMeasurable (fun x => (u x).1 z) volume) ∧
    ∃ alpha : ℝ, ∀ radius : ℝ, 0 < radius →
      localHardySqNorm alpha u radius < ⊤

/-! ## Fourier transform and the frequency equation -/

/-- The time Fourier transform of the coefficient, with the source's sign
convention. -/
noncomputable def coefficientFourier (M : Medium) (x frequency : ℝ) : ℂ :=
  ∫ t : ℝ,
    Complex.exp (Complex.I * ((frequency * t : ℝ) : ℂ)) * M.coefficient x t

/-- The multiplier `z/(z+i*gamma)` encoding exponential memory. -/
def memoryMultiplier (M : Medium) (z : ℂ) : ℂ :=
  z / (z + Complex.I * (M.memoryDecay : ℂ))

/-- The integrand in the convolution formula (1.4), including the memory
multiplier from (1.2). -/
def frequencyActionIntegrand (M : Medium) (u : FrequencyField)
    (x : ℝ) (z : ℂ) (frequency : ℝ) : ℂ :=
  let w : ℂ := (frequency : ℂ) + Complex.I * (z.im : ℂ)
  coefficientFourier M x (z.re - frequency) *
    memoryMultiplier M w * (u x).1 w

/-- The explicit operator `A(x) = a(x,D_omega) omega/(omega+i*gamma)`. -/
noncomputable def frequencyAction (M : Medium) (u : FrequencyField)
    (x : ℝ) (z : ℂ) : ℂ :=
  ((1 : ℂ) / (2 * (Real.pi : ℂ))) *
    ∫ frequency : ℝ, frequencyActionIntegrand M u x z frequency

/-- Absolute/Bochner integrability needed for the convolution defining
`A(x)u`. -/
def FrequencyActionDefined (M : Medium) (u : FrequencyField) : Prop :=
  ∀ z, z ∈ upperHalfPlane →
    AEStronglyMeasurable (fun x => frequencyAction M u x z) volume ∧
      ∀ᵐ x : ℝ,
        Integrable (fun frequency : ℝ => frequencyActionIntegrand M u x z frequency)

/-- A compactly supported smooth scalar test function. -/
def IsSpatialTestFunction (phi : ℝ → ℂ) : Prop :=
  ContDiff ℝ ⊤ phi ∧ HasCompactSupport phi

/-- The distributional integrand for
`(D_x^2 - z^2 + A(x))u = 0`, where `D_x = -i*partial_x`.
The second derivative is placed on the test function. -/
def weakFrequencyIntegrand (M : Medium) (u : FrequencyField)
    (z : ℂ) (phi : ℝ → ℂ) (x : ℝ) : ℂ :=
  -(u x).1 z * iteratedDeriv 2 phi x -
    z ^ 2 * (u x).1 z * phi x + frequencyAction M u x z * phi x

/-- A weak frequency solution of the actual equation `P u = 0`. -/
def IsWeakFrequencySolution (M : Medium) (u : FrequencyField) : Prop :=
  FrequencyLocal u ∧ FrequencyActionDefined M u ∧
    ∀ z, z ∈ upperHalfPlane → ∀ phi : ℝ → ℂ,
      IsSpatialTestFunction phi →
        Integrable (weakFrequencyIntegrand M u z phi) ∧
          (∫ x : ℝ, weakFrequencyIntegrand M u z phi x) = 0

/-- The exact plane-wave identities in (1.6). -/
def HasFrequencyExteriorData (M : Medium) (incoming reflected transmitted : FrequencySignal)
    (u : FrequencyField) : Prop :=
  ∀ x z, z ∈ upperHalfPlane →
    (x < -M.spatialRadius →
      (u x).1 z = incoming.1 z * Complex.exp (Complex.I * z * (x : ℂ)) +
        reflected.1 z * Complex.exp (-Complex.I * z * (x : ℂ))) ∧
    (M.spatialRadius < x →
      (u x).1 z = transmitted.1 z * Complex.exp (Complex.I * z * (x : ℂ)))

/-- Equality of weak frequency fields in the natural almost-everywhere sense
on every upper-half-plane frequency slice. -/
def FrequencyEquivalent (u v : FrequencyField) : Prop :=
  ∀ z, z ∈ upperHalfPlane →
    (fun x => (u x).1 z) =ᵐ[volume] fun x => (v x).1 z

/-! ## Time-domain finite-energy solutions -/

/-- A smooth compactly supported test function on spacetime `(t,x)`. -/
def IsSpaceTimeTestFunction (phi : ℝ × ℝ → ℂ) : Prop :=
  ContDiff ℝ ⊤ phi ∧ HasCompactSupport phi

/-- Time derivative of a spacetime test function. -/
def testTimeDerivative (phi : ℝ × ℝ → ℂ) (p : ℝ × ℝ) : ℂ :=
  deriv (fun t => phi (t, p.2)) p.1

/-- Space derivative of a spacetime test function. -/
def testSpaceDerivative (phi : ℝ × ℝ → ℂ) (p : ℝ × ℝ) : ℂ :=
  deriv (fun x => phi (p.1, x)) p.2

/-- A candidate `du` is the distributional time derivative of `u`. -/
def IsWeakTimeDerivative (u du : TimeField) : Prop :=
  ∀ phi : ℝ × ℝ → ℂ, IsSpaceTimeTestFunction phi →
    Integrable (fun p => du p.1 p.2 * phi p) ∧
    Integrable (fun p => u p.1 p.2 * testTimeDerivative phi p) ∧
    (∫ p : ℝ × ℝ, du p.1 p.2 * phi p) =
      -(∫ p : ℝ × ℝ, u p.1 p.2 * testTimeDerivative phi p)

/-- A candidate `du` is the distributional space derivative of `u`. -/
def IsWeakSpaceDerivative (u du : TimeField) : Prop :=
  ∀ phi : ℝ × ℝ → ℂ, IsSpaceTimeTestFunction phi →
    Integrable (fun p => du p.1 p.2 * phi p) ∧
    Integrable (fun p => u p.1 p.2 * testSpaceDerivative phi p) ∧
    (∫ p : ℝ × ℝ, du p.1 p.2 * phi p) =
      -(∫ p : ℝ × ℝ, u p.1 p.2 * testSpaceDerivative phi p)

/-- Squared `L^2` distance, valued in `ENNReal` so a non-integrable function
has infinite distance. -/
noncomputable def l2SqDistance (f g : ℝ → ℂ) : ℝ≥0∞ :=
  ∫⁻ x : ℝ, ENNReal.ofReal (‖f x - g x‖ ^ 2)

/-- A concrete representative of a field in
`C_t H^1_x intersection C^1_t L^2_x`.  The derivative laws make the named
derivatives part of the standard Sobolev structure rather than arbitrary
semantic data. -/
structure EnergyField where
  value : TimeField
  timeDerivative : TimeField
  spaceDerivative : TimeField
  timeDerivative_law : IsWeakTimeDerivative value timeDerivative
  spaceDerivative_law : IsWeakSpaceDerivative value spaceDerivative
  sliceMeasurable : ∀ t,
    AEStronglyMeasurable (value t) volume ∧
    AEStronglyMeasurable (timeDerivative t) volume ∧
    AEStronglyMeasurable (spaceDerivative t) volume
  finiteEnergy : ∀ t,
    (∫⁻ x : ℝ, ENNReal.ofReal (‖value t x‖ ^ 2)) < ⊤ ∧
    (∫⁻ x : ℝ, ENNReal.ofReal (‖timeDerivative t x‖ ^ 2)) < ⊤ ∧
    (∫⁻ x : ℝ, ENNReal.ofReal (‖spaceDerivative t x‖ ^ 2)) < ⊤
  h1Continuous : ∀ t0,
    Tendsto
      (fun t => l2SqDistance (value t) (value t0) +
        l2SqDistance (spaceDerivative t) (spaceDerivative t0))
      (nhds t0) (nhds 0)
  timeDerivativeContinuous : ∀ t0,
    Tendsto (fun t => l2SqDistance (timeDerivative t) (timeDerivative t0))
      (nhds t0) (nhds 0)

/-- The integrand in the causal memory convolution. -/
def memoryIntegrand (M : Medium) (u : EnergyField) (t x s : ℝ) : ℂ :=
  Complex.exp (-((M.memoryDecay * (t - s) : ℝ) : ℂ)) *
    (-Complex.I * u.timeDerivative s x)

/-- The causal integral from `-infinity` to `t` in equation (1.1). -/
noncomputable def memoryTerm (M : Medium) (u : EnergyField) (t x : ℝ) : ℂ :=
  ∫ s : ℝ in Set.Iic t, memoryIntegrand M u t x s

/-- The causal memory integral is genuinely integrable, so the total Bochner
integral cannot use its non-integrable fallback value. -/
def MemoryTermDefined (M : Medium) (u : EnergyField) : Prop :=
  ∀ t,
    AEStronglyMeasurable (memoryTerm M u t) volume ∧
      ∀ᵐ x : ℝ,
        Integrable (memoryIntegrand M u t x) (volume.restrict (Set.Iic t))

/-- The weak spacetime integrand for equation (1.1):
`D_t^2 u - a K(D_t u) - D_x^2 u = 0`.
One integration by parts gives the first two derivative terms below. -/
def weakTimeIntegrand (M : Medium) (u : EnergyField)
    (phi : ℝ × ℝ → ℂ) (p : ℝ × ℝ) : ℂ :=
  u.timeDerivative p.1 p.2 * testTimeDerivative phi p -
    u.spaceDerivative p.1 p.2 * testSpaceDerivative phi p -
    M.coefficient p.2 p.1 * memoryTerm M u p.1 p.2 * phi p

/-- The weak form of the actual time-domain equation (1.1). -/
def SatisfiesWeakTimeEquation (M : Medium) (u : EnergyField) : Prop :=
  MemoryTermDefined M u ∧
    ∀ phi : ℝ × ℝ → ℂ, IsSpaceTimeTestFunction phi →
      Integrable (weakTimeIntegrand M u phi) ∧
        (∫ p : ℝ × ℝ, weakTimeIntegrand M u phi p) = 0

/-- Absolute integrability of the Fourier--Laplace integral at every
upper-half-plane frequency. -/
def HasFourierLaplaceTransform (g : TimeSignal) : Prop :=
  ∀ z, z ∈ upperHalfPlane →
    Integrable (fun t : ℝ => Complex.exp (Complex.I * z * (t : ℂ)) * g t)

/-- The source's Fourier transform, canonically zero-extended away from the
upper half-plane. -/
noncomputable def fourierLaplace (g : TimeSignal) : FrequencySignal := by
  classical
  refine ⟨fun z => if hz : z ∈ upperHalfPlane then
      ∫ t : ℝ, Complex.exp (Complex.I * z * (t : ℂ)) * g t
    else 0, ?_⟩
  intro z hz
  simp [hz]

/-- The time data in Theorem 1.2: `C_c^infinity((R,infinity))`. -/
def AdmissibleTimeDatum (M : Medium) (g : TimeSignal) : Prop :=
  ContDiff ℝ ⊤ g ∧ HasCompactSupport g ∧
    tsupport g ⊆ Set.Ioi M.spatialRadius ∧
    HasFourierLaplaceTransform g

/-- A causal finite-energy solution with incoming past datum `g`. -/
def IsCausalEnergySolution (M : Medium) (g : TimeSignal) (u : EnergyField) : Prop :=
  SatisfiesWeakTimeEquation M u ∧
    ∀ t, t < 0 → ∀ x, u.value t x = g (t - x)

/-- The exact travelling-wave identities in (1.7). -/
def HasTimeExteriorData (M : Medium) (incoming reflected transmitted : TimeSignal)
    (u : EnergyField) : Prop :=
  ∀ t x,
    (x < -M.spatialRadius →
      u.value t x = incoming (t - x) + reflected (t + x)) ∧
    (M.spatialRadius < x → u.value t x = transmitted (t - x))

/-- Equality of energy solutions modulo the standard almost-everywhere
representative ambiguity, including both weak derivatives. -/
def EnergyEquivalent (u v : EnergyField) : Prop :=
  ∀ t,
    u.value t =ᵐ[volume] v.value t ∧
    u.timeDerivative t =ᵐ[volume] v.timeDerivative t ∧
    u.spaceDerivative t =ᵐ[volume] v.spaceDerivative t

/-! ## Mapping and Fourier-intertwining properties -/

/-- One frequency operator has the source's bounded mapping property at every
Hardy weight.  The same operator is used for all `alpha`. -/
def GradedBounded (shift : ℝ)
    (L : FrequencySignal →ₗ[ℂ] FrequencySignal) : Prop :=
  ∀ alpha : ℝ, ∃ C : ℝ≥0∞, C < ⊤ ∧
    ∀ f : FrequencySignal, MemIncomingHardy alpha f →
      MemOutgoingHardy (alpha + shift) (L f) ∧
        hardySqNorm (alpha + shift) (outgoingLift (L f)) ≤
          C * hardySqNorm alpha (incomingLift f)

/-- The time operator is the Fourier realization of the frequency operator
on every source datum.  Integrability of the output transform is included
explicitly. -/
def FourierIntertwines (M : Medium)
    (frequencyOp : FrequencySignal →ₗ[ℂ] FrequencySignal)
    (timeOp : TimeSignal →ₗ[ℂ] TimeSignal) : Prop :=
  ∀ g : TimeSignal, AdmissibleTimeDatum M g →
    HasFourierLaplaceTransform (timeOp g) ∧
      ∀ z, z ∈ upperHalfPlane →
        (fourierLaplace (timeOp g)).1 z = (frequencyOp (fourierLaplace g)).1 z

end ScatteringInterfaces

/-! ## The complete source proposition, published before the open goal -/

namespace ScatteringMain

open ScatteringInterfaces

/-- The conclusions of Theorems 1.1 and 1.2 at one exterior cutoff `R1`.

The transmission/reflection pair is chosen before the Hardy weight, so the
same two operators work simultaneously for every `alpha`.  Uniqueness of weak
and energy solutions is stated modulo their natural almost-everywhere
equivalences rather than equality of arbitrary representatives. -/
def OperatorValuedScatteringAt (M : Medium) (R1 : ℝ) : Prop :=
  M.spatialRadius < R1 →
    ∃ (transmission reflection : FrequencySignal →ₗ[ℂ] FrequencySignal)
        (timeTransmission timeReflection : TimeSignal →ₗ[ℂ] TimeSignal),
      GradedBounded (2 * R1) transmission ∧
      GradedBounded (2 * R1) reflection ∧
      (∀ (alpha : ℝ) (f : FrequencySignal), MemIncomingHardy alpha f →
        ∃ u : FrequencyField,
          IsWeakFrequencySolution M u ∧
          HasFrequencyExteriorData M f (reflection f) (transmission f) u ∧
          ∀ u' : FrequencyField,
            IsWeakFrequencySolution M u' →
            HasFrequencyExteriorData M f (reflection f) (transmission f) u' →
            FrequencyEquivalent u' u) ∧
      FourierIntertwines M transmission timeTransmission ∧
      FourierIntertwines M reflection timeReflection ∧
      (∀ g : TimeSignal, AdmissibleTimeDatum M g →
        ∃ u : EnergyField,
          IsCausalEnergySolution M g u ∧
          HasTimeExteriorData M g (timeReflection g) (timeTransmission g) u ∧
          ∀ u' : EnergyField,
            IsCausalEnergySolution M g u' → EnergyEquivalent u' u)

/-- Every cutoff strictly larger than the coefficient's spatial support radius
admits one common scattering pair with all frequency/time properties. -/
def OperatorValuedScatteringProblem (M : Medium) : Prop :=
  ∀ R1 : ℝ, OperatorValuedScatteringAt M R1

end ScatteringMain

Source

Jeffrey Galkowski and Maciej Zworski, 1D Scattering Through Time Dependent Media with Memory (with an appendix by Zhen Huang and Maciej Zworski), Discrete and Continuous Dynamical Systems 58 (2027), 111–135, Theorems 1.1–1.2 and equations (1.1)–(1.7), journal pp. 111–113: https://doi.org/10.3934/dcds.2026144

Read-back

What the Lean code literally says, in plain math · gpt-5.6-sol

Definitions.ScatteringInterfaces / definition bundle

ScatteringInterfaces.SupportedInRectangle. For a function $a:\mathbb R\to\mathbb R\to\mathbb C$ and real numbers $R,T$ , this proposition says that for every $x,t\in\mathbb R$ , if $R<|x|$ or $T<|t|$ , then $a(x,t)=0$ . The definition itself does not require $R$ or $T$ to be nonnegative; a negative radius can therefore force $a$ to vanish everywhere.

ScatteringInterfaces.UniformlyTimeSmooth. For every fixed $x$ , the function $t\mapsto a(x,t)$ is infinitely continuously differentiable over $\mathbb R$ ; additionally, for every derivative order $k\in\mathbb N$ , there exists a real $C\ge0$ , depending on $k$ but not on $x$ or $t$ , such that $‖a_x^{(k)}(t)‖\le C$ for every $x,t\in\mathbb R$ . It imposes no spatial differentiability.

ScatteringInterfaces.SpatiallyMeasurable. For every $t\in\mathbb R$ , the function $x\mapsto a(x,t)$ is strongly measurable.

ScatteringInterfaces.Medium. A medium consists of a coefficient $a:\mathbb R\to\mathbb R\to\mathbb C$ , real numbers $R,T,\gamma$ , proofs that $R,T,\gamma>0$ , the assertion that $a(x,t)=0$ whenever $R<|x|$ or $T<|t|$ , strong measurability of every spatial slice $x\mapsto a(x,t)$ , and uniform time smoothness as just defined. No spatial smoothness, reality, sign, symmetry, or nonzeroness condition is imposed on $a$ .

ScatteringInterfaces.freeMedium. This is the particular medium with coefficient identically zero and $R=T=\gamma=1$ , together with the required support, measurability, and smoothness witnesses. Thus the type of media is inhabited.

ScatteringInterfaces.upperHalfPlane. This is the set of complex numbers $z$ satisfying $\operatorname{Im}z>0$ .

ScatteringInterfaces.upperFunctionSubmodule. This is the complex submodule of all functions $f:\mathbb C\to\mathbb C$ such that $f(z)=0$ whenever $\operatorname{Im}z\le0$ . Membership alone imposes no holomorphy, measurability, integrability, or boundary regularity on the values in the upper half-plane.

ScatteringInterfaces.FrequencySignal, FrequencyField, TimeSignal, and TimeField. A frequency signal is an element of the preceding submodule; a frequency field is a function assigning such a signal to each $x\in\mathbb R$ ; a time signal is any function $\mathbb R\to\mathbb C$ ; and a time field is any function $\mathbb R\to\mathbb R\to\mathbb C$ , with time as the first argument.

ScatteringInterfaces.verticalPoint. Given a positive real $\sigma$ and $\xi\in\mathbb R$ , this is $\xi+i\sigma$ . The positivity of $\sigma$ is carried as part of its subtype.

ScatteringInterfaces.verticalPoint_mem. For every positive $\sigma$ and every real $\xi$ , $\xi+i\sigma$ belongs to the open upper half-plane.

ScatteringInterfaces.verticalHardyEnergy. For $\alpha\in\mathbb R$ , a frequency signal $f$ , and $\sigma>0$ , this is the extended nonnegative number

e^{-2\sigma\alpha}\int_{\mathbb R}|f(\xi+i\sigma)|^2\,d\xi.

It is defined using a nonnegative extended integral, so it may equal $+\infty$ .

ScatteringInterfaces.hardySqNorm. This is the supremum of the preceding energy over every $\sigma>0$ :

\sup_{\sigma>0}e^{-2\sigma\alpha}\int_{\mathbb R}|f(\xi+i\sigma)|^2\,d\xi.

Neither the boundary line $\sigma=0$ nor any single preferred height is used.

ScatteringInterfaces.MemHardy. A signal $f$ belongs at weight $\alpha$ exactly when $f$ is complex differentiable at every point of the open upper half-plane and its preceding squared Hardy norm is strictly less than $+\infty$ .

ScatteringInterfaces.incomingLift and outgoingLift. The incoming lift of $f$ is the frequency signal $z\mapsto(z+i)f(z)$ , and the outgoing lift is $z\mapsto zf(z)$ . Both remain zero off the upper half-plane because $f$ does.

ScatteringInterfaces.MemIncomingHardy and MemOutgoingHardy. The incoming condition at weight $\alpha$ means that $z\mapsto(z+i)f(z)$ is holomorphic in the upper half-plane and has finite squared Hardy norm there. The outgoing condition means the same for $z\mapsto zf(z)$ . The definitions assert membership through multiplication; they do not literally divide by $z+i$ or $z$ .

ScatteringInterfaces.localVerticalEnergy. For a frequency field $u$ , real radius $r$ , weight $\alpha$ , and $\sigma>0$ , this is

e^{-2\sigma\alpha}\int_{\mathbb R}\int_{[-r,r]} |(\xi+i\sigma)u(x,\xi+i\sigma)|^2\,dx\,d\xi

as an extended nonnegative number. If $r<0$ , the interval $[-r,r]$ is empty; if $r=0$ , it is a Lebesgue-null singleton, so this quantity is zero in the usual measurable cases.

ScatteringInterfaces.localHardySqNorm. This is the supremum of the local vertical energy over all $\sigma>0$ .

ScatteringInterfaces.FrequencyLocal. A frequency field $u$ is local exactly when: for every $x$ , $z\mapsto u(x,z)$ is holomorphic on the upper half-plane; for every upper-half-plane $z$ , $x\mapsto u(x,z)$ is almost-everywhere strongly measurable; and there exists one real weight $\alpha$ such that, for every real $r>0$ , the local squared Hardy norm on $[-r,r]$ is finite. The same existentially chosen $\alpha$ must work for all positive radii, but it need not be any externally supplied weight; no global spatial norm is required.

ScatteringInterfaces.coefficientFourier. For a medium $M$ , this is

\widehat a_M(x,\xi)=\int_{\mathbb R}e^{i\xi t}a(x,t)\,dt,

with no normalization factor.

ScatteringInterfaces.memoryMultiplier. This is $m_M(z)=z/(z+i\gamma)$ , where $\gamma$ is the medium’s positive memory-decay field. Complex division is total; at the otherwise singular input $z=-i\gamma$ , its value is $0$ . In applications to an upper horizontal line, the denominator has positive imaginary part and is nonzero.

ScatteringInterfaces.frequencyActionIntegrand. Given $M,u,x,z$ and a real integration variable $\xi$ , put $w=\xi+i\operatorname{Im}z$ . The integrand is

\widehat a_M(x,\operatorname{Re}z-\xi)\,m_M(w)\,u(x,w).

It uses $z$ only through its real and imaginary parts and samples $u$ on the horizontal line through $z$ .

ScatteringInterfaces.frequencyAction. This is

(A_Mu)(x,z)=\frac1{2\pi}\int_{\mathbb R} \widehat a_M(x,\operatorname{Re}z-\xi)m_M(\xi+i\operatorname{Im}z) u(x,\xi+i\operatorname{Im}z)\,d\xi.

The Bochner integral is a total function and therefore takes its fallback value $0$ if the integrand is not integrable; the next predicate rules this out only almost everywhere in $x$ on upper-half-plane slices.

ScatteringInterfaces.FrequencyActionDefined. For every $z$ in the upper half-plane, $x\mapsto(A_Mu)(x,z)$ must be almost-everywhere strongly measurable, and for almost every $x$ , the frequency-action integrand must be Bochner integrable as a function of $\xi$ . It does not require frequency integrability at every $x$ , or anything for $z$ outside the upper half-plane.

ScatteringInterfaces.IsSpatialTestFunction. A spatial test function is a complex-valued function on $\mathbb R$ that is infinitely continuously differentiable and has compact support. The zero function is allowed.

ScatteringInterfaces.weakFrequencyIntegrand. For $M,u,z,\phi,x$ , this is

-u(x,z)\phi''(x)-z^2u(x,z)\phi(x)+(A_Mu)(x,z)\phi(x),

where the second derivative is the iterated real derivative of $\phi$ .

ScatteringInterfaces.IsWeakFrequencySolution. A frequency field $u$ must be FrequencyLocal, its frequency action must be defined in the preceding almost-everywhere sense, and for every upper-half-plane $z$ and every smooth compactly supported $\phi$ , the weak-frequency integrand must be integrable over $x$ and have integral zero. This is solely a weak equation; exterior identities are not part of this predicate. The zero field satisfies these conditions for every medium.

ScatteringInterfaces.HasFrequencyExteriorData. For every real $x$ and every upper-half-plane $z$ , if $x<-R$ then

u(x,z)=f_{\rm in}(z)e^{izx}+f_{\rm refl}(z)e^{-izx},

and if $R<x$ then

u(x,z)=f_{\rm trans}(z)e^{izx},

where $R$ is the medium’s spatial radius. Both implications must hold as a conjunction. Nothing is asserted at $x=\pm R$ or for $-R<x<R$ .

ScatteringInterfaces.FrequencyEquivalent. Two frequency fields are equivalent when, for every fixed upper-half-plane $z$ , their spatial slices agree almost everywhere in $x$ . The exceptional null set may depend on $z$ ; no single joint null set is required.

ScatteringInterfaces.IsSpaceTimeTestFunction. A spacetime test function $\phi:\mathbb R^2\to\mathbb C$ is infinitely continuously differentiable over $\mathbb R$ and compactly supported.

ScatteringInterfaces.testTimeDerivative and testSpaceDerivative. At $p=(t,x)$ , these are respectively the ordinary derivative at $t$ of $s\mapsto\phi(s,x)$ , and the derivative at $x$ of $y\mapsto\phi(t,y)$ . The derivative operator itself is total, but every use in the weak laws is under the smooth-test hypothesis.

ScatteringInterfaces.IsWeakTimeDerivative. A candidate $d_tu$ is a weak time derivative of $u$ when, for every smooth compactly supported spacetime test $\phi$ , both $d_tu\,\phi$ and $u\,\partial_t\phi$ are integrable on $\mathbb R^2$ , and

\int_{\mathbb R^2}d_tu\,\phi=-\int_{\mathbb R^2}u\,\partial_t\phi.

ScatteringInterfaces.IsWeakSpaceDerivative. A candidate $d_xu$ is a weak space derivative when the analogous two integrability conditions hold and

\int_{\mathbb R^2}d_xu\,\phi=-\int_{\mathbb R^2}u\,\partial_x\phi.

ScatteringInterfaces.l2SqDistance. For arbitrary $f,g:\mathbb R\to\mathbb C$ , this is the extended nonnegative integral

\int_{\mathbb R}|f(x)-g(x)|^2\,dx,

which may be $+\infty$ .

ScatteringInterfaces.EnergyField. An energy field contains a value $u(t,x)$ , a named time derivative $u_t(t,x)$ , and a named space derivative $u_x(t,x)$ . The named fields must satisfy the two global weak-derivative laws above. For every fixed $t$ , all three spatial slices are almost-everywhere strongly measurable and have finite squared $L^2_x$ integrals. At every $t_0$ , the sum of the squared $L^2$ distances from $u(t)$ to $u(t_0)$ and from $u_x(t)$ to $u_x(t_0)$ tends to zero as $t\to t_0$ ; separately, the squared $L^2$ distance from $u_t(t)$ to $u_t(t_0)$ tends to zero. No pointwise continuity or second derivative is included.

ScatteringInterfaces.memoryIntegrand. For $s,t,x\in\mathbb R$ , this is

e^{-\gamma(t-s)}\bigl(-i\,u_t(s,x)\bigr).

ScatteringInterfaces.memoryTerm. This is the Bochner integral

K_Mu(t,x)=\int_{s\le t}e^{-\gamma(t-s)}\bigl(-i\,u_t(s,x)\bigr)\,ds.

As a raw definition it has the Bochner integral’s zero fallback at nonintegrable inputs.

ScatteringInterfaces.MemoryTermDefined. For every $t$ , $x\mapsto K_Mu(t,x)$ is almost-everywhere strongly measurable, and for almost every $x$ , the memory integrand is integrable in $s$ with respect to Lebesgue measure restricted to $(-\infty,t]$ . Integrability is not demanded at every $x$ .

ScatteringInterfaces.weakTimeIntegrand. At $p=(t,x)$ , this is

u_t(t,x)\partial_t\phi(t,x)-u_x(t,x)\partial_x\phi(t,x) -a(x,t)K_Mu(t,x)\phi(t,x).

ScatteringInterfaces.SatisfiesWeakTimeEquation. The memory term must be defined in the preceding sense, and for every smooth compactly supported spacetime test $\phi$ , the weak-time integrand must be integrable on $\mathbb R^2$ and have integral zero.

ScatteringInterfaces.HasFourierLaplaceTransform. A time signal $g$ has this property when, for every $z$ with $\operatorname{Im}z>0$ , the function $t\mapsto e^{izt}g(t)$ is Bochner integrable on $\mathbb R$ .

ScatteringInterfaces.fourierLaplace. This is the frequency signal

\widehat g(z)= \begin{cases} \int_{\mathbb R}e^{izt}g(t)\,dt,&\operatorname{Im}z>0,\\ 0,&\operatorname{Im}z\le0. \end{cases}

Without a separate integrability hypothesis, the upper-half-plane Bochner integral can itself take its zero fallback.

ScatteringInterfaces.AdmissibleTimeDatum. A time signal $g$ is admissible for $M$ when it is infinitely continuously differentiable, has compact support, its topological support is contained in the strict ray $(R,\infty)$ , and it has the preceding transform at every upper-half-plane frequency. Here $R$ is the medium’s spatial radius. Nonzeroness is not required; $g=0$ is admissible.

ScatteringInterfaces.IsCausalEnergySolution. An energy field $u$ must satisfy the weak time equation and, pointwise for every $t<0$ and every $x$ , obey

u(t,x)=g(t-x).

This condition does not say that $u$ itself vanishes for negative $t$ .

ScatteringInterfaces.HasTimeExteriorData. For every $t,x$ , if $x<-R$ then

u(t,x)=g_{\rm in}(t-x)+g_{\rm refl}(t+x),

and if $R<x$ then

u(t,x)=g_{\rm trans}(t-x).

Nothing is imposed at $x=\pm R$ or in the interior strip.

ScatteringInterfaces.EnergyEquivalent. Two energy fields are equivalent when, at every fixed $t$ , their value slices, named time-derivative slices, and named space-derivative slices each agree almost everywhere in $x$ . The three null sets, and the null sets at different times, need not coincide.

ScatteringInterfaces.GradedBounded. Given a real shift $s$ and a complex-linear map $L$ on frequency signals, this says that for every $\alpha\in\mathbb R$ , there exists an extended nonnegative constant $C_\alpha<+\infty$ such that every $f$ satisfying the incoming Hardy condition at $\alpha$ is sent to a signal satisfying the outgoing Hardy condition at $\alpha+s$ , and

\|z(Lf)(z)\|_{H_{\alpha+s}}^2 \le C_\alpha\,\|(z+i)f(z)\|_{H_\alpha}^2.

The same $L$ is used for all $\alpha$ , while $C_\alpha$ may depend on $\alpha$ . Nothing is required for signals outside the indicated incoming class.

ScatteringInterfaces.FourierIntertwines. For a frequency-side complex-linear map $L$ and time-side complex-linear map $L_t$ , this says that for every admissible datum $g$ , $L_tg$ has a Fourier–Laplace transform and, at every upper-half-plane $z$ ,

\widehat{L_tg}(z)=L(\widehat g)(z).

It does not require $L_tg$ to remain smooth, compactly supported, or admissible, and it imposes no transform condition on non-admissible inputs.

ScatteringMain.OperatorValuedScatteringAt. For a medium $M$ and real $R_1$ , this is the implication $R<R_1\Rightarrow\cdots$ . Under that premise, there must exist two complex-linear frequency maps, transmission and reflection, and two complex-linear time maps, time-transmission and time-reflection. Both frequency maps are graded bounded with shift $2R_1$ . For every $\alpha$ and every incoming-Hardy $f$ at $\alpha$ , there exists a weak frequency solution with incoming exterior signal $f$ , reflected signal $\mathrm{reflection}(f)$ , and transmitted signal $\mathrm{transmission}(f)$ ; every other weak frequency solution with those same three exterior signals is frequency-equivalent to it. The transmission and reflection maps Fourier-intertwine with their corresponding time maps. Finally, every admissible $g$ has a causal energy solution whose exterior signals are $g$ , $\mathrm{timeReflection}(g)$ , and $\mathrm{timeTransmission}(g)$ , and every causal energy solution for that $g$ —without an exterior-data hypothesis—is energy-equivalent to it. The four operators are chosen before $\alpha,f,g$ , but may depend on $M$ and $R_1$ ; their uniqueness is not asserted. The exterior identities use $R$ , not $R_1$ . If $R_1\le R$ , the initial implication is true without furnishing any operators.

ScatteringMain.OperatorValuedScatteringProblem. This says that OperatorValuedScatteringAt $M,R_1$ holds for every real $R_1$ . The clauses for $R_1\le R$ are automatic, but because every medium has $R>0$ , the universal quantifier also includes cutoffs $R_1>R$ , where the operator-existence conclusion is required. A different operator quadruple may be chosen for each $R_1$ .

Human review

Flagged by Shuze Chen · Aug 27, 2026
Inconsistent time/frequency pair — goal is false for generic media. In memoryIntegrand the causal kernel is applied to D_t u = −i·∂t u, but under this file's Fourier convention (ĥ(ω) = ∫e^{iωt}h(t)dt) the transform of ∫{−∞}^t e^{−γ(t−s)}(D_t u)(s)ds is −i·ω/(ω+iγ)·û — not the ω/(ω+iγ) used in memoryMultiplier. (Verified symbolically and numerically; the source paper's own (1.1)→(1.2) step is only "at least formally" and carries the same slip — its rigorous model 𝒫 = ∂_t ε ∂_t − ∂_x², eqs. (2.14)–(2.16), has no −i.) Since OperatorValuedScatteringProblem requires one operator pair (T, R₊) to simultaneously solve the frequency problem for P = D_x² − ω² + a(x,D_ω)·ω/(ω+iγ) AND Fourier-intertwine with the time scattering of the stated wave equation, the two clauses pin (T, R₊) to scattering data of two different equations — differing at first Born order by −i whenever reflection is nonzero — so the conjunction fails for generic media. Fix: drop the −Complex.I in memoryIntegrand (the memory acts on ∂_t u); the time equation then Fourier-transforms exactly to the stated P. The goal item's NL needs the matching edit (∂_t u instead of D_t u inside the memory integral).

View graph