Definitions

@[reducible, inline]

abbrev DimdPolyLEAN.Cd (d : ℕ) : Type

Cd d: the complex coordinate space Fin d → ℂ (d-dimensional).

Equations

• DimdPolyLEAN.Cd d = (Fin d → ℂ)

@[reducible, inline]

abbrev DimdPolyLEAN.MultiIndex (d : ℕ) : Type

MultiIndex d: a d-tuple of natural-number indices, Fin d → ℕ.

Equations

• DimdPolyLEAN.MultiIndex d = (Fin d → ℕ)

@[reducible, inline]

abbrev DimdPolyLEAN.Idx (d : ℕ) : Type

Idx d: the index set for Hermite-Fock coefficient arrays, equal to MultiIndex d.

Equations

• DimdPolyLEAN.Idx d = DimdPolyLEAN.MultiIndex d

@[reducible, inline]

abbrev DimdPolyLEAN.CircleFreq : Type

CircleFreq: an integer Fourier frequency on the circle.

Equations

• DimdPolyLEAN.CircleFreq = ℤ

@[reducible, inline]

abbrev DimdPolyLEAN.CircleTrigPoly : Type

CircleTrigPoly: a finite complex trigonometric polynomial on the circle, as a finitely supported map from frequencies to coefficients.

Equations

• DimdPolyLEAN.CircleTrigPoly = (DimdPolyLEAN.CircleFreq →₀ ℂ)

@[reducible, inline]

abbrev DimdPolyLEAN.Pkappa (d : ℕ) (kappa : MultiIndex d) : Type

Pkappa d kappa: the space of finite Hermite-Fock coefficient arrays at level kappa, namely finitely supported maps Idx d → ℂ.

Equations

• DimdPolyLEAN.Pkappa d kappa = (fun (x : DimdPolyLEAN.MultiIndex d) => DimdPolyLEAN.Idx d →₀ ℂ) kappa

theorem DimdPolyLEAN.Pkappa.ext {d : ℕ} {kappa : MultiIndex d} {F G : Pkappa d kappa} (h : ∀ (a : Idx d), F a = G a) : F = G

Two Pkappa d kappa coefficient arrays agreeing pointwise are equal.

theorem DimdPolyLEAN.Pkappa.ext_iff {d : ℕ} {kappa : MultiIndex d} {F G : Pkappa d kappa} : F = G ↔ ∀ (a : Idx d), F a = G a

structure DimdPolyLEAN.Skappa (d : ℕ) (kappa : MultiIndex d) : Type

Skappa d kappa: a square-summable Hermite-Fock coefficient array at level kappa (the ℓ² completion datum behind the Gaussian L² closure).

• coeff : Idx d → ℂ

  The coefficient of each multi-index.

• summable_norm_sq : Summable fun (alpha : Idx d) => ‖self.coeff alpha‖ ^ 2

  The coefficients are square-summable.

instance DimdPolyLEAN.instFactLtRealOfNatHMulPi_leanPool : Fact (0 < 2 * Real.pi)

noncomputable def DimdPolyLEAN.gaussianDensity (d : ℕ) (z : Cd d) : ℝ

gaussianDensity: gaussian Density.

Equations

• DimdPolyLEAN.gaussianDensity d z = 1 / Real.pi ^ d * Real.exp (-∑ q : Fin d, ‖z q‖ ^ 2)

noncomputable def DimdPolyLEAN.gammaD (d : ℕ) : MeasureTheory.Measure (Cd d)

gammaD: gamma d.

Equations

• DimdPolyLEAN.gammaD d = MeasureTheory.volume.withDensity fun (z : DimdPolyLEAN.Cd d) => ENNReal.ofReal (DimdPolyLEAN.gaussianDensity d z)

@[reducible, inline]

noncomputable abbrev DimdPolyLEAN.L2Tensor (d : ℕ) : AddSubgroup (Cd d →ₘ[gammaD d] ℂ)

L2Tensor: L2 Tensor.

Equations

• DimdPolyLEAN.L2Tensor d = MeasureTheory.Lp ℂ 2 (DimdPolyLEAN.gammaD d)

def DimdPolyLEAN.complexHermite (m n : ℕ) (z : ℂ) : ℂ

complexHermite: complex Hermite.

Equations

• DimdPolyLEAN.complexHermite m n z = ∑ j ∈ Finset.range (min m n + 1), (-1) ^ j * ↑j.factorial * ↑(m.choose j) * ↑(n.choose j) * z ^ (m - j) * star z ^ (n - j)

noncomputable def DimdPolyLEAN.phi1D (k n : ℕ) (z : ℂ) : ℂ

phi1D: phi1 D.

Equations

• DimdPolyLEAN.phi1D k n z = (↑√(↑n.factorial * ↑k.factorial))⁻¹ * DimdPolyLEAN.complexHermite n k z

noncomputable def DimdPolyLEAN.Phi {d : ℕ} (kappa : MultiIndex d) (alpha : Idx d) (z : Cd d) : ℂ

Phi: Phi.

Equations

• DimdPolyLEAN.Phi kappa alpha z = ∏ q : Fin d, DimdPolyLEAN.phi1D (kappa q) (alpha q) (z q)

def DimdPolyLEAN.box {d : ℕ} (J : MultiIndex d) : Finset (Idx d)

box: box.

Equations

• DimdPolyLEAN.box J = Fintype.piFinset fun (q : Fin d) => Finset.range (J q + 1)

@[implicit_reducible]

noncomputable instance DimdPolyLEAN.instNormCircleTrigPoly : Norm CircleTrigPoly

Equations

• DimdPolyLEAN.instNormCircleTrigPoly = { norm := fun (p : DimdPolyLEAN.CircleTrigPoly) => √(∑ n ∈ p.support, ‖p n‖ ^ 2) }

@[implicit_reducible]

noncomputable instance DimdPolyLEAN.instNormPkappa {d : ℕ} {kappa : MultiIndex d} : Norm (Pkappa d kappa)

Equations

• DimdPolyLEAN.instNormPkappa = { norm := fun (F : DimdPolyLEAN.Pkappa d kappa) => √(∑ alpha ∈ F.support, ‖F alpha‖ ^ 2) }

@[implicit_reducible]

instance DimdPolyLEAN.instZeroSkappa {d : ℕ} {kappa : MultiIndex d} : Zero (Skappa d kappa)

Equations

• DimdPolyLEAN.instZeroSkappa = { zero := { coeff := fun (x : DimdPolyLEAN.Idx d) => 0, summable_norm_sq := ⋯ } }

@[implicit_reducible]

instance DimdPolyLEAN.instSMulComplexSkappa {d : ℕ} {kappa : MultiIndex d} : SMul ℂ (Skappa d kappa)

Equations

• DimdPolyLEAN.instSMulComplexSkappa = { smul := fun (c : ℂ) (u : DimdPolyLEAN.Skappa d kappa) => { coeff := fun (alpha : DimdPolyLEAN.Idx d) => c * u.coeff alpha, summable_norm_sq := ⋯ } }

def DimdPolyLEAN.coeffPkappa {d : ℕ} {kappa : MultiIndex d} (F : Pkappa d kappa) (alpha : Idx d) : ℂ

coeffPkappa: coeff Pkappa.

Equations

• DimdPolyLEAN.coeffPkappa F alpha = F alpha

def DimdPolyLEAN.coeffSkappa {d : ℕ} {kappa : MultiIndex d} (F : Skappa d kappa) (alpha : Idx d) : ℂ

coeffSkappa: coeff Skappa.

Equations

• DimdPolyLEAN.coeffSkappa F alpha = F.coeff alpha

noncomputable def DimdPolyLEAN.evalPkappa {d : ℕ} (kappa : MultiIndex d) (F : Pkappa d kappa) : Cd d → ℂ

evalPkappa: eval Pkappa.

Equations

• DimdPolyLEAN.evalPkappa kappa F z = Finsupp.sum F fun (alpha : DimdPolyLEAN.Idx d) (c : ℂ) => c * DimdPolyLEAN.Phi kappa alpha z

noncomputable def DimdPolyLEAN.toFun {d : ℕ} (kappa : MultiIndex d) (F : Skappa d kappa) : Cd d → ℂ

toFun: to Fun.

Equations

• DimdPolyLEAN.toFun kappa F z = ∑' (alpha : DimdPolyLEAN.Idx d), DimdPolyLEAN.coeffSkappa F alpha * DimdPolyLEAN.Phi kappa alpha z

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

toL2: to L2.

Equations

• DimdPolyLEAN.toL2 kappa F = if h : MeasureTheory.MemLp (DimdPolyLEAN.toFun kappa F) 2 (DimdPolyLEAN.gammaD d) then MeasureTheory.MemLp.toLp (DimdPolyLEAN.toFun kappa F) h else 0

def DimdPolyLEAN.ofPkappa {d : ℕ} (kappa : MultiIndex d) (F : Pkappa d kappa) : Skappa d kappa

ofPkappa: of Pkappa.

Equations

• DimdPolyLEAN.ofPkappa kappa F = { coeff := fun (alpha : DimdPolyLEAN.Idx d) => F alpha, summable_norm_sq := ⋯ }

def DimdPolyLEAN.projFinset {d : ℕ} {kappa : MultiIndex d} (E : Finset (Idx d)) (F : Pkappa d kappa) : Pkappa d kappa

projFinset: proj Finset.

Equations

• DimdPolyLEAN.projFinset E F = Finsupp.filter (fun (alpha : DimdPolyLEAN.Idx d) => alpha ∈ E) F

noncomputable def DimdPolyLEAN.truncateFinset {d : ℕ} {kappa : MultiIndex d} (E : Finset (Idx d)) (F : Skappa d kappa) : Pkappa d kappa

truncateFinset: truncate Finset.

Equations

• DimdPolyLEAN.truncateFinset E F = ∑ alpha ∈ E, Finsupp.single alpha (DimdPolyLEAN.coeffSkappa F alpha)

noncomputable def DimdPolyLEAN.rotateCoord {d : ℕ} (q : Fin d) (t : ℝ) (z : Cd d) : Cd d

rotateCoord: rotate Coord.

Equations

• DimdPolyLEAN.rotateCoord q t z = Function.update z q (Complex.exp (↑t * Complex.I) * z q)

def DimdPolyLEAN.pkappaInner {d : ℕ} {kappa : MultiIndex d} (F G : Pkappa d kappa) : ℂ

pkappaInner: pkappa Inner.

Equations

• DimdPolyLEAN.pkappaInner F G = Finsupp.sum F fun (alpha : DimdPolyLEAN.Idx d) (c : ℂ) => c * star (G alpha)

def DimdPolyLEAN.basePointNormalized {d : ℕ} {kappa : MultiIndex d} (F : Pkappa d kappa) : Prop

basePointNormalized: base Point Normalized.

Equations

• DimdPolyLEAN.basePointNormalized F = (F ≠ 0 ∧ ‖F‖ = 1)

def DimdPolyLEAN.orthogonalToPk {d : ℕ} {kappa : MultiIndex d} (F G : Pkappa d kappa) : Prop

orthogonalToPk: orthogonal To Pk.

Equations

• DimdPolyLEAN.orthogonalToPk F G = (DimdPolyLEAN.pkappaInner G F = 0)

def DimdPolyLEAN.positivePhaseGauge {d : ℕ} {kappa : MultiIndex d} (F Q : Pkappa d kappa) : Prop

The positive phase gauge for a fixed base point F.

The coefficient of Q in the F direction is required to be a nonnegative real number. This is the global gauge needed for a no-δ, lambda = 1 stability statement: the weaker local real gauge would still allow Q = -F.

Equations

• DimdPolyLEAN.positivePhaseGauge F Q = ((DimdPolyLEAN.pkappaInner Q F).im = 0 ∧ 0 ≤ (DimdPolyLEAN.pkappaInner Q F).re)

noncomputable def DimdPolyLEAN.defect {d : ℕ} {kappa : MultiIndex d} (F G : Pkappa d kappa) : ℝ

defect: defect.

Equations

• DimdPolyLEAN.defect F G = √(∫ (z : DimdPolyLEAN.Cd d), (‖DimdPolyLEAN.evalPkappa kappa (F + G) z‖ - ‖DimdPolyLEAN.evalPkappa kappa F z‖) ^ 2 ∂DimdPolyLEAN.gammaD d)

def DimdPolyLEAN.productAnnulus {d : ℕ} (j : Idx d) : Set (Cd d)

productAnnulus: product Annulus.

Equations

• DimdPolyLEAN.productAnnulus j = {z : DimdPolyLEAN.Cd d | ∀ (q : Fin d), ↑(j q) ≤ ‖z q‖ ∧ ‖z q‖ < ↑(j q) + 1}

noncomputable def DimdPolyLEAN.annulusMass {d : ℕ} {kappa : MultiIndex d} (j : Idx d) (F : Skappa d kappa) : ℝ

annulusMass: annulus Mass.

Equations

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

def DimdPolyLEAN.lowAnnuli (d J : ℕ) : Finset (Idx d)

lowAnnuli: low Annuli.

Equations

• DimdPolyLEAN.lowAnnuli d J = Fintype.piFinset fun (x : Fin d) => Finset.range J

noncomputable def DimdPolyLEAN.lowAnnulusMass {d : ℕ} {kappa : MultiIndex d} (J : ℕ) (F : Skappa d kappa) : ℝ

lowAnnulusMass: low Annulus Mass.

Equations

• DimdPolyLEAN.lowAnnulusMass J F = ∑ j ∈ DimdPolyLEAN.lowAnnuli d J, DimdPolyLEAN.annulusMass j F

noncomputable def DimdPolyLEAN.highAnnulusMass {d : ℕ} {kappa : MultiIndex d} (J : ℕ) (F : Skappa d kappa) : ℝ

highAnnulusMass: high Annulus Mass.

Equations

• DimdPolyLEAN.highAnnulusMass J F = ∫ (z : DimdPolyLEAN.Cd d), ‖DimdPolyLEAN.toFun kappa F z‖ ^ 2 ∂DimdPolyLEAN.gammaD d - DimdPolyLEAN.lowAnnulusMass J F

def DimdPolyLEAN.coefficientRadius {d : ℕ} (alpha : Idx d) : ℕ

coefficientRadius: coefficient Radius.

Equations

• DimdPolyLEAN.coefficientRadius alpha = Finset.univ.sup alpha

noncomputable def DimdPolyLEAN.highAnnulusEnergy {d : ℕ} {kappa : MultiIndex d} (J : ℕ) (F : Pkappa d kappa) : ℝ

highAnnulusEnergy: high Annulus Energy.

Equations

• DimdPolyLEAN.highAnnulusEnergy J F = DimdPolyLEAN.highAnnulusMass J (DimdPolyLEAN.ofPkappa kappa F)

noncomputable def DimdPolyLEAN.lowBlockLeakage {d : ℕ} {kappa : MultiIndex d} (J : ℕ) (F : Pkappa d kappa) : ℝ

lowBlockLeakage: low Block Leakage.

Equations

• DimdPolyLEAN.lowBlockLeakage J F = DimdPolyLEAN.lowAnnulusMass J (DimdPolyLEAN.ofPkappa kappa F)

def DimdPolyLEAN.supportRadius {d : ℕ} {kappa : MultiIndex d} (F : Pkappa d kappa) : ℕ

supportRadius: support Radius.

Equations

• DimdPolyLEAN.supportRadius F = F.support.sup DimdPolyLEAN.coefficientRadius

def DimdPolyLEAN.Jann {d : ℕ} {kappa : MultiIndex d} (F : Pkappa d kappa) : ℕ

Jann: Jann.

Equations

• DimdPolyLEAN.Jann F = DimdPolyLEAN.supportRadius F + 1

noncomputable def DimdPolyLEAN.Cann {d : ℕ} {kappa : MultiIndex d} (F : Pkappa d kappa) : ℝ

Cann: Cann.

Equations

• DimdPolyLEAN.Cann F = ‖F‖ ^ 2 + ↑(DimdPolyLEAN.Jann F) + 1

noncomputable def DimdPolyLEAN.Cleak {d : ℕ} {kappa : MultiIndex d} (F : Pkappa d kappa) : ℝ

Cleak: Cleak.

Equations

• DimdPolyLEAN.Cleak F = ‖F‖ + ↑F.support.card + 1

noncomputable def DimdPolyLEAN.deltaRig {d : ℕ} {kappa : MultiIndex d} (F : Pkappa d kappa) (E : Finset (Idx d)) (rho : ℝ) : ℝ

deltaRig: delta Rig.

Equations

• DimdPolyLEAN.deltaRig F E rho = rho / ↑(DimdPolyLEAN.Jann F + E.card + 1)

noncomputable def DimdPolyLEAN.Cperp {d : ℕ} {kappa : MultiIndex d} (F : Pkappa d kappa) : ℝ

Cperp: Cperp.

Equations

• DimdPolyLEAN.Cperp F = DimdPolyLEAN.Cann F + DimdPolyLEAN.Cleak F

noncomputable def DimdPolyLEAN.evalCircle (p : CircleTrigPoly) : AddCircle (2 * Real.pi) → ℂ

evalCircle: eval Circle.

Equations

• DimdPolyLEAN.evalCircle p t = ∑ n ∈ p.support, p n * ↑(n • t).toCircle

def DimdPolyLEAN.oneSidedLowFreq (p : CircleTrigPoly) (D : ℕ) : Prop

oneSidedLowFreq: one Sided Low Freq.

Equations

• DimdPolyLEAN.oneSidedLowFreq p D = ∀ n ∈ p.support, 0 ≤ n ∧ n ≤ ↑D

def DimdPolyLEAN.highBandSupport (q : CircleTrigPoly) (N B : ℕ) : Prop

highBandSupport: high Band Support.

Equations

• DimdPolyLEAN.highBandSupport q N B = ∀ n ∈ q.support, ↑N ≤ n ∧ n < ↑N + ↑B

def DimdPolyLEAN.gapCircle (D : ℕ) : ℕ

gapCircle: gap Circle.

Equations

• DimdPolyLEAN.gapCircle D = D + 1

noncomputable def DimdPolyLEAN.defectCircle (p q : CircleTrigPoly) : ℝ

defectCircle: defect Circle.

Equations

• DimdPolyLEAN.defectCircle p q = √(∫ (t : AddCircle (2 * Real.pi)), (‖DimdPolyLEAN.evalCircle (p + q) t‖ - ‖DimdPolyLEAN.evalCircle p t‖) ^ 2 ∂AddCircle.haarAddCircle)

noncomputable def DimdPolyLEAN.Ccircle (p : CircleTrigPoly) (D N B : ℕ) : ℝ

Ccircle: Ccircle.

Equations

• DimdPolyLEAN.Ccircle p D N B = ‖p‖ + ↑(D + N + B + 1)