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

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