TensorBasis

TensorBasis

Statement-first scaffold for the frozen coefficient model and realization maps for the fixed-dimension polyanalytic Fock basis.

theorem DimdPolyLEAN.coeff_ofPkappa {d : ℕ} (hd : 0 < d) (kappa : MultiIndex d) (F : Pkappa d kappa) (alpha : Idx d) : coeffSkappa (ofPkappa kappa F) alpha = coeffPkappa F alpha

theorem DimdPolyLEAN.evalPkappa_zero {d : ℕ} (hd : 0 < d) (kappa : MultiIndex d) : evalPkappa kappa 0 = 0

theorem DimdPolyLEAN.evalPkappa_add {d : ℕ} (hd : 0 < d) (kappa : MultiIndex d) (F G : Pkappa d kappa) : evalPkappa kappa (F + G) = fun (z : Cd d) => evalPkappa kappa F z + evalPkappa kappa G z

theorem DimdPolyLEAN.evalPkappa_smul {d : ℕ} (hd : 0 < d) (kappa : MultiIndex d) (c : ℂ) (F : Pkappa d kappa) : evalPkappa kappa (c • F) = fun (z : Cd d) => c * evalPkappa kappa F z

theorem DimdPolyLEAN.evalPkappa_sub {d : ℕ} (hd : 0 < d) (kappa : MultiIndex d) (F G : Pkappa d kappa) : evalPkappa kappa (F - G) = fun (z : Cd d) => evalPkappa kappa F z - evalPkappa kappa G z

theorem DimdPolyLEAN.projFinset_idempotent {d : ℕ} (hd : 0 < d) {kappa : MultiIndex d} (E : Finset (Idx d)) (F : Pkappa d kappa) : projFinset E (projFinset E F) = projFinset E F

theorem DimdPolyLEAN.exact_truncate_coeff_energy {d : ℕ} (hd : 0 < d) {kappa : MultiIndex d} (E : Finset (Idx d)) (F : Skappa d kappa) : ‖truncateFinset E F‖ ^ 2 = ∑ alpha ∈ E, ‖coeffSkappa F alpha‖ ^ 2

theorem DimdPolyLEAN.Phi_rotate_one_exp {d : ℕ} (kappa alpha : MultiIndex d) (q0 : Fin d) (t : ℝ) (z : Cd d) : Phi kappa alpha (Function.update z q0 (Complex.exp (Complex.I * ↑t) * z q0)) = Complex.exp (Complex.I * ((↑↑(alpha q0) - ↑↑(kappa q0)) * ↑t)) * Phi kappa alpha z

theorem DimdPolyLEAN.Phi_rotateCoord_circle_phase {d : ℕ} (kappa alpha : MultiIndex d) (q0 : Fin d) (x : Circle) (z : Cd d) : (fourier ↑(kappa q0)) x * Phi kappa alpha (Function.update z q0 ((fourier 1) x * z q0)) = (fourier ↑(alpha q0)) x * Phi kappa alpha z

theorem DimdPolyLEAN.evalPkappa_rotateCoord_circle_phase_sum {d : ℕ} (kappa : MultiIndex d) (q0 : Fin d) (F : Pkappa d kappa) (x : Circle) (z : Cd d) : (fourier ↑(kappa q0)) x * evalPkappa kappa F (Function.update z q0 ((fourier 1) x * z q0)) = ∑ alpha ∈ F.support, F alpha * Phi kappa alpha z * circleChar (alpha q0) x

theorem DimdPolyLEAN.evalPkappa_total_mass {d : ℕ} (hd : 0 < d) (kappa : MultiIndex d) (F : Pkappa d kappa) : ∫ (z : Cd d), ‖evalPkappa kappa F z‖ ^ 2 ∂gammaD d = ‖F‖ ^ 2

theorem DimdPolyLEAN.toFun_ofPkappa {d : ℕ} (kappa : MultiIndex d) (F : Pkappa d kappa) : toFun kappa (ofPkappa kappa F) = evalPkappa kappa F

theorem DimdPolyLEAN.summable_sq_Phi_eval {d : ℕ} (kappa : MultiIndex d) (z : Cd d) : Summable fun (alpha : Idx d) => ‖Phi kappa alpha z‖ ^ 2

theorem DimdPolyLEAN.summable_skappa_eval_mul_of_phi_sq {d : ℕ} (kappa : MultiIndex d) (U : Skappa d kappa) (z : Cd d) (hPhi : Summable fun (alpha : Idx d) => ‖Phi kappa alpha z‖ ^ 2) : Summable fun (alpha : Idx d) => coeffSkappa U alpha * Phi kappa alpha z

theorem DimdPolyLEAN.summable_skappa_eval_mul {d : ℕ} (kappa : MultiIndex d) (U : Skappa d kappa) (z : Cd d) : Summable fun (alpha : Idx d) => coeffSkappa U alpha * Phi kappa alpha z

theorem DimdPolyLEAN.toFun_rotateCoord_circle_phase_tsum {d : ℕ} (kappa : MultiIndex d) (q0 : Fin d) (U : Skappa d kappa) (x : Circle) (z : Cd d) : (fourier ↑(kappa q0)) x * toFun kappa U (Function.update z q0 ((fourier 1) x * z q0)) = ∑' (alpha : Idx d), coeffSkappa U alpha * Phi kappa alpha z * circleChar (alpha q0) x

theorem DimdPolyLEAN.box_subset_box {d : ℕ} {J K : MultiIndex d} (hJK : J ≤ K) : box J ⊆ box K

theorem DimdPolyLEAN.finite_subset_box {d : ℕ} (E : Finset (Idx d)) : ∃ (J : MultiIndex d), E ⊆ box J

theorem DimdPolyLEAN.tendsto_box_atTop {d : ℕ} : Filter.Tendsto (fun (J : MultiIndex d) => box J) Filter.atTop Filter.atTop

Representative bridge stubs

These are the Skappa realization facts needed by the phase-space exact modulus recovery file. They are declaration-shaped stubs for the locally-uniform/L2 representative package described in the tensor-basis

noncomputable def DimdPolyLEAN.partialSum {d : ℕ} (kappa : MultiIndex d) (U : Skappa d kappa) (J : MultiIndex d) : Cd d → ℂ

partialSum: partial Sum.

Equations

• DimdPolyLEAN.partialSum kappa U J z = ∑ alpha ∈ DimdPolyLEAN.box J, DimdPolyLEAN.coeffSkappa U alpha * DimdPolyLEAN.Phi kappa alpha z

theorem DimdPolyLEAN.partialSum_tendsto_toFun_pointwise {d : ℕ} (kappa : MultiIndex d) (U : Skappa d kappa) (z : Cd d) : Filter.Tendsto (fun (J : MultiIndex d) => partialSum kappa U J z) Filter.atTop (nhds (toFun kappa U z))

noncomputable def DimdPolyLEAN.evalPkappaL2 {d : ℕ} (kappa : MultiIndex d) (F : Pkappa d kappa) : ↥(L2Tensor d)

evalPkappaL2: eval Pkappa L2.

Equations

• DimdPolyLEAN.evalPkappaL2 kappa F = DimdPolyLEAN.toL2 kappa (DimdPolyLEAN.ofPkappa kappa F)

noncomputable def DimdPolyLEAN.PhiL2 {d : ℕ} (kappa : MultiIndex d) (alpha : Idx d) : ↥(L2Tensor d)

PhiL2: Phi L2.

Equations

• DimdPolyLEAN.PhiL2 kappa alpha = DimdPolyLEAN.evalPkappaL2 kappa (Finsupp.single alpha 1)

def DimdPolyLEAN.BoxPartialSumsLocallyUniformTo {d : ℕ} (kappa : MultiIndex d) (U : Skappa d kappa) (f : Cd d → ℂ) : Prop

BoxPartialSumsLocallyUniformTo: Box Partial Sums Locally Uniform To.

Equations

• DimdPolyLEAN.BoxPartialSumsLocallyUniformTo kappa U f = TendstoLocallyUniformly (fun (J : DimdPolyLEAN.MultiIndex d) => DimdPolyLEAN.partialSum kappa U J) f Filter.atTop

def DimdPolyLEAN.BoxPartialSumsLocallyUniformCauchy {d : ℕ} (kappa : MultiIndex d) (U : Skappa d kappa) : Prop

BoxPartialSumsLocallyUniformCauchy: Box Partial Sums Locally Uniform Cauchy.

Equations

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

def DimdPolyLEAN.IsTensorL2Rep {d : ℕ} (F : ↥(L2Tensor d)) (f : Cd d → ℂ) : Prop

IsTensorL2Rep: Is Tensor L2 Rep.

Equations

• DimdPolyLEAN.IsTensorL2Rep F f = ∃ (hf_mem : MeasureTheory.MemLp f 2 (DimdPolyLEAN.gammaD d)), MeasureTheory.MemLp.toLp f hf_mem = F

def DimdPolyLEAN.L2BoxPartialSumsTendTo {d : ℕ} (kappa : MultiIndex d) (U : Skappa d kappa) (F : ↥(L2Tensor d)) : Prop

L2BoxPartialSumsTendTo: L2 Box Partial Sums Tend To.

Equations

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

theorem DimdPolyLEAN.continuous_Phi {d : ℕ} (kappa alpha : MultiIndex d) : Continuous (Phi kappa alpha)

theorem DimdPolyLEAN.continuous_evalPkappa {d : ℕ} (kappa : MultiIndex d) (F : Pkappa d kappa) : Continuous (evalPkappa kappa F)

theorem DimdPolyLEAN.integrable_evalPkappa_sq {d : ℕ} (hd : 0 < d) (kappa : MultiIndex d) (F : Pkappa d kappa) : MeasureTheory.Integrable (fun (z : Cd d) => ‖evalPkappa kappa F z‖ ^ 2) (gammaD d)

theorem DimdPolyLEAN.memLp_two_evalPkappa {d : ℕ} (hd : 0 < d) (kappa : MultiIndex d) (F : Pkappa d kappa) : MeasureTheory.MemLp (evalPkappa kappa F) 2 (gammaD d)

theorem DimdPolyLEAN.evalPkappaL2_eq_toLp {d : ℕ} (hd : 0 < d) (kappa : MultiIndex d) (F : Pkappa d kappa) : evalPkappaL2 kappa F = MeasureTheory.MemLp.toLp (evalPkappa kappa F) ⋯

theorem DimdPolyLEAN.evalPkappaL2_add {d : ℕ} (hd : 0 < d) (kappa : MultiIndex d) (F G : Pkappa d kappa) : evalPkappaL2 kappa (F + G) = evalPkappaL2 kappa F + evalPkappaL2 kappa G

theorem DimdPolyLEAN.evalPkappaL2_smul {d : ℕ} (hd : 0 < d) (kappa : MultiIndex d) (c : ℂ) (F : Pkappa d kappa) : evalPkappaL2 kappa (c • F) = c • evalPkappaL2 kappa F

theorem DimdPolyLEAN.evalPkappaL2_zero {d : ℕ} (hd : 0 < d) (kappa : MultiIndex d) : evalPkappaL2 kappa 0 = 0

theorem DimdPolyLEAN.PhiL2_orthonormal {d : ℕ} (hd : 0 < d) (kappa : MultiIndex d) (alpha beta : Idx d) : inner ℂ (PhiL2 kappa alpha) (PhiL2 kappa beta) = if alpha = beta then 1 else 0

theorem DimdPolyLEAN.evalPkappaL2_single {d : ℕ} (hd : 0 < d) (kappa : MultiIndex d) (alpha : Idx d) (c : ℂ) : evalPkappaL2 kappa (Finsupp.single alpha c) = c • PhiL2 kappa alpha

theorem DimdPolyLEAN.finite_coeff_recovery {d : ℕ} (hd : 0 < d) (kappa : MultiIndex d) (F : Pkappa d kappa) (beta : Idx d) : coeffPkappa F beta = inner ℂ (PhiL2 kappa beta) (evalPkappaL2 kappa F)

theorem DimdPolyLEAN.PhiL2_orthonormal_family {d : ℕ} (hd : 0 < d) (kappa : MultiIndex d) : Orthonormal ℂ fun (alpha : Idx d) => PhiL2 kappa alpha

theorem DimdPolyLEAN.summable_PhiL2_coeff_smul {d : ℕ} (hd : 0 < d) (kappa : MultiIndex d) (U : Skappa d kappa) : Summable fun (alpha : Idx d) => coeffSkappa U alpha • PhiL2 kappa alpha

theorem DimdPolyLEAN.evalPkappaL2_truncateFinset {d : ℕ} (hd : 0 < d) (kappa : MultiIndex d) (U : Skappa d kappa) (E : Finset (Idx d)) : evalPkappaL2 kappa (truncateFinset E U) = ∑ alpha ∈ E, coeffSkappa U alpha • PhiL2 kappa alpha

theorem DimdPolyLEAN.evalPkappaL2_box_tendsto_tsum {d : ℕ} (hd : 0 < d) (kappa : MultiIndex d) (U : Skappa d kappa) : Filter.Tendsto (fun (J : MultiIndex d) => evalPkappaL2 kappa (truncateFinset (box J) U)) Filter.atTop (nhds (∑' (alpha : Idx d), coeffSkappa U alpha • PhiL2 kappa alpha))

theorem DimdPolyLEAN.evalPkappa_truncateFinset {d : ℕ} (hd : 0 < d) (kappa : MultiIndex d) (U : Skappa d kappa) (E : Finset (Idx d)) : evalPkappa kappa (truncateFinset E U) = fun (z : Cd d) => ∑ alpha ∈ E, coeffSkappa U alpha * Phi kappa alpha z

theorem DimdPolyLEAN.l2_tsum_represents_toFun {d : ℕ} (hd : 0 < d) (kappa : MultiIndex d) (U : Skappa d kappa) : IsTensorL2Rep (∑' (alpha : Idx d), coeffSkappa U alpha • PhiL2 kappa alpha) (toFun kappa U)

theorem DimdPolyLEAN.partialSum_continuous {d : ℕ} (hd : 0 < d) (kappa : MultiIndex d) (U : Skappa d kappa) (J : MultiIndex d) : Continuous (partialSum kappa U J)

theorem DimdPolyLEAN.partialSum_locallyUniform {d : ℕ} (hd : 0 < d) (kappa : MultiIndex d) (U : Skappa d kappa) : BoxPartialSumsLocallyUniformCauchy kappa U

theorem DimdPolyLEAN.toFun_eq_boxLimit {d : ℕ} (hd : 0 < d) (kappa : MultiIndex d) (U : Skappa d kappa) : BoxPartialSumsLocallyUniformTo kappa U (toFun kappa U)

theorem DimdPolyLEAN.toL2_eq_boxLimit {d : ℕ} (hd : 0 < d) (kappa : MultiIndex d) (U : Skappa d kappa) : L2BoxPartialSumsTendTo kappa U (toL2 kappa U)

theorem DimdPolyLEAN.continuous_limit_of_locallyUniform_boxPartialSums {d : ℕ} (hd : 0 < d) (kappa : MultiIndex d) (U : Skappa d kappa) {f : Cd d → ℂ} (hlim : BoxPartialSumsLocallyUniformTo kappa U f) : Continuous f

theorem DimdPolyLEAN.toFun_as_L2_eq_boxLimit {d : ℕ} (hd : 0 < d) (kappa : MultiIndex d) (U : Skappa d kappa) : IsTensorL2Rep (toL2 kappa U) (toFun kappa U)

theorem DimdPolyLEAN.toFun_represents_toL2 {d : ℕ} (hd : 0 < d) (kappa : MultiIndex d) (U : Skappa d kappa) : IsTensorL2Rep (toL2 kappa U) (toFun kappa U)

theorem DimdPolyLEAN.coeff_recovery {d : ℕ} (hd : 0 < d) (kappa : MultiIndex d) (U : Skappa d kappa) (beta : Idx d) : coeffSkappa U beta = inner ℂ (PhiL2 kappa beta) (toL2 kappa U)

theorem DimdPolyLEAN.toL2_eq_of_toFun_eq {d : ℕ} (hd : 0 < d) {kappa : MultiIndex d} {U V : Skappa d kappa} (h : ∀ (z : Cd d), toFun kappa U z = toFun kappa V z) : toL2 kappa U = toL2 kappa V

theorem DimdPolyLEAN.skappa_ext_of_coeff_eq {d : ℕ} {kappa : MultiIndex d} {U V : Skappa d kappa} (hcoeff : ∀ (alpha : Idx d), coeffSkappa U alpha = coeffSkappa V alpha) : U = V

theorem DimdPolyLEAN.continuous_toFun {d : ℕ} (hd : 0 < d) (kappa : MultiIndex d) (U : Skappa d kappa) : Continuous (toFun kappa U)

theorem DimdPolyLEAN.toFun_smul_complex {d : ℕ} (kappa : MultiIndex d) (w : ℂ) (U : Skappa d kappa) : toFun kappa (w • U) = fun (z : Cd d) => w * toFun kappa U z

theorem DimdPolyLEAN.skappa_ext_of_toFun_eq {d : ℕ} (hd : 0 < d) {kappa : MultiIndex d} {U V : Skappa d kappa} (h : ∀ (z : Cd d), toFun kappa U z = toFun kappa V z) : U = V