ImportedAnalyticInputs

ImportedAnalyticInputs

Mathlib-facing wrapper file for the analytic inputs that later modules are allowed to cite through a stable local API.

@[reducible, inline]

abbrev DimdPolyLEAN.Circle : Type

Circle: Circle.

Equations

• DimdPolyLEAN.Circle = AddCircle (2 * Real.pi)

noncomputable def DimdPolyLEAN.μCircle : MeasureTheory.Measure Circle

μCircle: the normalized Haar measure on the circle AddCircle (2π).

Equations

• DimdPolyLEAN.μCircle = AddCircle.haarAddCircle

@[reducible, inline]

noncomputable abbrev DimdPolyLEAN.muCircle : MeasureTheory.Measure Circle

muCircle: mu Circle.

Equations

• DimdPolyLEAN.muCircle = DimdPolyLEAN.μCircle

def DimdPolyLEAN.Cavg : ℝ

Cavg: Cavg.

Equations

• DimdPolyLEAN.Cavg = 1

theorem DimdPolyLEAN.Cavg_pos : 0 < Cavg

noncomputable def DimdPolyLEAN.Crot : ℝ

Crot: Crot.

Equations

• DimdPolyLEAN.Crot = 64 * Real.pi

theorem DimdPolyLEAN.Crot_pos : 0 < Crot

noncomputable def DimdPolyLEAN.zeta (x : Circle) : ℂ

zeta: zeta.

Equations

• DimdPolyLEAN.zeta x = ↑(AddCircle.toCircle x)

theorem DimdPolyLEAN.norm_zeta (x : Circle) : ‖zeta x‖ = 1

noncomputable def DimdPolyLEAN.circleChar (n : ℕ) : Circle → ℂ

circleChar: circle Char.

Equations

• DimdPolyLEAN.circleChar n x = DimdPolyLEAN.zeta x ^ n

theorem DimdPolyLEAN.circleChar_eq_zeta_pow (n : ℕ) (x : Circle) : circleChar n x = zeta x ^ n

structure DimdPolyLEAN.CircleArc : Type

CircleArc: Circle Arc.

• left : ℝ

  left: left.

• right : ℝ

  right: right.

• left_le_right : self.left ≤ self.right
• width_le_period : self.right - self.left ≤ 2 * Real.pi

def DimdPolyLEAN.arcLength (I : CircleArc) : ℝ

arcLength: arc Length.

Equations

• DimdPolyLEAN.arcLength I = I.right - I.left

noncomputable def DimdPolyLEAN.arcParam (I : CircleArc) (t : ℝ) : Circle

arcParam: arc Param.

Equations

• DimdPolyLEAN.arcParam I t = ↑(I.left + t * DimdPolyLEAN.arcLength I)

def DimdPolyLEAN.arcSet (I : CircleArc) : Set Circle

arcSet: arc Set.

Equations

• DimdPolyLEAN.arcSet I = {x : DimdPolyLEAN.Circle | ∃ t ∈ Set.Icc 0 1, DimdPolyLEAN.arcParam I t = x}

noncomputable def DimdPolyLEAN.carrierArc (N : ℕ) (k : Fin N) : CircleArc

carrierArc: carrier Arc.

Equations

• DimdPolyLEAN.carrierArc N k = { left := 2 * Real.pi * ↑↑k / ↑N, right := 2 * Real.pi * ↑(↑k + 1) / ↑N, left_le_right := ⋯, width_le_period := ⋯ }

theorem DimdPolyLEAN.carrierArc_length {N : ℕ} (k : Fin N) : arcLength (carrierArc N k) = 2 * Real.pi / ↑N

theorem DimdPolyLEAN.carrierArc_length_pos {N : ℕ} (k : Fin N) : 0 < arcLength (carrierArc N k)

theorem DimdPolyLEAN.carrierArc_left_nonneg {N : ℕ} (k : Fin N) : 0 ≤ (carrierArc N k).left

theorem DimdPolyLEAN.carrierArc_right_le_period {N : ℕ} (k : Fin N) : (carrierArc N k).right ≤ 2 * Real.pi

theorem DimdPolyLEAN.carrierArc_left_lt_right {N : ℕ} (k : Fin N) : (carrierArc N k).left < (carrierArc N k).right

theorem DimdPolyLEAN.carrierArc_arcSet_eq_mk_image_Icc {N : ℕ} (k : Fin N) : arcSet (carrierArc N k) = QuotientAddGroup.mk '' Set.Icc (carrierArc N k).left (carrierArc N k).right

theorem DimdPolyLEAN.carrierArc_arcSet_eq_mk_image_Ioc_union_left {N : ℕ} (k : Fin N) : arcSet (carrierArc N k) = QuotientAddGroup.mk '' Set.Ioc (carrierArc N k).left (carrierArc N k).right ∪ {↑(carrierArc N k).left}

theorem DimdPolyLEAN.quotient_mk_injOn_Ioc_zero_period : Set.InjOn (fun (t : ℝ) => ↑t) (Set.Ioc 0 (2 * Real.pi))

theorem DimdPolyLEAN.carrierArc_mk_preimage_image_Ioc_inter_fundamental {N : ℕ} (k : Fin N) : (fun (t : ℝ) => ↑t) ⁻¹' (fun (t : ℝ) => ↑t) '' Set.Ioc (carrierArc N k).left (carrierArc N k).right ∩ Set.Ioc 0 (2 * Real.pi) = Set.Ioc (carrierArc N k).left (carrierArc N k).right

theorem DimdPolyLEAN.volume_singleton_circle (x : Circle) : MeasureTheory.volume {x} = 0

theorem DimdPolyLEAN.μCircle_singleton (x : Circle) : μCircle {x} = 0

theorem DimdPolyLEAN.carrierArc_arcSet_ae_eq_mk_image_Ioc {N : ℕ} (k : Fin N) : arcSet (carrierArc N k) =ᵐ[μCircle] QuotientAddGroup.mk '' Set.Ioc (carrierArc N k).left (carrierArc N k).right

theorem DimdPolyLEAN.carrierArc_arcSet_ae_eq_mk_image_Ioc_volume {N : ℕ} (k : Fin N) : arcSet (carrierArc N k) =ᵐ[MeasureTheory.volume] QuotientAddGroup.mk '' Set.Ioc (carrierArc N k).left (carrierArc N k).right

noncomputable def DimdPolyLEAN.carrierAverage {N : ℕ} (k : Fin N) (f : Circle → ℂ) : ℂ

carrierAverage: carrier Average.

Equations

• DimdPolyLEAN.carrierAverage k f = ↑N * ∫ (x : DimdPolyLEAN.Circle) in DimdPolyLEAN.arcSet (DimdPolyLEAN.carrierArc N k), f x ∂DimdPolyLEAN.μCircle

theorem DimdPolyLEAN.arcLength_nonneg (I : CircleArc) : 0 ≤ arcLength I

theorem DimdPolyLEAN.continuous_arcParam (I : CircleArc) : Continuous (arcParam I)

theorem DimdPolyLEAN.arcSet_eq_image (I : CircleArc) : arcSet I = arcParam I '' Set.Icc 0 1

theorem DimdPolyLEAN.isCompact_arcSet (I : CircleArc) : IsCompact (arcSet I)

theorem DimdPolyLEAN.measurableSet_arcSet (I : CircleArc) : MeasurableSet (arcSet I)

theorem DimdPolyLEAN.volume_mk_image_carrierArc_Ioc {N : ℕ} (k : Fin N) : MeasureTheory.volume ((fun (t : ℝ) => ↑t) '' Set.Ioc (carrierArc N k).left (carrierArc N k).right) = ENNReal.ofReal (arcLength (carrierArc N k))

theorem DimdPolyLEAN.period_smul_μCircle_mk_image_carrierArc_Ioc {N : ℕ} (k : Fin N) : ENNReal.ofReal (2 * Real.pi) * μCircle ((fun (t : ℝ) => ↑t) '' Set.Ioc (carrierArc N k).left (carrierArc N k).right) = ENNReal.ofReal (arcLength (carrierArc N k))

theorem DimdPolyLEAN.period_smul_μCircle_carrierArc {N : ℕ} (k : Fin N) : ENNReal.ofReal (2 * Real.pi) * μCircle (arcSet (carrierArc N k)) = ENNReal.ofReal (arcLength (carrierArc N k))

noncomputable def DimdPolyLEAN.arcIntegral (I : CircleArc) (f : Circle → ℝ) : ℝ

arcIntegral: arc Integral.

Equations

• DimdPolyLEAN.arcIntegral I f = ∫ (x : DimdPolyLEAN.Circle) in DimdPolyLEAN.arcSet I, f x ∂DimdPolyLEAN.μCircle

theorem DimdPolyLEAN.carrierArc_arcIntegral_eq_mk_image_Ioc {N : ℕ} (k : Fin N) (f : Circle → ℝ) : arcIntegral (carrierArc N k) f = ∫ (x : Circle) in QuotientAddGroup.mk '' Set.Ioc (carrierArc N k).left (carrierArc N k).right, f x ∂μCircle

theorem DimdPolyLEAN.carrierArc_mk_image_Ioc_integral_eq_scaled {N : ℕ} (k : Fin N) (f : Circle → ℝ) : ∫ (x : Circle) in (fun (t : ℝ) => ↑t) '' Set.Ioc (carrierArc N k).left (carrierArc N k).right, f x ∂μCircle = (2 * Real.pi)⁻¹ * ∫ (t : ℝ) in Set.Ioc (carrierArc N k).left (carrierArc N k).right, f ↑t

noncomputable def DimdPolyLEAN.arcAverage (I : CircleArc) (f : Circle → ℂ) : ℂ

arcAverage: arc Average.

Equations

• DimdPolyLEAN.arcAverage I f = (DimdPolyLEAN.arcLength I)⁻¹ • ∫ (x : DimdPolyLEAN.Circle) in DimdPolyLEAN.arcSet I, f x ∂DimdPolyLEAN.μCircle

theorem DimdPolyLEAN.intervalParam_mem_arc (I : CircleArc) (t : ℝ) : t ∈ Set.Icc 0 1 → arcParam I t ∈ arcSet I

theorem DimdPolyLEAN.arcIntegral_nonneg (I : CircleArc) {f : Circle → ℝ} (hf : ∀ x ∈ arcSet I, 0 ≤ f x) : 0 ≤ arcIntegral I f

theorem DimdPolyLEAN.arcAverage_eq_arcIntegral_div (I : CircleArc) (f : Circle → ℂ) : arcAverage I f = (arcLength I)⁻¹ • ∫ (x : Circle) in arcSet I, f x ∂μCircle

theorem DimdPolyLEAN.norm_circleChar (n : ℕ) (x : Circle) : ‖circleChar n x‖ = 1

theorem DimdPolyLEAN.circleChar_zero (x : Circle) : circleChar 0 x = 1

theorem DimdPolyLEAN.circleChar_one (x : Circle) : circleChar 1 x = zeta x

theorem DimdPolyLEAN.circleChar_add (m n : ℕ) (x : Circle) : circleChar (m + n) x = circleChar m x * circleChar n x

theorem DimdPolyLEAN.circleChar_mk (n : ℕ) (theta : ℝ) : circleChar n ↑theta = Complex.exp (Complex.I * ↑n * ↑theta)

theorem DimdPolyLEAN.circleChar_eq_fourier_nat (n : ℕ) (x : Circle) : circleChar n x = (fourier ↑n) x

theorem DimdPolyLEAN.circleChar_carrierArc_arcParam {N : ℕ} (k : Fin N) (t : ℝ) : circleChar N (arcParam (carrierArc N k) t) = Complex.exp (Complex.I * (2 * ↑Real.pi * ↑t))

theorem DimdPolyLEAN.circleIntegral_union_finset {ι : Type} [Fintype ι] (I : ι → CircleArc) (hdisj : Pairwise fun (i j : ι) => Disjoint (arcSet (I i)) (arcSet (I j))) {f : Circle → ℝ} (hf : ∀ (i : ι), MeasureTheory.IntegrableOn f (arcSet (I i)) μCircle) : ∫ (x : Circle) in ⋃ (i : ι), arcSet (I i), f x ∂μCircle = ∑ i : ι, arcIntegral (I i) f

theorem DimdPolyLEAN.circleIntegral_split_compl (s : Set Circle) (hs : MeasurableSet s) {f : Circle → ℝ} (hf : MeasureTheory.Integrable f μCircle) : ∫ (x : Circle), f x ∂μCircle = ∫ (x : Circle) in s, f x ∂μCircle + ∫ (x : Circle) in sᶜ, f x ∂μCircle

theorem DimdPolyLEAN.constantCenter_fastRotate_carrierArc_sq_le_defectSq {N : ℕ} (k : Fin N) {c u : ℂ} (hc : c ≠ 0) : arcLength (carrierArc N k) * ‖u‖ ^ 2 ≤ Crot * arcIntegral (carrierArc N k) fun (x : Circle) => (‖c + circleChar N x * u‖ - ‖c‖) ^ 2

theorem DimdPolyLEAN.continuous_eq_of_ae_eq_gamma {d : ℕ} (hd : 0 < d) {f g : Cd d → ℂ} (hf : Continuous f) (hg : Continuous g) (hfg : f =ᵐ[gammaD d] g) : f = g

Phase-space analytic boundary stubs

These declaration-shaped stubs expose the analytic objects needed by ExactModulusRecovery. The definitions are placeholders; the theorem statements record the frozen API that the STFT/ambiguity proof must eventually provide.

@[reducible, inline]

abbrev DimdPolyLEAN.RealVec (d : ℕ) : Type

RealVec: Real Vec.

Equations

• DimdPolyLEAN.RealVec d = EuclideanSpace ℝ (Fin d)

@[reducible, inline]

abbrev DimdPolyLEAN.PhaseSpace (d : ℕ) : Type

PhaseSpace: Phase Space.

Equations

• DimdPolyLEAN.PhaseSpace d = (DimdPolyLEAN.RealVec d × DimdPolyLEAN.RealVec d)

@[reducible, inline]

noncomputable abbrev DimdPolyLEAN.L2Real (d : ℕ) : AddSubgroup (RealVec d →ₘ[MeasureTheory.volume] ℂ)

L2Real: L2 Real.

Equations

• DimdPolyLEAN.L2Real d = MeasureTheory.Lp ℂ 2 MeasureTheory.volume

noncomputable def DimdPolyLEAN.stftRep {d : ℕ} : ↥(L2Real d) → ↥(L2Real d) → PhaseSpace d → ℂ

stftRep: stft Rep.

Equations

• DimdPolyLEAN.stftRep h f ξ = ∫ (t : DimdPolyLEAN.RealVec d), ↑↑f t * star (↑↑h (t - ξ.1)) * Complex.exp (-(2 * ↑Real.pi) * Complex.I * ↑(inner ℝ ξ.2 t))

noncomputable def DimdPolyLEAN.ambiguityRep {d : ℕ} : ↥(L2Real d) → ↥(L2Real d) → PhaseSpace d → ℂ

ambiguityRep: ambiguity Rep.

Equations

• DimdPolyLEAN.ambiguityRep f g ξ = ∫ (t : DimdPolyLEAN.RealVec d), ↑↑f (t + (1 / 2) • ξ.1) * star (↑↑g (t - (1 / 2) • ξ.1)) * Complex.exp (-(2 * ↑Real.pi) * Complex.I * ↑(inner ℝ ξ.2 t))

noncomputable def DimdPolyLEAN.symplecticFourierRep {d : ℕ} (F : PhaseSpace d → ℂ) : PhaseSpace d → ℂ

symplecticFourierRep: symplectic Fourier Rep.

Equations

• DimdPolyLEAN.symplecticFourierRep F ξ = ∫ (η : DimdPolyLEAN.PhaseSpace d), F η * Complex.exp (2 * ↑Real.pi * Complex.I * ↑(inner ℝ η.2 ξ.1 - inner ℝ η.1 ξ.2))

theorem DimdPolyLEAN.symplecticFourierPhase_norm {d : ℕ} (η ξ : PhaseSpace d) : ‖Complex.exp (2 * ↑Real.pi * Complex.I * ↑(inner ℝ η.2 ξ.1 - inner ℝ η.1 ξ.2))‖ = 1

noncomputable def DimdPolyLEAN.symplecticFormLinear {d : ℕ} : PhaseSpace d →ₗ[ℝ] PhaseSpace d →ₗ[ℝ] ℝ

symplecticFormLinear: symplectic Form Linear.

Equations

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

theorem DimdPolyLEAN.symplecticFourierRep_eq_vectorFourier {d : ℕ} (F : PhaseSpace d → ℂ) (ξ : PhaseSpace d) : symplecticFourierRep F ξ = VectorFourier.fourierIntegral Real.fourierChar MeasureTheory.volume symplecticFormLinear F ξ

theorem DimdPolyLEAN.symplecticFourierRep_sub_le_lpNorm_one {d : ℕ} {G₁ G₂ : PhaseSpace d → ℂ} (h1 : MeasureTheory.Integrable G₁ MeasureTheory.volume) (h2 : MeasureTheory.Integrable G₂ MeasureTheory.volume) (ξ : PhaseSpace d) : ‖symplecticFourierRep G₁ ξ - symplecticFourierRep G₂ ξ‖ ≤ MeasureTheory.lpNorm (fun (η : PhaseSpace d) => G₁ η - G₂ η) 1 MeasureTheory.volume

theorem DimdPolyLEAN.tendsto_symplecticFourierRep_of_lpNorm_one {d : ℕ} {G : PhaseSpace d → ℂ} {Gₙ : ℕ → PhaseSpace d → ℂ} (hG : MeasureTheory.Integrable G MeasureTheory.volume) (hGₙ : ∀ (n : ℕ), MeasureTheory.Integrable (Gₙ n) MeasureTheory.volume) (hLp : Filter.Tendsto (fun (n : ℕ) => MeasureTheory.lpNorm (fun (η : PhaseSpace d) => Gₙ n η - G η) 1 MeasureTheory.volume) Filter.atTop (nhds 0)) (ξ : PhaseSpace d) : Filter.Tendsto (fun (n : ℕ) => symplecticFourierRep (Gₙ n) ξ) Filter.atTop (nhds (symplecticFourierRep G ξ))

theorem DimdPolyLEAN.symplecticFourierRep_eq_of_lpNorm_one_approx {d : ℕ} {G : PhaseSpace d → ℂ} {Gₙ : ℕ → PhaseSpace d → ℂ} {A : ℂ} {Aₙ : ℕ → ℂ} (hG : MeasureTheory.Integrable G MeasureTheory.volume) (hGₙ : ∀ (n : ℕ), MeasureTheory.Integrable (Gₙ n) MeasureTheory.volume) (hLp : Filter.Tendsto (fun (n : ℕ) => MeasureTheory.lpNorm (fun (η : PhaseSpace d) => Gₙ n η - G η) 1 MeasureTheory.volume) Filter.atTop (nhds 0)) (hA : Filter.Tendsto Aₙ Filter.atTop (nhds A)) (ξ : PhaseSpace d) (hEq : ∀ (n : ℕ), symplecticFourierRep (Gₙ n) ξ = Aₙ n) : symplecticFourierRep G ξ = A

def DimdPolyLEAN.IsL2Rep {d : ℕ} (f : ↥(L2Real d)) (fRep : RealVec d → ℂ) : Prop

IsL2Rep: Is L2 Rep.

Equations

• DimdPolyLEAN.IsL2Rep f fRep = ∃ (hf_mem : MeasureTheory.MemLp fRep 2 MeasureTheory.volume), MeasureTheory.MemLp.toLp fRep hf_mem = f

noncomputable def DimdPolyLEAN.translateL2 {d : ℕ} (a : RealVec d) (f : ↥(L2Real d)) : ↥(L2Real d)

translateL2: translate L2.

Equations

• DimdPolyLEAN.translateL2 a f = DomAddAct.mk a +ᵥ f

theorem DimdPolyLEAN.translateL2_coeFn {d : ℕ} (a : RealVec d) (f : ↥(L2Real d)) : ↑↑(translateL2 a f) =ᵐ[MeasureTheory.volume] fun (t : RealVec d) => ↑↑f (t + a)

theorem DimdPolyLEAN.translateL2_neg_coeFn {d : ℕ} (a : RealVec d) (f : ↥(L2Real d)) : ↑↑(translateL2 (-a) f) =ᵐ[MeasureTheory.volume] fun (t : RealVec d) => ↑↑f (t - a)

theorem DimdPolyLEAN.norm_translateL2 {d : ℕ} (a : RealVec d) (f : ↥(L2Real d)) : ‖translateL2 a f‖ = ‖f‖

theorem DimdPolyLEAN.dist_translateL2 {d : ℕ} (a : RealVec d) (f g : ↥(L2Real d)) : dist (translateL2 a f) (translateL2 a g) = dist f g

theorem DimdPolyLEAN.continuous_translateL2_apply {d : ℕ} (f : ↥(L2Real d)) : Continuous fun (a : RealVec d) => translateL2 a f

noncomputable def DimdPolyLEAN.modulationPhase {d : ℕ} (ω t : RealVec d) : ℂ

modulationPhase: modulation Phase.

Equations

• DimdPolyLEAN.modulationPhase ω t = Complex.exp (-(2 * ↑Real.pi) * Complex.I * ↑(inner ℝ ω t))

theorem DimdPolyLEAN.modulationPhase_norm {d : ℕ} (ω t : RealVec d) : ‖modulationPhase ω t‖ = 1

theorem DimdPolyLEAN.fourier_translate_realVec {d : ℕ} (a : RealVec d) (f : RealVec d → ℂ) (_hf : MeasureTheory.Integrable f MeasureTheory.volume) : (FourierTransform.fourier fun (t : RealVec d) => f (t - a)) = fun (ω : RealVec d) => modulationPhase a ω * FourierTransform.fourier f ω

noncomputable def DimdPolyLEAN.schwartzCompSubConstCLM {d : ℕ} (a : RealVec d) : SchwartzMap (RealVec d) ℂ →L[ℂ] SchwartzMap (RealVec d) ℂ

schwartzCompSubConstCLM: schwartz Comp Sub Const CLM.

Equations

• DimdPolyLEAN.schwartzCompSubConstCLM a = SchwartzMap.compCLMOfAntilipschitz ℂ ⋯ ⋯

@[simp]

theorem DimdPolyLEAN.schwartzCompSubConstCLM_apply {d : ℕ} (a : RealVec d) (f : SchwartzMap (RealVec d) ℂ) : ⇑((schwartzCompSubConstCLM a) f) = ⇑f ∘ fun (x : RealVec d) => x - a

theorem DimdPolyLEAN.fourier_schwartzCompSubConstCLM_realVec {d : ℕ} (f : SchwartzMap (RealVec d) ℂ) (a : RealVec d) : FourierTransform.fourier ⇑((schwartzCompSubConstCLM a) f) = fun (ω : RealVec d) => modulationPhase a ω * FourierTransform.fourier (⇑f) ω

noncomputable def DimdPolyLEAN.modulateL2 {d : ℕ} (ω : RealVec d) (f : ↥(L2Real d)) : ↥(L2Real d)

modulateL2: modulate L2.

Equations

• DimdPolyLEAN.modulateL2 ω f = MeasureTheory.MemLp.toLp (fun (t : DimdPolyLEAN.RealVec d) => DimdPolyLEAN.modulationPhase ω t * ↑↑f t) ⋯

theorem DimdPolyLEAN.modulateL2_coeFn {d : ℕ} (ω : RealVec d) (f : ↥(L2Real d)) : ↑↑(modulateL2 ω f) =ᵐ[MeasureTheory.volume] fun (t : RealVec d) => modulationPhase ω t * ↑↑f t

theorem DimdPolyLEAN.norm_modulateL2 {d : ℕ} (ω : RealVec d) (f : ↥(L2Real d)) : ‖modulateL2 ω f‖ = ‖f‖

theorem DimdPolyLEAN.continuous_modulateL2_apply {d : ℕ} (f : ↥(L2Real d)) : Continuous fun (ω : RealVec d) => modulateL2 ω f

theorem DimdPolyLEAN.stftRep_congr_right {d : ℕ} {h f g : ↥(L2Real d)} (hfg : f = g) : stftRep h f = stftRep h g

theorem DimdPolyLEAN.stftRep_congr_left {d : ℕ} {h h' f : ↥(L2Real d)} (hh : h = h') : stftRep h f = stftRep h' f

theorem DimdPolyLEAN.ambiguityRep_congr_left {d : ℕ} {f f' g : ↥(L2Real d)} (hf : f = f') : ambiguityRep f g = ambiguityRep f' g

theorem DimdPolyLEAN.ambiguityRep_congr_right {d : ℕ} {f g g' : ↥(L2Real d)} (hg : g = g') : ambiguityRep f g = ambiguityRep f g'

theorem DimdPolyLEAN.ambiguityRep_eq_lpPairing {d : ℕ} (f g : ↥(L2Real d)) (ξ : PhaseSpace d) : ambiguityRep f g ξ = ((ContinuousLinearMap.lpPairing MeasureTheory.volume 2 2 (ContinuousLinearMap.mul ℂ ℂ)) (translateL2 ((1 / 2) • ξ.1) f)) (modulateL2 ξ.2 (star (translateL2 (-((1 / 2) • ξ.1)) g)))

theorem DimdPolyLEAN.edist_modulateL2 {d : ℕ} (ω : RealVec d) (f g : ↥(L2Real d)) : edist (modulateL2 ω f) (modulateL2 ω g) = edist f g

theorem DimdPolyLEAN.dist_modulateL2 {d : ℕ} (ω : RealVec d) (f g : ↥(L2Real d)) : dist (modulateL2 ω f) (modulateL2 ω g) = dist f g

theorem DimdPolyLEAN.continuous_modulateL2 {d : ℕ} {X : Type u_1} [TopologicalSpace X] {ω : X → RealVec d} {h : X → ↥(L2Real d)} (hω : Continuous ω) (hh : Continuous h) : Continuous fun (x : X) => modulateL2 (ω x) (h x)

theorem DimdPolyLEAN.edist_star_L2 {d : ℕ} (f g : ↥(L2Real d)) : edist (star f) (star g) = edist f g

theorem DimdPolyLEAN.dist_star_L2 {d : ℕ} (f g : ↥(L2Real d)) : dist (star f) (star g) = dist f g

theorem DimdPolyLEAN.continuous_star_L2 {d : ℕ} : Continuous fun (f : ↥(L2Real d)) => star f

theorem DimdPolyLEAN.norm_star_L2 {d : ℕ} (f : ↥(L2Real d)) : ‖star f‖ = ‖f‖

theorem DimdPolyLEAN.norm_ambiguityRep_le {d : ℕ} (f g : ↥(L2Real d)) (ξ : PhaseSpace d) : ‖ambiguityRep f g ξ‖ ≤ ‖f‖ * ‖g‖

theorem DimdPolyLEAN.stftRep_eq_lpPairing {d : ℕ} (h f : ↥(L2Real d)) (ξ : PhaseSpace d) : stftRep h f ξ = ((ContinuousLinearMap.lpPairing MeasureTheory.volume 2 2 (ContinuousLinearMap.mul ℂ ℂ)) f) (modulateL2 ξ.2 (star (translateL2 (-ξ.1) h)))

theorem DimdPolyLEAN.norm_stftRep_le {d : ℕ} (h f : ↥(L2Real d)) (ξ : PhaseSpace d) : ‖stftRep h f ξ‖ ≤ ‖f‖ * ‖h‖

theorem DimdPolyLEAN.continuous_stftRep {d : ℕ} (h f : ↥(L2Real d)) : Continuous (stftRep h f)

theorem DimdPolyLEAN.continuous_spectrogramRep {d : ℕ} (h f : ↥(L2Real d)) : Continuous fun (ξ : PhaseSpace d) => ↑(‖stftRep h f ξ‖ ^ 2)

theorem DimdPolyLEAN.spectrogramRep_eq_stft_mul_star {d : ℕ} (h f : ↥(L2Real d)) (ξ : PhaseSpace d) : ↑(‖stftRep h f ξ‖ ^ 2) = stftRep h f ξ * star (stftRep h f ξ)

theorem DimdPolyLEAN.spectrogram_ambiguity_identity_of_product_moyal {d : ℕ} (hmoyal : ∀ (h f : ↥(L2Real d)) (ξ : PhaseSpace d), symplecticFourierRep (fun (η : PhaseSpace d) => stftRep h f η * star (stftRep h f η)) ξ = ambiguityRep f f ξ * star (ambiguityRep h h ξ)) (h f : ↥(L2Real d)) (ξ : PhaseSpace d) : symplecticFourierRep (fun (η : PhaseSpace d) => ↑(‖stftRep h f η‖ ^ 2)) ξ = ambiguityRep f f ξ * star (ambiguityRep h h ξ)

theorem DimdPolyLEAN.spectrogram_ambiguity_identity {d : ℕ} (h f : ↥(L2Real d)) (ξ : PhaseSpace d) : symplecticFourierRep (fun (η : PhaseSpace d) => ↑(‖stftRep h f η‖ ^ 2)) ξ = ambiguityRep f f ξ * star (ambiguityRep h h ξ)

theorem DimdPolyLEAN.continuous_ambiguityRep {d : ℕ} (f g : ↥(L2Real d)) : Continuous (ambiguityRep f g)

theorem DimdPolyLEAN.ae_unimodular_phase_to_L2_eq {d : ℕ} {f g : ↥(L2Real d)} {fRep gRep : RealVec d → ℂ} {w : ℂ} (hf_rep : IsL2Rep f fRep) (hg_rep : IsL2Rep g gRep) (hphase : gRep =ᵐ[MeasureTheory.volume] fun (u : RealVec d) => w * fRep u) : g = w • f

theorem DimdPolyLEAN.rep_ae_eq_zero_of_L2_eq_zero {d : ℕ} {f : ↥(L2Real d)} {fRep : RealVec d → ℂ} (hf_rep : IsL2Rep f fRep) (hf_zero : f = 0) : fRep =ᵐ[MeasureTheory.volume] fun (x : RealVec d) => 0

theorem DimdPolyLEAN.L2_eq_zero_of_rep_ae_eq_zero {d : ℕ} {f : ↥(L2Real d)} {fRep : RealVec d → ℂ} (hf_rep : IsL2Rep f fRep) (hzero : fRep =ᵐ[MeasureTheory.volume] fun (x : RealVec d) => 0) : f = 0

theorem DimdPolyLEAN.boxPartialSums_have_L2_limit {d : ℕ} (hd : 0 < d) (kappa : MultiIndex d) : True

theorem DimdPolyLEAN.circleFourier_exact_modulus_bridge : True