ExactModulusRecovery #
ExactModulusRecovery #
WIP scaffold for the STFT/ambiguity bridge, exposing the finite-facing corollary needed by downstream modules.
WIP phase-space API stubs #
These declarations freeze the proof-facing objects from the exact-modulus
The definitions are only placeholders; the theorem statements below
are the real work items needed to replace
coeff_kernel_of_exact_modulus_recovery_skappa_ae_wip.
theorem
DimdPolyLEAN.realHermiteGenerating_hasDerivAt
(t : ℝ)
(u : ℂ)
:
HasDerivAt (realHermiteGenerating t) ((↑√2 * ↑t - u) * realHermiteGenerating t u) u
theorem
DimdPolyLEAN.realHermiteGenerating_integral_shift_mul_modulated_completed
(u v : ℂ)
(x ω : ℝ)
:
theorem
DimdPolyLEAN.realHermiteGenerating_stft_integral_kernel
(x ω : ℝ)
(u v : ℂ)
:
∫ (t : ℝ), realHermiteGenerating t u * realHermiteGenerating (t - x) v * Complex.exp (-(2 * ↑Real.pi) * Complex.I * (↑ω * ↑t)) = Complex.exp (-↑Real.pi * Complex.I * (↑x * ↑ω)) * Complex.exp
(u * v + (↑x - 2 * ↑Real.pi * Complex.I * ↑ω) / ↑√2 * u - star ((↑x - 2 * ↑Real.pi * Complex.I * ↑ω) / ↑√2) * v) * ↑(Real.exp (-((x ^ 2 + (2 * Real.pi) ^ 2 * ω ^ 2) / 4)))
theorem
DimdPolyLEAN.realHermiteGenerating_ambiguity_integral_linear_form
(x ω : ℝ)
(u v : ℂ)
:
∫ (t : ℝ), realHermiteGenerating (t + x / 2) u * realHermiteGenerating (t - x / 2) v * Complex.exp (-(2 * ↑Real.pi) * Complex.I * (↑ω * ↑t)) = Complex.exp (-((↑x ^ 2 + (2 * ↑Real.pi) ^ 2 * ↑ω ^ 2) / 4)) * Complex.exp
((↑√2 * ↑x / 2 - ↑√2 * ↑Real.pi * Complex.I * ↑ω) * u - (↑√2 * ↑x / 2 + ↑√2 * ↑Real.pi * Complex.I * ↑ω) * v + u * v)
theorem
DimdPolyLEAN.realHermiteGenerating_ambiguity_integral_kernel
(x ω : ℝ)
(u w : ℂ)
:
∫ (t : ℝ), realHermiteGenerating (t + x / 2) u * realHermiteGenerating (t - x / 2) w * Complex.exp (-(2 * ↑Real.pi) * Complex.I * (↑ω * ↑t)) = Complex.exp
(u * w + (↑x - 2 * ↑Real.pi * Complex.I * ↑ω) / ↑√2 * u - star ((↑x - 2 * ↑Real.pi * Complex.I * ↑ω) / ↑√2) * w) * ↑(Real.exp (-((x ^ 2 + (2 * Real.pi) ^ 2 * ω ^ 2) / 4)))
theorem
DimdPolyLEAN.realHermiteGenerating_ambiguity_integral_conj_raw
(x ω : ℝ)
(u v : ℂ)
:
∫ (t : ℝ), realHermiteGenerating (t + x / 2) u * star (realHermiteGenerating (t - x / 2) v) * Complex.exp (-(2 * ↑Real.pi) * Complex.I * (↑ω * ↑t)) = Complex.exp
(-↑x ^ 2 / 4 + ↑√2 * ↑x * u / 2 - ↑√2 * ↑x * star v / 2 - (u ^ 2 + star v ^ 2) / 2 + (↑√2 * (u + star v) - 2 * ↑Real.pi * Complex.I * ↑ω) ^ 2 / 4)
theorem
DimdPolyLEAN.realHermiteGenerating_ambiguity_integral_conj_kernel
(x ω : ℝ)
(u v : ℂ)
:
∫ (t : ℝ), realHermiteGenerating (t + x / 2) u * star (realHermiteGenerating (t - x / 2) v) * Complex.exp (-(2 * ↑Real.pi) * Complex.I * (↑ω * ↑t)) = Complex.exp
(u * star v + (↑x - 2 * ↑Real.pi * Complex.I * ↑ω) / ↑√2 * u - (↑x + 2 * ↑Real.pi * Complex.I * ↑ω) / ↑√2 * star v) * ↑(Real.exp (-((x ^ 2 + (2 * Real.pi) ^ 2 * ω ^ 2) / 4)))
theorem
DimdPolyLEAN.realHermiteGenerating_ambiguity_integral_independent_kernel
(x ω : ℝ)
(u w : ℂ)
:
∫ (t : ℝ), realHermiteGenerating (t + x / 2) u * realHermiteGenerating (t - x / 2) w * Complex.exp (-(2 * ↑Real.pi) * Complex.I * (↑ω * ↑t)) = Complex.exp
(u * w + (↑x - 2 * ↑Real.pi * Complex.I * ↑ω) / ↑√2 * u - star ((↑x - 2 * ↑Real.pi * Complex.I * ↑ω) / ↑√2) * w) * ↑(Real.exp (-((x ^ 2 + (2 * Real.pi) ^ 2 * ω ^ 2) / 4)))
shiftedGeneratingRightDerivBoundConstant: shifted Generating Right Deriv Bound Constant.
Equations
- One or more equations did not get rendered due to their size.
Instances For
shiftedGeneratingRightDerivBound: shifted Generating Right Deriv Bound.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
DimdPolyLEAN.hasDerivAt_integral_fixed_mul_shifted_modulated_realHermiteGenerating_right_of_bound
(phi : ℝ → ℂ)
(x ω : ℝ)
(w0 : ℂ)
{s : Set ℂ}
{bound : ℝ → ℝ}
(hs : s ∈ nhds w0)
(hF_meas :
∀ᶠ (z : ℂ) in nhds w0, MeasureTheory.AEStronglyMeasurable
(fun (t : ℝ) =>
phi t * realHermiteGenerating (t - 1 / 2 * x) z * Complex.exp (-(2 * ↑Real.pi) * Complex.I * ↑(inner ℝ ω t)))
MeasureTheory.volume)
(hF_int :
MeasureTheory.Integrable
(fun (t : ℝ) =>
phi t * realHermiteGenerating (t - 1 / 2 * x) w0 * Complex.exp (-(2 * ↑Real.pi) * Complex.I * ↑(inner ℝ ω t)))
MeasureTheory.volume)
(hF'_meas :
MeasureTheory.AEStronglyMeasurable
(fun (t : ℝ) =>
phi t * ((↑√2 * ↑(t - 1 / 2 * x) - w0) * realHermiteGenerating (t - 1 / 2 * x) w0) * Complex.exp (-(2 * ↑Real.pi) * Complex.I * ↑(inner ℝ ω t)))
MeasureTheory.volume)
(h_bound :
∀ᵐ (t : ℝ), ∀ z ∈ s,
‖phi t * ((↑√2 * ↑(t - 1 / 2 * x) - z) * realHermiteGenerating (t - 1 / 2 * x) z) * Complex.exp (-(2 * ↑Real.pi) * Complex.I * ↑(inner ℝ ω t))‖ ≤ bound t)
(bound_integrable : MeasureTheory.Integrable bound MeasureTheory.volume)
:
HasDerivAt
(fun (z : ℂ) =>
∫ (t : ℝ), phi t * realHermiteGenerating (t - 1 / 2 * x) z * Complex.exp (-(2 * ↑Real.pi) * Complex.I * ↑(inner ℝ ω t)))
(∫ (t : ℝ), phi t * ((↑√2 * ↑(t - 1 / 2 * x) - w0) * realHermiteGenerating (t - 1 / 2 * x) w0) * Complex.exp (-(2 * ↑Real.pi) * Complex.I * ↑(inner ℝ ω t)))
w0
theorem
DimdPolyLEAN.hasDerivAt_integral_shifted_generating_mul_modulated_right_of_bound
(u w0 : ℂ)
(x ω : ℝ)
{s : Set ℂ}
{bound : ℝ → ℝ}
(hs : s ∈ nhds w0)
(hF_meas :
∀ᶠ (z : ℂ) in nhds w0, MeasureTheory.AEStronglyMeasurable
(fun (t : ℝ) =>
realHermiteGenerating (t + 1 / 2 * x) u * realHermiteGenerating (t - 1 / 2 * x) z * Complex.exp (-(2 * ↑Real.pi) * Complex.I * ↑(inner ℝ ω t)))
MeasureTheory.volume)
(hF_int :
MeasureTheory.Integrable
(fun (t : ℝ) =>
realHermiteGenerating (t + 1 / 2 * x) u * realHermiteGenerating (t - 1 / 2 * x) w0 * Complex.exp (-(2 * ↑Real.pi) * Complex.I * ↑(inner ℝ ω t)))
MeasureTheory.volume)
(hF'_meas :
MeasureTheory.AEStronglyMeasurable
(fun (t : ℝ) =>
realHermiteGenerating (t + 1 / 2 * x) u * ((↑√2 * ↑(t - 1 / 2 * x) - w0) * realHermiteGenerating (t - 1 / 2 * x) w0) * Complex.exp (-(2 * ↑Real.pi) * Complex.I * ↑(inner ℝ ω t)))
MeasureTheory.volume)
(h_bound :
∀ᵐ (t : ℝ), ∀ z ∈ s,
‖realHermiteGenerating (t + 1 / 2 * x) u * ((↑√2 * ↑(t - 1 / 2 * x) - z) * realHermiteGenerating (t - 1 / 2 * x) z) * Complex.exp (-(2 * ↑Real.pi) * Complex.I * ↑(inner ℝ ω t))‖ ≤ bound t)
(bound_integrable : MeasureTheory.Integrable bound MeasureTheory.volume)
:
HasDerivAt
(fun (z : ℂ) =>
∫ (t : ℝ), realHermiteGenerating (t + 1 / 2 * x) u * realHermiteGenerating (t - 1 / 2 * x) z * Complex.exp (-(2 * ↑Real.pi) * Complex.I * ↑(inner ℝ ω t)))
(∫ (t : ℝ), realHermiteGenerating (t + 1 / 2 * x) u * ((↑√2 * ↑(t - 1 / 2 * x) - w0) * realHermiteGenerating (t - 1 / 2 * x) w0) * Complex.exp (-(2 * ↑Real.pi) * Complex.I * ↑(inner ℝ ω t)))
w0
theorem
DimdPolyLEAN.hasDerivAt_integral_shifted_generating_mul_modulated_right_closed
(u w0 : ℂ)
(x ω : ℝ)
:
HasDerivAt
(fun (w : ℂ) =>
∫ (t : ℝ), realHermiteGenerating (t + x / 2) u * realHermiteGenerating (t - x / 2) w * Complex.exp (-(2 * ↑Real.pi) * Complex.I * (↑ω * ↑t)))
((u - star ((↑x - 2 * ↑Real.pi * Complex.I * ↑ω) / ↑√2)) * Complex.exp
(u * w0 + (↑x - 2 * ↑Real.pi * Complex.I * ↑ω) / ↑√2 * u - star ((↑x - 2 * ↑Real.pi * Complex.I * ↑ω) / ↑√2) * w0) * ↑(Real.exp (-((x ^ 2 + (2 * Real.pi) ^ 2 * ω ^ 2) / 4))))
w0
theorem
DimdPolyLEAN.hasDerivAt_integral_shifted_generating_mul_modulated_left_closed
(u0 w : ℂ)
(x ω : ℝ)
:
HasDerivAt
(fun (u : ℂ) =>
∫ (t : ℝ), realHermiteGenerating (t + x / 2) u * realHermiteGenerating (t - x / 2) w * Complex.exp (-(2 * ↑Real.pi) * Complex.I * (↑ω * ↑t)))
((w + (↑x - 2 * ↑Real.pi * Complex.I * ↑ω) / ↑√2) * Complex.exp
(u0 * w + (↑x - 2 * ↑Real.pi * Complex.I * ↑ω) / ↑√2 * u0 - star ((↑x - 2 * ↑Real.pi * Complex.I * ↑ω) / ↑√2) * w) * ↑(Real.exp (-((x ^ 2 + (2 * Real.pi) ^ 2 * ω ^ 2) / 4))))
u0
theorem
DimdPolyLEAN.iteratedDeriv_iteratedDeriv_cexp_mul_at_zero
(m n : ℕ)
:
iteratedDeriv m (fun (w : ℂ) => iteratedDeriv n (fun (u : ℂ) => Complex.exp (u * w)) 0) 0 = if m = n then ↑n.factorial else 0
realHermite1D: real Hermite1 D.
Equations
- DimdPolyLEAN.realHermite1D n t = ↑√↑n.factorial / ↑n.factorial * iteratedDeriv n (DimdPolyLEAN.realHermiteGenerating t) 0
Instances For
theorem
DimdPolyLEAN.complex_monomial_gaussian_memLp
(k : ℕ)
:
MeasureTheory.MemLp (fun (t : ℝ) => ↑t ^ k * Complex.exp (-(↑t ^ 2 / 2))) 2 MeasureTheory.volume
complexMonomialGaussian: complex monomial gaussian.
Equations
- DimdPolyLEAN.complexMonomialGaussian k t = ↑t ^ k * Complex.exp (-(↑t ^ 2 / 2))
Instances For
theorem
DimdPolyLEAN.complex_monomial_gaussian_product_integrable
(k l : ℕ)
:
MeasureTheory.Integrable (fun (t : ℝ) => complexMonomialGaussian k t * complexMonomialGaussian l t) MeasureTheory.volume
theorem
DimdPolyLEAN.complex_monomial_gaussian_product_integral_of_odd
{k l : ℕ}
(hodd : Odd (k + l))
:
theorem
DimdPolyLEAN.complex_monomial_gaussian_product_integral_of_even
{k l : ℕ}
(heven : Even (k + l))
:
∫ (t : ℝ), complexMonomialGaussian k t * complexMonomialGaussian l t = ↑(Real.Gamma ((↑(k + l) + 1) / 2))
theorem
DimdPolyLEAN.complex_monomial_gaussian_finite_bilinear_integrable
(s t : Finset ℕ)
(a b : ℕ → ℂ)
:
MeasureTheory.Integrable
(fun (x : ℝ) => ∑ k ∈ s, ∑ l ∈ t, a k * b l * (complexMonomialGaussian k x * complexMonomialGaussian l x))
MeasureTheory.volume
theorem
DimdPolyLEAN.complex_monomial_gaussian_finite_bilinear_integral_eq_ite
(s t : Finset ℕ)
(a b : ℕ → ℂ)
:
theorem
DimdPolyLEAN.complex_monomial_gaussian_finite_bilinear_integral_eq_even_moments
(s t : Finset ℕ)
(a b : ℕ → ℂ)
(heven : ∀ k ∈ s, ∀ l ∈ t, Even (k + l))
:
∫ (x : ℝ), ∑ k ∈ s, ∑ l ∈ t, a k * b l * (complexMonomialGaussian k x * complexMonomialGaussian l x) = ∑ k ∈ s, ∑ l ∈ t, a k * b l * ↑(Real.Gamma ((↑(k + l) + 1) / 2))
theorem
DimdPolyLEAN.realHermiteGenerating_iteratedDeriv_zero_expansion
(n : ℕ)
(t : ℝ)
:
iteratedDeriv n (realHermiteGenerating t) 0 = ∑ k ∈ Finset.range (n + 1),
↑(Real.pi ^ (-(1 / 4))) * (↑(n.choose k) * ↑√2 ^ k * iteratedDeriv (n - k) (fun (u : ℂ) => Complex.exp (-u ^ 2 / 2)) 0) * (↑t ^ k * Complex.exp (-(↑t ^ 2 / 2)))
theorem
DimdPolyLEAN.realHermiteGeneratingExpansionCoeff_eq_zero_of_odd_sub
{n k : ℕ}
(hodd : Odd (n - k))
:
theorem
DimdPolyLEAN.realHermiteGeneratingExpansionCoeff_eq_zero_of_odd_add
{n k : ℕ}
(hk : k ≤ n)
(hodd : Odd (n + k))
:
standardGaussianMoment: standard Gaussian Moment.
Equations
- DimdPolyLEAN.standardGaussianMoment r = if Even r then ↑(r - 1).doubleFactorial else 0
Instances For
theorem
DimdPolyLEAN.realHermiteGenerating_iteratedDeriv_zero_expansion_monomial
(n : ℕ)
(t : ℝ)
:
iteratedDeriv n (realHermiteGenerating t) 0 = ∑ k ∈ Finset.range (n + 1), realHermiteGeneratingExpansionCoeff n k * complexMonomialGaussian k t
theorem
DimdPolyLEAN.realHermiteGenerating_iteratedDeriv_zero_product_expansion
(n m : ℕ)
(t : ℝ)
:
iteratedDeriv n (realHermiteGenerating t) 0 * iteratedDeriv m (realHermiteGenerating t) 0 = ∑ k ∈ Finset.range (n + 1),
∑ l ∈ Finset.range (m + 1),
realHermiteGeneratingExpansionCoeff n k * realHermiteGeneratingExpansionCoeff m l * (complexMonomialGaussian k t * complexMonomialGaussian l t)
theorem
DimdPolyLEAN.realHermiteGenerating_iteratedDeriv_inner_finite_sum
(n m : ℕ)
:
∫ (t : ℝ), iteratedDeriv n (realHermiteGenerating t) 0 * iteratedDeriv m (realHermiteGenerating t) 0 = ∑ k ∈ Finset.range (n + 1),
∑ l ∈ Finset.range (m + 1),
realHermiteGeneratingExpansionCoeff n k * realHermiteGeneratingExpansionCoeff m l * if Even (k + l) then ↑(Real.Gamma ((↑(k + l) + 1) / 2)) else 0
theorem
DimdPolyLEAN.realHermiteGenerating_iteratedDeriv_inner_eq_zero_of_odd_add
{n m : ℕ}
(hodd : Odd (n + m))
:
∫ (t : ℝ), iteratedDeriv n (realHermiteGenerating t) 0 * iteratedDeriv m (realHermiteGenerating t) 0 = 0
theorem
DimdPolyLEAN.realHermiteGenerating_inner_finite_sum_eq_factorial
(n m : ℕ)
:
(∑ k ∈ Finset.range (n + 1),
∑ l ∈ Finset.range (m + 1),
realHermiteGeneratingExpansionCoeff n k * realHermiteGeneratingExpansionCoeff m l * if Even (k + l) then ↑(Real.Gamma ((↑(k + l) + 1) / 2)) else 0) = if n = m then ↑n.factorial else 0
theorem
DimdPolyLEAN.realHermiteGenerating_iteratedDeriv_inner_eq_factorial
(n m : ℕ)
:
∫ (t : ℝ), iteratedDeriv n (realHermiteGenerating t) 0 * iteratedDeriv m (realHermiteGenerating t) 0 = if n = m then ↑n.factorial else 0
theorem
DimdPolyLEAN.realHermiteGenerating_no_conj_interchange_of_finite_sum
(n m : ℕ)
:
∫ (t : ℝ), iteratedDeriv n (realHermiteGenerating t) 0 * iteratedDeriv m (realHermiteGenerating t) 0 = iteratedDeriv m
(fun (w : ℂ) => iteratedDeriv n (fun (u : ℂ) => ∫ (t : ℝ), realHermiteGenerating t u * realHermiteGenerating t w) 0)
0
theorem
DimdPolyLEAN.realHermiteGenerating_iteratedDeriv_zero_memLp
(n : ℕ)
:
MeasureTheory.MemLp (fun (t : ℝ) => iteratedDeriv n (realHermiteGenerating t) 0) 2 MeasureTheory.volume
theorem
DimdPolyLEAN.realHermite1D_inner_of_iteratedDeriv_inner
(n m : ℕ)
(hderiv :
∫ (t : ℝ), iteratedDeriv n (realHermiteGenerating t) 0 * star (iteratedDeriv m (realHermiteGenerating t) 0) = if n = m then ↑n.factorial else 0)
:
theorem
DimdPolyLEAN.realHermiteGenerating_iteratedDeriv_inner_of_no_conj_interchange
(n m : ℕ)
(hinterchange :
∫ (t : ℝ), iteratedDeriv n (realHermiteGenerating t) 0 * iteratedDeriv m (realHermiteGenerating t) 0 = iteratedDeriv m
(fun (w : ℂ) =>
iteratedDeriv n (fun (u : ℂ) => ∫ (t : ℝ), realHermiteGenerating t u * realHermiteGenerating t w) 0)
0)
:
∫ (t : ℝ), iteratedDeriv n (realHermiteGenerating t) 0 * star (iteratedDeriv m (realHermiteGenerating t) 0) = if n = m then ↑n.factorial else 0
theorem
DimdPolyLEAN.realHermite1D_inner_orthonormal_of_no_conj_interchange
(hinterchange :
∀ (n m : ℕ),
∫ (t : ℝ), iteratedDeriv n (realHermiteGenerating t) 0 * iteratedDeriv m (realHermiteGenerating t) 0 = iteratedDeriv m
(fun (w : ℂ) =>
iteratedDeriv n (fun (u : ℂ) => ∫ (t : ℝ), realHermiteGenerating t u * realHermiteGenerating t w) 0)
0)
(n m : ℕ)
:
theorem
DimdPolyLEAN.realHermite1D_memLp_inner_orthonormal_of_no_conj_interchange
(hmem : ∀ (n : ℕ), MeasureTheory.MemLp (realHermite1D n) 2 MeasureTheory.volume)
(hinterchange :
∀ (n m : ℕ),
∫ (t : ℝ), iteratedDeriv n (realHermiteGenerating t) 0 * iteratedDeriv m (realHermiteGenerating t) 0 = iteratedDeriv m
(fun (w : ℂ) =>
iteratedDeriv n (fun (u : ℂ) => ∫ (t : ℝ), realHermiteGenerating t u * realHermiteGenerating t w) 0)
0)
:
(∀ (n : ℕ), MeasureTheory.MemLp (realHermite1D n) 2 MeasureTheory.volume) ∧ ∀ (n m : ℕ), ∫ (t : ℝ), realHermite1D m t * star (realHermite1D n t) = if n = m then 1 else 0
realHermiteTensorRep: real Hermite Tensor Rep.
Equations
- DimdPolyLEAN.realHermiteTensorRep alpha x = ∏ q : Fin d, DimdPolyLEAN.realHermite1D (alpha q) (x.ofLp q)
Instances For
varphiKappa: varphi Kappa.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
DimdPolyLEAN.bKappaSeriesRep
{d : ℕ}
(kappa : MultiIndex d)
(U : Skappa d kappa)
:
bKappaSeriesRep: b Kappa Series Rep.
Equations
- DimdPolyLEAN.bKappaSeriesRep kappa U x = ∑' (alpha : DimdPolyLEAN.Idx d), DimdPolyLEAN.coeffSkappa U alpha * DimdPolyLEAN.realHermiteTensorRep alpha x
Instances For
noncomputable def
DimdPolyLEAN.bKappa
{d : ℕ}
(kappa : MultiIndex d)
(U : Skappa d kappa)
:
↥(L2Real d)
bKappa: b Kappa.
Equations
- DimdPolyLEAN.bKappa kappa U = ∑' (alpha : DimdPolyLEAN.Idx d), DimdPolyLEAN.coeffSkappa U alpha • DimdPolyLEAN.realHermiteTensorL2 alpha
Instances For
bKappaRep: b Kappa Rep.
Equations
- DimdPolyLEAN.bKappaRep kappa U = ↑↑(DimdPolyLEAN.bKappa kappa U)
Instances For
theorem
DimdPolyLEAN.realHermiteTensorL2_eq_toLp_of_memLp
{d : ℕ}
(alpha : Idx d)
(h : MeasureTheory.MemLp (realHermiteTensorRep alpha) 2 MeasureTheory.volume)
:
theorem
DimdPolyLEAN.realHermiteTensorL2_inner_eq_integral_of_memLp
{d : ℕ}
(alpha beta : Idx d)
(hα : MeasureTheory.MemLp (realHermiteTensorRep alpha) 2 MeasureTheory.volume)
(hβ : MeasureTheory.MemLp (realHermiteTensorRep beta) 2 MeasureTheory.volume)
:
inner ℂ (realHermiteTensorL2 alpha) (realHermiteTensorL2 beta) = ∫ (x : RealVec d), realHermiteTensorRep beta x * star (realHermiteTensorRep alpha x)
theorem
DimdPolyLEAN.realHermiteTensorL2_orthonormal_of_memLp_integral
{d : ℕ}
(hmem : ∀ (alpha : Idx d), MeasureTheory.MemLp (realHermiteTensorRep alpha) 2 MeasureTheory.volume)
(hinner :
∀ (alpha beta : Idx d),
∫ (x : RealVec d), realHermiteTensorRep beta x * star (realHermiteTensorRep alpha x) = if alpha = beta then 1 else 0)
:
Orthonormal ℂ fun (alpha : Idx d) => realHermiteTensorL2 alpha
theorem
DimdPolyLEAN.realHermite1D_memLp_inner_orthonormal :
(∀ (n : ℕ), MeasureTheory.MemLp (realHermite1D n) 2 MeasureTheory.volume) ∧ ∀ (n m : ℕ), ∫ (t : ℝ), realHermite1D m t * star (realHermite1D n t) = if n = m then 1 else 0
theorem
DimdPolyLEAN.realHermiteTensorRep_memLp_of_realHermite1D_memLp
{d : ℕ}
(alpha : Idx d)
(hmem1 : ∀ (n : ℕ), MeasureTheory.MemLp (realHermite1D n) 2 MeasureTheory.volume)
:
theorem
DimdPolyLEAN.realHermiteTensorL2_orthonormal
{d : ℕ}
:
Orthonormal ℂ fun (alpha : Idx d) => realHermiteTensorL2 alpha
theorem
DimdPolyLEAN.varphiKappa_isL2Rep
{d : ℕ}
(kappa : MultiIndex d)
:
IsL2Rep (varphiKappa kappa) (realHermiteTensorRep kappa)
theorem
DimdPolyLEAN.varphiKappa_coe_ae_eq_realHermiteTensorRep
{d : ℕ}
(kappa : MultiIndex d)
:
↑↑(varphiKappa kappa) =ᵐ[MeasureTheory.volume] realHermiteTensorRep kappa
theorem
DimdPolyLEAN.summable_realHermiteTensorL2_coeff_smul_of_orthonormal
{d : ℕ}
(kappa : MultiIndex d)
(horth : Orthonormal ℂ fun (alpha : Idx d) => realHermiteTensorL2 alpha)
(U : Skappa d kappa)
:
Summable fun (alpha : Idx d) => coeffSkappa U alpha • realHermiteTensorL2 alpha
theorem
DimdPolyLEAN.bKappa_coeff_recovery_of_realHermite_orthonormal
{d : ℕ}
(kappa : MultiIndex d)
(horth : Orthonormal ℂ fun (alpha : Idx d) => realHermiteTensorL2 alpha)
(U : Skappa d kappa)
(beta : Idx d)
:
theorem
DimdPolyLEAN.bKappa_injective_of_realHermite_coeff_recovery
{d : ℕ}
(kappa : MultiIndex d)
(hcoeff :
∀ (U : Skappa d kappa) (alpha : Idx d), coeffSkappa U alpha = inner ℂ (realHermiteTensorL2 alpha) (bKappa kappa U))
:
Function.Injective (bKappa kappa)
theorem
DimdPolyLEAN.bKappa_injective_of_realHermite_orthonormal
{d : ℕ}
(kappa : MultiIndex d)
(horth : Orthonormal ℂ fun (alpha : Idx d) => realHermiteTensorL2 alpha)
:
Function.Injective (bKappa kappa)
theorem
DimdPolyLEAN.bKappa_injective
{d : ℕ}
(kappa : MultiIndex d)
:
Function.Injective (bKappa kappa)
phaseSpacePolyEval: phase Space Poly Eval.
Equations
- DimdPolyLEAN.phaseSpacePolyEval ξ (Sum.inl q) = ↑(ξ.1.ofLp q)
- DimdPolyLEAN.phaseSpacePolyEval ξ (Sum.inr q) = ↑(ξ.2.ofLp q)
Instances For
IsPhaseSpacePolynomial: Is Phase Space Polynomial.
Equations
- DimdPolyLEAN.IsPhaseSpacePolynomial P = ∃ (p : MvPolynomial (Fin d ⊕ Fin d) ℂ), ∀ (ξ : DimdPolyLEAN.PhaseSpace d), P ξ = (MvPolynomial.eval (DimdPolyLEAN.phaseSpacePolyEval ξ)) p
Instances For
PKappa: P Kappa.
Equations
- DimdPolyLEAN.PKappa kappa ξ = ((-1) ^ ∑ q : Fin d, kappa q) * DimdPolyLEAN.Phi kappa kappa (DimdPolyLEAN.TKappa ξ)
Instances For
theorem
DimdPolyLEAN.PKappa_isPolynomial
{d : ℕ}
(hd : 0 < d)
(kappa : MultiIndex d)
:
IsPhaseSpacePolynomial (PKappa kappa)
theorem
DimdPolyLEAN.stft_model_modulus
{d : ℕ}
(hd : 0 < d)
(kappa : MultiIndex d)
(U : Skappa d kappa)
(ξ : PhaseSpace d)
:
theorem
DimdPolyLEAN.windowAmbiguity_factorization
{d : ℕ}
(hd : 0 < d)
(kappa : MultiIndex d)
(ξ : PhaseSpace d)
:
theorem
DimdPolyLEAN.windowAmbiguity_polynomial_nonzero
{d : ℕ}
(hd : 0 < d)
(kappa : MultiIndex d)
:
theorem
DimdPolyLEAN.windowAmbiguity_dense_nonvanishing
{d : ℕ}
(hd : 0 < d)
(kappa : MultiIndex d)
:
Dense {ξ : PhaseSpace d | ambiguityRep (varphiKappa kappa) (varphiKappa kappa) ξ ≠ 0}
theorem
DimdPolyLEAN.spectrogram_eq_of_equal_modulus_to_ambiguity_eq
{d : ℕ}
(hd : 0 < d)
(kappa : MultiIndex d)
{f g : ↥(L2Real d)}
(hmod : ∀ (ξ : PhaseSpace d), ‖stftRep (varphiKappa kappa) f ξ‖ = ‖stftRep (varphiKappa kappa) g ξ‖)
(ξ : PhaseSpace d)
:
theorem
DimdPolyLEAN.equalAmbiguity_to_rankOneKernel_ae
{d : ℕ}
{f g : ↥(L2Real d)}
{fRep gRep : RealVec d → ℂ}
(hf_rep : IsL2Rep f fRep)
(hg_rep : IsL2Rep g gRep)
(hAmb : ∀ (ξ : PhaseSpace d), ambiguityRep f f ξ = ambiguityRep g g ξ)
:
theorem
DimdPolyLEAN.rankOneKernel_ae_to_unimodular_phase
{d : ℕ}
{f g : ↥(L2Real d)}
{fRep gRep : RealVec d → ℂ}
(hf_rep : IsL2Rep f fRep)
(hg_rep : IsL2Rep g gRep)
(hkernel :
(fun (p : RealVec d × RealVec d) => fRep p.1 * star (fRep p.2)) =ᵐ[MeasureTheory.volume]
fun (p : RealVec d × RealVec d) => gRep p.1 * star (gRep p.2))
:
theorem
DimdPolyLEAN.ae_modulus_to_stft_modulus
{d : ℕ}
(hd : 0 < d)
(kappa : MultiIndex d)
{U V : Skappa d kappa}
(hmod : (fun (z : Cd d) => ‖toFun kappa U z‖) =ᵐ[gammaD d] fun (z : Cd d) => ‖toFun kappa V z‖)
(ξ : PhaseSpace d)
:
theorem
DimdPolyLEAN.ae_modulus_to_ambiguity_eq
{d : ℕ}
(hd : 0 < d)
(kappa : MultiIndex d)
{U V : Skappa d kappa}
(hmod : (fun (z : Cd d) => ‖toFun kappa U z‖) =ᵐ[gammaD d] fun (z : Cd d) => ‖toFun kappa V z‖)
(ξ : PhaseSpace d)
:
theorem
DimdPolyLEAN.ambiguity_eq_to_skappa_phase
{d : ℕ}
(hd : 0 < d)
(kappa : MultiIndex d)
{U V : Skappa d kappa}
(hAmb :
∀ (ξ : PhaseSpace d),
ambiguityRep (bKappa kappa U) (bKappa kappa U) ξ = ambiguityRep (bKappa kappa V) (bKappa kappa V) ξ)
: