Definitions

@[reducible, inline]

abbrev Hermite1DimdLEAN.CSpace (d : ℕ) : Type

CSpace: C Space.

Equations

• Hermite1DimdLEAN.CSpace d = (Fin d → ℂ)

@[reducible, inline]

abbrev Hermite1DimdLEAN.MultiIndex (d : ℕ) : Type

MultiIndex: Multi Index.

Equations

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

@[reducible, inline]

noncomputable abbrev Hermite1DimdLEAN.T : ℝ

T: T.

Equations

• Hermite1DimdLEAN.T = HermiteLEAN.T

theorem Hermite1DimdLEAN.T_pos : 0 < T

instance Hermite1DimdLEAN.instFactLtRealOfNatT : Fact (0 < T)

@[reducible, inline]

abbrev Hermite1DimdLEAN.Circle : Type

Circle: Circle.

Equations

• Hermite1DimdLEAN.Circle = AddCircle Hermite1DimdLEAN.T

noncomputable def Hermite1DimdLEAN.gaussianDensity (d : ℕ) (z : CSpace d) : ℝ

gaussianDensity: gaussian Density.

Equations

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

noncomputable def Hermite1DimdLEAN.gaussianMeasure (d : ℕ) : MeasureTheory.Measure (CSpace d)

gaussianMeasure: gaussian Measure.

Equations

• Hermite1DimdLEAN.gaussianMeasure d = MeasureTheory.volume.withDensity fun (z : Hermite1DimdLEAN.CSpace d) => ENNReal.ofReal (Hermite1DimdLEAN.gaussianDensity d z)

noncomputable def Hermite1DimdLEAN.oneDimPhi (k n : ℕ) : ℂ → ℂ

oneDimPhi: one Dim Phi.

Equations

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

noncomputable def Hermite1DimdLEAN.PhiKappaAlpha {d : ℕ} (κ α : MultiIndex d) : CSpace d → ℂ

PhiKappaAlpha: Phi Kappa Alpha.

Equations

• Hermite1DimdLEAN.PhiKappaAlpha κ α z = ∏ q : Fin d, Hermite1DimdLEAN.oneDimPhi (κ q) (α q) (z q)

noncomputable def Hermite1DimdLEAN.nuKappa {d : ℕ} (κ : MultiIndex d) : CSpace d → ℂ

nuKappa: nu Kappa.

Equations

• Hermite1DimdLEAN.nuKappa κ = Hermite1DimdLEAN.PhiKappaAlpha κ 0

noncomputable def Hermite1DimdLEAN.rho (a u : ℂ) : ℝ

rho: rho.

Equations

• Hermite1DimdLEAN.rho a u = |‖a + u‖ - ‖a‖|

noncomputable def Hermite1DimdLEAN.gaussianL2NormSq {d : ℕ} {α : Type u_1} [Norm α] (F : CSpace d → α) : ℝ

gaussianL2NormSq: gaussian L2 Norm Sq.

Equations

• Hermite1DimdLEAN.gaussianL2NormSq F = ∫ (z : Hermite1DimdLEAN.CSpace d), ‖F z‖ ^ 2 ∂Hermite1DimdLEAN.gaussianMeasure d

noncomputable def Hermite1DimdLEAN.gaussianL2Norm {d : ℕ} {α : Type u_1} [Norm α] (F : CSpace d → α) : ℝ

gaussianL2Norm: gaussian L2 Norm.

Equations

• Hermite1DimdLEAN.gaussianL2Norm F = √(Hermite1DimdLEAN.gaussianL2NormSq F)

noncomputable def Hermite1DimdLEAN.gaussianInner {d : ℕ} (F G : CSpace d → ℂ) : ℂ

gaussianInner: gaussian Inner.

Equations

• Hermite1DimdLEAN.gaussianInner F G = ∫ (z : Hermite1DimdLEAN.CSpace d), F z * (starRingEnd ℂ) (G z) ∂Hermite1DimdLEAN.gaussianMeasure d

noncomputable def Hermite1DimdLEAN.circleL2NormSq {α : Type u_1} [Norm α] (F : Circle → α) : ℝ

circleL2NormSq: circle L2 Norm Sq.

Equations

• Hermite1DimdLEAN.circleL2NormSq F = ∫ (t : AddCircle Hermite1DimdLEAN.T), ‖F t‖ ^ 2 ∂AddCircle.haarAddCircle

noncomputable def Hermite1DimdLEAN.circleL2Norm {α : Type u_1} [Norm α] (F : Circle → α) : ℝ

circleL2Norm: circle L2 Norm.

Equations

• Hermite1DimdLEAN.circleL2Norm F = √(Hermite1DimdLEAN.circleL2NormSq F)

structure Hermite1DimdLEAN.FiniteHermiteSum (d : ℕ) : Type

FiniteHermiteSum: Finite Hermite Sum.

• coeff : MultiIndex d →₀ ℂ

  coeff: coeff.

def Hermite1DimdLEAN.FiniteHermiteSum.support {d : ℕ} (G : FiniteHermiteSum d) : Finset (MultiIndex d)

support: support.

Equations

• G.support = G.coeff.support

noncomputable def Hermite1DimdLEAN.evalHermiteSum {d : ℕ} (κ : MultiIndex d) (G : FiniteHermiteSum d) : CSpace d → ℂ

evalHermiteSum: eval Hermite Sum.

Equations

• Hermite1DimdLEAN.evalHermiteSum κ G z = ∑ α ∈ G.support, G.coeff α * Hermite1DimdLEAN.PhiKappaAlpha κ α z

noncomputable def Hermite1DimdLEAN.hermiteInner {d : ℕ} (κ : MultiIndex d) (G H : FiniteHermiteSum d) : ℂ

hermiteInner: hermite Inner.

Equations

• Hermite1DimdLEAN.hermiteInner κ G H = Hermite1DimdLEAN.gaussianInner (Hermite1DimdLEAN.evalHermiteSum κ G) (Hermite1DimdLEAN.evalHermiteSum κ H)

noncomputable def Hermite1DimdLEAN.hermiteInnerNu {d : ℕ} (κ : MultiIndex d) (G : FiniteHermiteSum d) : ℂ

hermiteInnerNu: hermite Inner Nu.

Equations

• Hermite1DimdLEAN.hermiteInnerNu κ G = Hermite1DimdLEAN.gaussianInner (Hermite1DimdLEAN.evalHermiteSum κ G) (Hermite1DimdLEAN.nuKappa κ)

noncomputable def Hermite1DimdLEAN.hermiteNormSq {d : ℕ} (κ : MultiIndex d) (G : FiniteHermiteSum d) : ℝ

hermiteNormSq: hermite Norm Sq.

Equations

• Hermite1DimdLEAN.hermiteNormSq κ G = Hermite1DimdLEAN.gaussianL2NormSq (Hermite1DimdLEAN.evalHermiteSum κ G)

noncomputable def Hermite1DimdLEAN.hermiteNorm {d : ℕ} (κ : MultiIndex d) (G : FiniteHermiteSum d) : ℝ

hermiteNorm: hermite Norm.

Equations

• Hermite1DimdLEAN.hermiteNorm κ G = Hermite1DimdLEAN.gaussianL2Norm (Hermite1DimdLEAN.evalHermiteSum κ G)

noncomputable def Hermite1DimdLEAN.defectFunction {d : ℕ} (κ : MultiIndex d) (G : FiniteHermiteSum d) : CSpace d → ℝ

defectFunction: defect Function.

Equations

• Hermite1DimdLEAN.defectFunction κ G z = Hermite1DimdLEAN.rho (Hermite1DimdLEAN.nuKappa κ z) (Hermite1DimdLEAN.evalHermiteSum κ G z)

noncomputable def Hermite1DimdLEAN.defectNormSq {d : ℕ} (κ : MultiIndex d) (G : FiniteHermiteSum d) : ℝ

defectNormSq: defect Norm Sq.

Equations

• Hermite1DimdLEAN.defectNormSq κ G = Hermite1DimdLEAN.gaussianL2NormSq (Hermite1DimdLEAN.defectFunction κ G)

noncomputable def Hermite1DimdLEAN.defectNorm {d : ℕ} (κ : MultiIndex d) (G : FiniteHermiteSum d) : ℝ

defectNorm: defect Norm.

Equations

• Hermite1DimdLEAN.defectNorm κ G = Hermite1DimdLEAN.gaussianL2Norm (Hermite1DimdLEAN.defectFunction κ G)

def Hermite1DimdLEAN.totalDegree {d : ℕ} (α : MultiIndex d) : ℕ

totalDegree: total Degree.

Equations

• Hermite1DimdLEAN.totalDegree α = ∑ q : Fin d, α q

def Hermite1DimdLEAN.blockIndexMulti {d : ℕ} (α : MultiIndex d) : MultiIndex d

blockIndexMulti: block Index Multi.

Equations

• Hermite1DimdLEAN.blockIndexMulti α q = HermiteLEAN.blockIndex (α q)

noncomputable def Hermite1DimdLEAN.totalDegreePiece {d : ℕ} (n : ℕ) (G : FiniteHermiteSum d) : FiniteHermiteSum d

totalDegreePiece: total Degree Piece.

Equations

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

def Hermite1DimdLEAN.productAnnulus {d : ℕ} (j : MultiIndex d) : Set (CSpace d)

productAnnulus: product Annulus.

Equations

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

noncomputable def Hermite1DimdLEAN.indicatorMul {α : Type u_1} (s : Set α) (f : α → ℂ) : α → ℂ

indicatorMul: the indicator of s times f, valued in ℂ.

Equations

• Hermite1DimdLEAN.indicatorMul s f x = if x ∈ s then f x else 0

noncomputable def Hermite1DimdLEAN.annulusInner {d : ℕ} (j : MultiIndex d) (F G : CSpace d → ℂ) : ℂ

annulusInner: annulus Inner.

Equations

• Hermite1DimdLEAN.annulusInner j F G = ∫ (z : Hermite1DimdLEAN.CSpace d), if z ∈ Hermite1DimdLEAN.productAnnulus j then F z * (starRingEnd ℂ) (G z) else 0 ∂Hermite1DimdLEAN.gaussianMeasure d

noncomputable def Hermite1DimdLEAN.annulusMass {d : ℕ} (j : MultiIndex d) (F : CSpace d → ℂ) : ℝ

annulusMass: annulus Mass.

Equations

• Hermite1DimdLEAN.annulusMass j F = ∫ (z : Hermite1DimdLEAN.CSpace d), if z ∈ Hermite1DimdLEAN.productAnnulus j then ‖F z‖ ^ 2 else 0 ∂Hermite1DimdLEAN.gaussianMeasure d

noncomputable def Hermite1DimdLEAN.defectAnnulusMass {d : ℕ} (κ j : MultiIndex d) (F : CSpace d → ℂ) : ℝ

defectAnnulusMass: defect Annulus Mass.

Equations

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

def Hermite1DimdLEAN.squareBlock {d : ℕ} (ℓ : MultiIndex d) : Set (MultiIndex d)

squareBlock: square Block.

Equations

• Hermite1DimdLEAN.squareBlock ℓ = {α : Hermite1DimdLEAN.MultiIndex d | ∀ (q : Fin d), α q ∈ HermiteLEAN.squareBlock (ℓ q)}

def Hermite1DimdLEAN.blockDistance {d : ℕ} (j ℓ : MultiIndex d) : ℕ

blockDistance: block Distance.

Equations

• Hermite1DimdLEAN.blockDistance j ℓ = Finset.univ.sup fun (q : Fin d) => (j q).dist (ℓ q)

noncomputable def Hermite1DimdLEAN.blockPart {d : ℕ} (ℓ : MultiIndex d) (G : FiniteHermiteSum d) : FiniteHermiteSum d

blockPart: block Part.

Equations

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

def Hermite1DimdLEAN.localCoeffSet {d : ℕ} (j : MultiIndex d) (M : ℕ) (G : FiniteHermiteSum d) : Finset (MultiIndex d)

localCoeffSet: local Coeff Set.

Equations

• Hermite1DimdLEAN.localCoeffSet j M G = {α ∈ G.support | Hermite1DimdLEAN.blockDistance j (Hermite1DimdLEAN.blockIndexMulti α) ≤ M}

def Hermite1DimdLEAN.farCoeffSet {d : ℕ} (j : MultiIndex d) (M : ℕ) (G : FiniteHermiteSum d) : Finset (MultiIndex d)

farCoeffSet: far Coeff Set.

Equations

• Hermite1DimdLEAN.farCoeffSet j M G = {α ∈ G.support | M < Hermite1DimdLEAN.blockDistance j (Hermite1DimdLEAN.blockIndexMulti α)}

noncomputable def Hermite1DimdLEAN.localPart {d : ℕ} (j : MultiIndex d) (M : ℕ) (G : FiniteHermiteSum d) : FiniteHermiteSum d

localPart: local Part.

Equations

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

noncomputable def Hermite1DimdLEAN.remainderPart {d : ℕ} (j : MultiIndex d) (M : ℕ) (G : FiniteHermiteSum d) : FiniteHermiteSum d

remainderPart: remainder Part.

Equations

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

def Hermite1DimdLEAN.localDegreeSet {d : ℕ} (j : MultiIndex d) (M : ℕ) (G : FiniteHermiteSum d) : Finset ℕ

localDegreeSet: local Degree Set.

Equations

• Hermite1DimdLEAN.localDegreeSet j M G = Finset.image Hermite1DimdLEAN.totalDegree (Hermite1DimdLEAN.localCoeffSet j M G)

noncomputable def Hermite1DimdLEAN.localDegreePiece {d : ℕ} (j : MultiIndex d) (M n : ℕ) (G : FiniteHermiteSum d) : FiniteHermiteSum d

localDegreePiece: local Degree Piece.

Equations

• Hermite1DimdLEAN.localDegreePiece j M n G = Hermite1DimdLEAN.totalDegreePiece n (Hermite1DimdLEAN.localPart j M G)

def Hermite1DimdLEAN.degreeIntervalLower {d : ℕ} (j : MultiIndex d) (M : ℕ) : ℕ

degreeIntervalLower: degree Interval Lower.

Equations

• Hermite1DimdLEAN.degreeIntervalLower j M = ∑ q : Fin d, (max (j q) M - M) ^ 2

def Hermite1DimdLEAN.degreeIntervalUpper {d : ℕ} (j : MultiIndex d) (M : ℕ) : ℕ

degreeIntervalUpper: degree Interval Upper.

Equations

• Hermite1DimdLEAN.degreeIntervalUpper j M = ∑ q : Fin d, ((j q + M + 1) ^ 2 - 1)

def Hermite1DimdLEAN.degreeWidth {d : ℕ} (j : MultiIndex d) (M : ℕ) : ℕ

degreeWidth: degree Width.

Equations

• Hermite1DimdLEAN.degreeWidth j M = Hermite1DimdLEAN.degreeIntervalUpper j M - Hermite1DimdLEAN.degreeIntervalLower j M + 1

def Hermite1DimdLEAN.annulusRadius {d : ℕ} (j : MultiIndex d) : ℕ

annulusRadius: annulus Radius.

Equations

• Hermite1DimdLEAN.annulusRadius j = Finset.univ.sup fun (q : Fin d) => j q

def Hermite1DimdLEAN.degreeThreshold (d M : ℕ) : ℕ

degreeThreshold: degree Threshold.

Equations

• Hermite1DimdLEAN.degreeThreshold d M = M + 120 * d * (2 * M + 1)

noncomputable def Hermite1DimdLEAN.productAnnulusConstant (d M : ℕ) : ℝ

productAnnulusConstant: product Annulus Constant.

Equations

• Hermite1DimdLEAN.productAnnulusConstant d M = 12 * √↑d * ↑(Hermite1DimdLEAN.degreeThreshold d M + M)

def Hermite1DimdLEAN.productAnnulusConstantSq (d M : ℕ) : ℝ

productAnnulusConstantSq: product Annulus Constant Sq.

Equations

• Hermite1DimdLEAN.productAnnulusConstantSq d M = 144 * ↑d * ↑(Hermite1DimdLEAN.degreeThreshold d M + M) ^ 2

def Hermite1DimdLEAN.prodLocalizationConstant {d : ℕ} (κ : MultiIndex d) : ℝ

prodLocalizationConstant: prod Localization Constant.

Equations

• Hermite1DimdLEAN.prodLocalizationConstant κ = ∏ q : Fin d, ↑(κ q + 1)

noncomputable def Hermite1DimdLEAN.prodLocalizationDecay {d : ℕ} (κ : MultiIndex d) : ℝ

prodLocalizationDecay: prod Localization Decay.

Equations

• Hermite1DimdLEAN.prodLocalizationDecay κ = (∏ q : Fin d, ↑(κ q + 1))⁻¹

def Hermite1DimdLEAN.prodLocalizationShift {d : ℕ} (κ : MultiIndex d) : ℝ

prodLocalizationShift: prod Localization Shift.

Equations

• Hermite1DimdLEAN.prodLocalizationShift κ = ∑ q : Fin d, ↑(κ q + 4)

def Hermite1DimdLEAN.shellCardinality (d r : ℕ) : ℕ

shellCardinality: shell Cardinality.

Equations

• Hermite1DimdLEAN.shellCardinality d r = (2 * r + 1) ^ d - (2 * r - 1) ^ d

noncomputable def Hermite1DimdLEAN.localizationLeakageCoefficient (C c B : ℝ) (d M : ℕ) : ℝ

localizationLeakageCoefficient: localization Leakage Coefficient.

Equations

• Hermite1DimdLEAN.localizationLeakageCoefficient C c B d M = C * ∑' (r : ℕ), if M + 1 ≤ r then ↑(Hermite1DimdLEAN.shellCardinality d r) * Real.exp (-c * max (↑r - B) 0 ^ 2) else 0

noncomputable def Hermite1DimdLEAN.leakageCoefficient {d : ℕ} (κ : MultiIndex d) (M : ℕ) : ℝ

leakageCoefficient: leakage Coefficient.

Equations

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

def Hermite1DimdLEAN.absorptionPredicate {d : ℕ} (κ : MultiIndex d) (M : ℕ) : Prop

absorptionPredicate: absorption Predicate.

Equations

• Hermite1DimdLEAN.absorptionPredicate κ M = ((4 * Hermite1DimdLEAN.productAnnulusConstantSq d M + 2) * Hermite1DimdLEAN.leakageCoefficient κ M < 1 / 2)

noncomputable def Hermite1DimdLEAN.coercivityConstant {d : ℕ} (κ : MultiIndex d) (M : ℕ) : ℝ

coercivityConstant: coercivity Constant.

Equations

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

noncomputable def Hermite1DimdLEAN.reductionDelta (M : ℝ) : ℝ

reductionDelta: reduction Delta.

Equations

• Hermite1DimdLEAN.reductionDelta M = 1 / (M + 1)

def Hermite1DimdLEAN.reductionMtilde (M : ℝ) : ℝ

reductionMtilde: reduction Mtilde.

Equations

• Hermite1DimdLEAN.reductionMtilde M = 5 * M + 3

noncomputable def Hermite1DimdLEAN.phaseAdjustedDifference {d : ℕ} (κ : MultiIndex d) (w : ℂ) (G : FiniteHermiteSum d) : CSpace d → ℂ

phaseAdjustedDifference: phase Adjusted Difference.

Equations

• Hermite1DimdLEAN.phaseAdjustedDifference κ w G z = w * (Hermite1DimdLEAN.nuKappa κ z + Hermite1DimdLEAN.evalHermiteSum κ G z) - Hermite1DimdLEAN.nuKappa κ z

noncomputable def Hermite1DimdLEAN.phaseAdjustedNormSq {d : ℕ} (κ : MultiIndex d) (w : ℂ) (G : FiniteHermiteSum d) : ℝ

phaseAdjustedNormSq: phase Adjusted Norm Sq.

Equations

• Hermite1DimdLEAN.phaseAdjustedNormSq κ w G = Hermite1DimdLEAN.gaussianL2NormSq (Hermite1DimdLEAN.phaseAdjustedDifference κ w G)

noncomputable def Hermite1DimdLEAN.phaseAdjustedNorm {d : ℕ} (κ : MultiIndex d) (w : ℂ) (G : FiniteHermiteSum d) : ℝ

phaseAdjustedNorm: phase Adjusted Norm.

Equations

• Hermite1DimdLEAN.phaseAdjustedNorm κ w G = Hermite1DimdLEAN.gaussianL2Norm (Hermite1DimdLEAN.phaseAdjustedDifference κ w G)

noncomputable def Hermite1DimdLEAN.positiveFrequencyPolynomial (E : Finset ℕ) (b : ℕ → ℂ) : Circle → ℂ

positiveFrequencyPolynomial: positive Frequency Polynomial.

Equations

• Hermite1DimdLEAN.positiveFrequencyPolynomial E b t = ∑ n ∈ E, b n * (fourier ↑n) t

noncomputable def Hermite1DimdLEAN.bandLimitedPolynomial (N L : ℕ) (c : Fin L → ℂ) : Circle → ℂ

bandLimitedPolynomial: band Limited Polynomial.

Equations

• Hermite1DimdLEAN.bandLimitedPolynomial N L c t = ∑ m : Fin L, c m * (fourier ↑(N + ↑m)) t

def Hermite1DimdLEAN.HasPositiveFrequencySupport (P : Circle → ℂ) (E : Finset ℕ) : Prop

HasPositiveFrequencySupport: Has Positive Frequency Support.

Equations

• Hermite1DimdLEAN.HasPositiveFrequencySupport P E = ∃ (b : ℕ → ℂ), P = Hermite1DimdLEAN.positiveFrequencyPolynomial E b

def Hermite1DimdLEAN.HasBandlimitedSupport (P : Circle → ℂ) (N L : ℕ) : Prop

HasBandlimitedSupport: Has Bandlimited Support.

Equations

• Hermite1DimdLEAN.HasBandlimitedSupport P N L = ∃ (c : Fin L → ℂ), P = Hermite1DimdLEAN.bandLimitedPolynomial N L c