Analytic Continuation Framework

theorem FUST.MellinSampling.euler_identity : Complex.exp (↑Real.pi * Complex.I) = -1

noncomputable def FUST.MellinSampling.sincC (z : ℂ) : ℂ

Equations

• FUST.MellinSampling.sincC z = if z = 0 then 1 else Complex.sin (↑Real.pi * z) / (↑Real.pi * z)

theorem FUST.MellinSampling.sincC_zero : sincC 0 = 1

theorem FUST.MellinSampling.sincC_int (n : ℤ) (hn : n ≠ 0) : sincC ↑n = 0

noncomputable def FUST.MellinSampling.frourioRotationOffset : ℝ

Equations

• FUST.MellinSampling.frourioRotationOffset = Real.pi / Real.log FUST.φ

theorem FUST.MellinSampling.frourioRotationOffset_pos : frourioRotationOffset > 0

theorem FUST.MellinSampling.phi_imaginary_rotation : Complex.exp (↑(Real.log φ) * (↑frourioRotationOffset * Complex.I)) = -1

noncomputable def FUST.MellinSampling.complexFrourioTime (x : ℝ) : ℂ

Equations

• FUST.MellinSampling.complexFrourioTime x = ↑(Real.log x / Real.log FUST.φ)

noncomputable def FUST.MellinSampling.rotatedFrourioTime (x : ℝ) : ℂ

Equations

• FUST.MellinSampling.rotatedFrourioTime x = ↑(Real.log x / Real.log FUST.φ) + ↑FUST.MellinSampling.frourioRotationOffset * Complex.I

theorem FUST.MellinSampling.sincC_delta (m n : ℤ) : sincC (↑m - ↑n) = if m = n then 1 else 0

noncomputable def FUST.MellinSampling.sincRecon (a : ℤ → ℂ) (z : ℂ) : ℂ

Equations

• FUST.MellinSampling.sincRecon a z = ∑' (n : ℤ), a n * FUST.MellinSampling.sincC (z - ↑n)

noncomputable def FUST.MellinSampling.phiSincRecon (f : ℂ → ℂ) (x₀ z : ℂ) : ℂ

Equations

• FUST.MellinSampling.phiSincRecon f x₀ z = FUST.MellinSampling.sincRecon (fun (n : ℤ) => FUST.PhiBloch.phiLatticeSample f x₀ n) z

theorem FUST.MellinSampling.sincRecon_eval_int (a : ℤ → ℂ) (m : ℤ) : sincRecon a ↑m = a m

theorem FUST.MellinSampling.sincC_delta_extract_finite (a : ℤ → ℂ) (m : ℤ) (S : Finset ℤ) (hm : m ∈ S) : ∑ n ∈ S, a n * sincC (↑m - ↑n) = a m

theorem FUST.MellinSampling.sincRecon_injective (a b : ℤ → ℂ) (heq : ∀ (m : ℤ), sincRecon a ↑m = sincRecon b ↑m) : a = b

theorem FUST.MellinSampling.sincC_lattice_interpolation : sincC 0 = 1 ∧ ∀ (n : ℤ), n ≠ 0 → sincC ↑n = 0

theorem FUST.MellinSampling.discrete_analytic_bijection (a b : ℤ → ℂ) : (∀ (z : ℂ), sincRecon a z = sincRecon b z) ↔ a = b

theorem FUST.MellinSampling.sincC_even (z : ℂ) : sincC (-z) = sincC z

theorem FUST.MellinSampling.discrete_FE_implies_global_FE (a : ℤ → ℂ) (hdfe : ∀ (n : ℤ), a n = a (1 - n)) (s : ℂ) : sincRecon a s = sincRecon a (1 - s)

def FUST.MellinSampling.IsEntire (h : ℂ → ℂ) : Prop

Equations

• FUST.MellinSampling.IsEntire h = ∀ (z : ℂ), DifferentiableAt ℂ h z

def FUST.MellinSampling.ExponentialType_le_pi (h : ℂ → ℂ) : Prop

Equations

• FUST.MellinSampling.ExponentialType_le_pi h = ∃ C > 0, ∀ (z : ℂ), ‖h z‖ ≤ C * Real.exp (Real.pi * ‖z‖)

def FUST.MellinSampling.SquareIntegrableOnReals (h : ℂ → ℂ) : Prop

Equations

• FUST.MellinSampling.SquareIntegrableOnReals h = MeasureTheory.Integrable (fun (t : ℝ) => ‖h ↑t‖ ^ 2) MeasureTheory.volume

theorem FUST.MellinSampling.sin_pi_mul_eq_zero_iff (z : ℂ) : Complex.sin (↑Real.pi * z) = 0 ↔ ∃ (n : ℤ), z = ↑n

theorem FUST.MellinSampling.cos_pi_int_ne_zero (n : ℤ) : Complex.cos (↑Real.pi * ↑n) ≠ 0

theorem FUST.MellinSampling.sin_pi_deriv_ne_zero (n : ℤ) : ↑Real.pi * Complex.cos (↑Real.pi * ↑n) ≠ 0

theorem FUST.MellinSampling.entire_vanish_int_div_sin (f : ℂ → ℂ) (hf : IsEntire f) (hvan : ∀ (n : ℤ), f ↑n = 0) : ∃ (g : ℂ → ℂ), IsEntire g ∧ ∀ (z : ℂ), f z = Complex.sin (↑Real.pi * z) * g z

theorem FUST.MellinSampling.div_sin_growth (f g : ℂ → ℂ) (hf_type : ExponentialType_le_pi f) (hfg : ∀ (z : ℂ), f z = Complex.sin (↑Real.pi * z) * g z) : ∃ C > 0, ∀ (z : ℂ), |z.im| ≥ 1 → ‖g z‖ ≤ C * Real.exp (Real.pi * |z.re|)

theorem FUST.MellinSampling.sin_const_not_L2 (c : ℂ) (hc : c ≠ 0) : ¬MeasureTheory.Integrable (fun (t : ℝ) => ‖Complex.sin (↑Real.pi * ↑t) * c‖ ^ 2) MeasureTheory.volume

FE Preservation and Zero Pairing under Bandlimiting

def FUST.MellinSampling.FunctionalEquation (f : ℂ → ℂ) : Prop

Equations

• FUST.MellinSampling.FunctionalEquation f = ∀ (s : ℂ), f s = f (1 - s)

def FUST.MellinSampling.RealOnCriticalLine (f : ℂ → ℂ) : Prop

Equations

• FUST.MellinSampling.RealOnCriticalLine f = ∀ (t : ℝ), (f (1 / 2 + ↑t * Complex.I)).im = 0

def FUST.MellinSampling.EvenMellinSpectrum (fhat : ℝ → ℂ) : Prop

Equations

• FUST.MellinSampling.EvenMellinSpectrum fhat = Function.Even fhat

theorem FUST.MellinSampling.bandlimit_preserves_even (fhat : ℝ → ℂ) (omegaN : ℝ) (heven : EvenMellinSpectrum fhat) : EvenMellinSpectrum fun (ω : ℝ) => if |ω| ≤ omegaN then fhat ω else 0

theorem FUST.MellinSampling.functional_equation_zero_pair (g : ℂ → ℂ) (hFE : FunctionalEquation g) (s : ℂ) (hs : g s = 0) : g (1 - s) = 0

theorem FUST.MellinSampling.critical_line_pair (s : ℂ) (hre : s.re = 1 / 2) : (1 - s).re = 1 / 2

theorem FUST.MellinSampling.off_line_distinct (s : ℂ) (hre : s.re ≠ 1 / 2) : s ≠ 1 - s

theorem FUST.MellinSampling.critical_line_zero_re (t₀ : ℝ) : (1 / 2 + ↑t₀ * Complex.I).re = 1 / 2

theorem FUST.MellinSampling.re_half_from_FE_uniqueness (g : ℂ → ℂ) : FunctionalEquation g → ∀ (rho_tilde : ℂ), g rho_tilde = 0 → ∀ (hself : rho_tilde = 1 - rho_tilde), rho_tilde.re = 1 / 2

structure FUST.MellinSampling.BandlimitedZeroStructure : Type

• g : ℂ → ℂ
• g_FE : FunctionalEquation self.g
• g_real : RealOnCriticalLine self.g
• G : ℝ → ℝ
• G_eq (t : ℝ) : ↑(self.G t) = self.g (1 / 2 + ↑t * Complex.I)
• zero_pair (s : ℂ) : self.g s = 0 → self.g (1 - s) = 0
• re_half (t₀ : ℝ) : self.G t₀ = 0 → (1 / 2 + ↑t₀ * Complex.I).re = 1 / 2

def FUST.MellinSampling.mkBandlimitedZeroStructure (g : ℂ → ℂ) (G : ℝ → ℝ) (hFE : FunctionalEquation g) (hreal : RealOnCriticalLine g) (hG : ∀ (t : ℝ), ↑(G t) = g (1 / 2 + ↑t * Complex.I)) : BandlimitedZeroStructure

Equations

• FUST.MellinSampling.mkBandlimitedZeroStructure g G hFE hreal hG = { g := g, g_FE := hFE, g_real := hreal, G := G, G_eq := hG, zero_pair := ⋯, re_half := ⋯ }

def FUST.MellinSampling.SpectrallyFiltered (f g : ℂ → ℂ) : Prop

Equations

• FUST.MellinSampling.SpectrallyFiltered f g = ∀ (s : ℂ), ∃ (fBL : ℂ) (fperp : ℂ), f s = fBL + fperp ∧ g s = fBL

theorem FUST.MellinSampling.spectral_trivial_zeros (f g : ℂ → ℂ) : SpectrallyFiltered f g → ∀ (s : ℂ) (hf : f s = 0) (hg : g s ≠ 0), f s - g s ≠ 0

def FUST.MellinSampling.ZeroSet (g : ℂ → ℂ) : Set ℂ

Equations

• FUST.MellinSampling.ZeroSet g = {s : ℂ | g s = 0}

def FUST.MellinSampling.DiscreteZeroSet (a : ℤ → ℂ) : Set ℤ

Equations

• FUST.MellinSampling.DiscreteZeroSet a = {n : ℤ | a n = 0}

def FUST.MellinSampling.CriticalLineZeroSet (g : ℂ → ℂ) : Set ℝ

Equations

• FUST.MellinSampling.CriticalLineZeroSet g = {t : ℝ | g (1 / 2 + ↑t * Complex.I) = 0}

theorem FUST.MellinSampling.discreteZeroSet_countable (a : ℤ → ℂ) : (DiscreteZeroSet a).Countable

theorem FUST.MellinSampling.zeroSet_FE_symm (g : ℂ → ℂ) (hFE : FunctionalEquation g) (s : ℂ) : s ∈ ZeroSet g ↔ 1 - s ∈ ZeroSet g

theorem FUST.MellinSampling.discreteZero_to_continuousZero (a : ℤ → ℂ) (m : ℤ) (hm : m ∈ DiscreteZeroSet a) : ↑m ∈ ZeroSet (sincRecon a)

theorem FUST.MellinSampling.continuousZero_to_discreteZero (a : ℤ → ℂ) (m : ℤ) (hm : ↑m ∈ ZeroSet (sincRecon a)) : m ∈ DiscreteZeroSet a

theorem FUST.MellinSampling.zeroSet_int_iff_discreteZeroSet (a : ℤ → ℂ) (m : ℤ) : ↑m ∈ ZeroSet (sincRecon a) ↔ m ∈ DiscreteZeroSet a

theorem FUST.MellinSampling.nonzero_sample_preserved (a : ℤ → ℂ) (m : ℤ) (hm : a m ≠ 0) : sincRecon a ↑m ≠ 0

theorem FUST.MellinSampling.discrete_zero_lifts_to_continuous (a : ℤ → ℂ) (m : ℤ) (hm : m ∈ DiscreteZeroSet a) : ∃ ρ ∈ ZeroSet (sincRecon a), ρ.re = ↑m

theorem FUST.MellinSampling.continuous_integer_zero_projects (a : ℤ → ℂ) (m : ℤ) (hm : ↑m ∈ ZeroSet (sincRecon a)) : ∃ n ∈ DiscreteZeroSet a, (↑m).re = ↑n

theorem FUST.MellinSampling.re_projection_correspondence (a : ℤ → ℂ) : (fun (ρ : ℂ) => ρ.re) '' (ZeroSet (sincRecon a) ∩ Set.range fun (m : ℤ) => ↑m) = (fun (m : ℤ) => ↑m) '' DiscreteZeroSet a

theorem FUST.MellinSampling.sincC_zeroSet_infinite : (ZeroSet sincC).Infinite

theorem FUST.MellinSampling.entire_zeros_isolated (g : ℂ → ℂ) (h_entire : IsEntire g) (h_nz : ∃ (z₀ : ℂ), g z₀ ≠ 0) (z : ℂ) : g z = 0 → ∀ᶠ (w : ℂ) in nhdsWithin z {z}ᶜ, g w ≠ 0

theorem FUST.MellinSampling.entire_zeroSet_isDiscrete (g : ℂ → ℂ) (h_entire : IsEntire g) (h_nz : ∃ (z₀ : ℂ), g z₀ ≠ 0) : IsDiscrete (ZeroSet g)

theorem FUST.MellinSampling.entire_zeroSet_isClosed (g : ℂ → ℂ) (h_entire : IsEntire g) : IsClosed (ZeroSet g)

theorem FUST.MellinSampling.zeroSet_inter_ball_finite (g : ℂ → ℂ) (h_entire : IsEntire g) (h_nz : ∃ (z₀ : ℂ), g z₀ ≠ 0) (n : ℕ) : (ZeroSet g ∩ Metric.closedBall 0 ↑n).Finite

theorem FUST.MellinSampling.entire_zeroSet_countable (g : ℂ → ℂ) (h_entire : IsEntire g) (h_nz : ∃ (z : ℂ), g z ≠ 0) : (ZeroSet g).Countable

Mellin-Poisson Aliasing Structure

noncomputable def FUST.MellinSampling.aliasedSpectrum (fhat : ℝ → ℂ) (T ω : ℝ) : ℂ

Equations

• FUST.MellinSampling.aliasedSpectrum fhat T ω = ∑' (k : ℤ), fhat (ω + ↑k * T)

theorem FUST.MellinSampling.aliasing_preserves_even (fhat : ℝ → ℂ) (T : ℝ) (heven : ∀ (ω : ℝ), fhat (-ω) = fhat ω) (ω : ℝ) : aliasedSpectrum fhat T (-ω) = aliasedSpectrum fhat T ω

Discrete Rotation Representation

theorem FUST.MellinSampling.psi_on_phi_lattice (n k : ℤ) (x₀ : ℝ) : ψ ^ k * (φ ^ n * x₀) = (-1) ^ k * (φ ^ (n - k) * x₀)

theorem FUST.MellinSampling.rotation_parity (k : ℤ) (hk : Odd k) (n : ℤ) (x₀ : ℝ) : ψ ^ k * (φ ^ n * x₀) = -(φ ^ (n - k) * x₀)

theorem FUST.MellinSampling.shift_parity (k : ℤ) (hk : Even k) (n : ℤ) (x₀ : ℝ) : ψ ^ k * (φ ^ n * x₀) = φ ^ (n - k) * x₀

theorem FUST.MellinSampling.dual_probe (f : ℝ → ℝ) (n : ℤ) (x₀ : ℝ) : f (ψ ^ 1 * (φ ^ n * x₀)) = f (-(φ ^ (n - 1) * x₀)) ∧ f (ψ ^ 2 * (φ ^ n * x₀)) = f (φ ^ (n - 2) * x₀) ∧ f (ψ ^ 3 * (φ ^ n * x₀)) = f (-(φ ^ (n - 3) * x₀))