Gaussian frequency integration

Abstract

The original Gaussian density controls the zero-frequency quotient and the logarithmic singular H in actual symmetric product L2.

Definition 1.1 (Actual weighted measure).

$\forall c \in R e a l, \forall ka pp a \in R e a l, spatialMeasure (c, ka pp a) = withDensity (v o l u m e, (x : R e a l \mapsto ofReal (c \cdot exp (\frac{- ka pp a \cdot x ^{2}}{2}))))$

Formalization. D5/S3/Fourier/Asymptotics/GaussianFrequencyKernel.spatialMeasure (✓ std3).

Source. Repository-derived.

Acknowledgement. David Nualart and Giovanni Peccati (2005). Central limit theorems for sequences of multiple stochastic integrals. DOI: 10.1214/009117904000000621. URL: https://arxiv.org/pdf/math/0503598v1.

Commentary.

For arbitrary real c and kappa, spatialMeasure is the Lebesgue measure with density ofReal(c exp(-kappa x^2/2)). Positive kappa and nonnegative c are required only by the subsequent estimates.

Definition 1.2 (Gaussian normalization constant).

$\forall c \in R e a l, \forall ka pp a \in R e a l, spatialMass (c, ka pp a) = c \cdot sqrt (\frac{2 \cdot pi ( )}{ka pp a})$

Formalization. D5/S3/Fourier/Asymptotics/GaussianFrequencyKernel.spatialMass (✓ std3).

Source. Repository-derived.

Commentary.

The mass expression retains the unnormalized coefficient c.

Theorem 1.3 (Density normalization).

$\forall c \in R e a l, \forall ka pp a \in R e a l, \forall h c \in 0 \leq c, \forall hka pp a \in 0 < ka pp a, spatialMeasure (c, ka pp a) = smul (ofReal (spatialMass (c, ka pp a)), gaussianReal (0, toNNReal (\frac{1}{ka pp a})))$

Proof. Machine-checked in Lean as D5/S3/Fourier/Asymptotics/GaussianFrequencyKernel.spatialMeasure_normalized (✓ std3). ∎

Source. Repository-derived.

Commentary.

For c nonnegative and kappa positive, the actual weighted measure is its mass times the centered Gaussian probability measure with variance 1/kappa. This is an equality of measures derived from their densities, including c=0.

Theorem 1.4 (Original spatial mass).

$\forall c \in R e a l, \forall ka pp a \in R e a l, \forall h c \in 0 \leq c, \forall hka pp a \in 0 < ka pp a, spatialMass (c, ka pp a) = integral ((x : R e a l \mapsto c \cdot exp (\frac{- ka pp a \cdot x ^{2}}{2})), v o l u m e)$

Proof. Machine-checked in Lean as D5/S3/Fourier/Asymptotics/GaussianFrequencyKernel.spatialMass_eq_integral (✓ std3). ∎

Source. Repository-derived.

Commentary.

The normalization constant equals the integral of the original real density. Thus gamma is the actual unnormalized mass, rather than an imposed probability normalization.

Theorem 1.5 (Finite Gaussian weight).

$\forall c \in R e a l, \forall ka pp a \in R e a l, \forall h c \in 0 \leq c, \forall hka pp a \in 0 < ka pp a, IsFiniteMeasure (spatialMeasure (c, ka pp a))$

Proof. Machine-checked in Lean as D5/S3/Fourier/Asymptotics/GaussianFrequencyKernel.spatialMeasure_finite (✓ std3). ∎

Source. Repository-derived.

Commentary.

The density normalization supplies finiteness for every nonnegative c and positive kappa.

Theorem 1.6 (Product-coordinate difference law).

$\forall v \in NNR e a l, map (prod (gaussianReal (0, v), gaussianReal (0, v)), (z : Prod (R e a l, R e a l) \mapsto (fst (z) - snd (z)))) = gaussianReal (0, v + v)$

Proof. Machine-checked in Lean as D5/S3/Fourier/Asymptotics/GaussianFrequencyKernel.gaussian_difference_law (✓ std3). ∎

Source. Repository-derived.

Commentary.

Independent coordinates of the actual Gaussian product measure have centered difference law with variance 2v. The pinned Gaussian convolution and map theorems supply this statement, including v=0.

Theorem 1.7 (Reused scalar fourth moment).

$\forall v \in NNR e a l, integral ((x : R e a l \mapsto x^{4}), gaussianReal (0, v)) = 3 \cdot coe (v)^{2}$

Proof. Machine-checked in Lean as D5/S3/Fourier/Asymptotics/GaussianFrequencyKernel.gaussian_fourth (✓ std3). ∎

Source. Repository-derived.

Commentary.

The scalar fourth moment is 3v^2, using centralMoment_two_mul in its existing owner. Zero variance is included.

Theorem 1.8 (Exact fourth spatial difference moment).

$\forall c \in R e a l, \forall ka pp a \in R e a l, \forall h c \in 0 \leq c, \forall hka pp a \in 0 < ka pp a, integral ((z : Prod (R e a l, R e a l) \mapsto (fst (z) - snd (z))^{4}), prod (spatialMeasure (c, ka pp a), spatialMeasure (c, ka pp a))) = \frac{12 \cdot integral ( ( x : R e a l \mapsto c \cdot exp ( \frac{- ka pp a \cdot x ^{2}}{2} ) ) , v o l u m e ) ^{2}}{ka pp a ^{2}}$

Proof. Machine-checked in Lean as D5/S3/Fourier/Asymptotics/GaussianFrequencyKernel.spatial_difference_fourth (✓ std3). ∎

Source. Repository-derived.

Commentary.

The actual product-measure integral of (x-y)^4 is 12 gamma^2/kappa^2. Density normalization, the product-coordinate difference law and the existing scalar moment determine every constant.

Theorem 1.9 (Fourth difference integrability).

$\forall c \in R e a l, \forall ka pp a \in R e a l, \forall h c \in 0 \leq c, \forall hka pp a \in 0 < ka pp a, Integrable ((z : Prod (R e a l, R e a l) \mapsto (fst (z) - snd (z))^{4}), prod (spatialMeasure (c, ka pp a), spatialMeasure (c, ka pp a)))$

Proof. Machine-checked in Lean as D5/S3/Fourier/Asymptotics/GaussianFrequencyKernel.spatial_difference_fourth_integrable (✓ std3). ∎

Source. Repository-derived.

Commentary.

Gaussian finite-moment integrability transports through the actual difference map and finite scaling of each coordinate measure.

Definition 1.10 (Actual square-difference class).

$\forall c \in R e a l, \forall ka pp a \in R e a l, \forall h c \in 0 \leq c, \forall hka pp a \in 0 < ka pp a, HasType (squareDifference (c, ka pp a, h c, hka pp a), Lp (R e a l, 2, prod (spatialMeasure (c, ka pp a), spatialMeasure (c, ka pp a)))) \land squareDifference (c, ka pp a, h c, hka pp a) = toLp (memLpOfIntegrableSquare (spatialDifferenceFourthIntegrable (c, ka pp a, h c, hka pp a)), (z : Prod (R e a l, R e a l) \mapsto (fst (z) - snd (z))^{2}))$

Formalization. D5/S3/Fourier/Asymptotics/GaussianFrequencyKernel.squareDifference (✓ std3).

Source. Repository-derived.

Commentary.

This is the toLp class of (x-y)^2, with its membership witness obtained from fourth difference integrability.

Theorem 1.11 (Square-difference representative).

$\forall c \in R e a l, \forall ka pp a \in R e a l, \forall h c \in 0 \leq c, \forall hka pp a \in 0 < ka pp a, AEEq (coeFn (squareDifference (c, ka pp a, h c, hka pp a)), (z : Prod (R e a l, R e a l) \mapsto (fst (z) - snd (z))^{2}), prod (spatialMeasure (c, ka pp a), spatialMeasure (c, ka pp a)))$

Proof. Machine-checked in Lean as D5/S3/Fourier/Asymptotics/GaussianFrequencyKernel.squareDifference_coe (✓ std3). ∎

Source. Repository-derived.

Commentary.

The L2 class has the displayed actual product-measure representative.

Theorem 1.12 (Exact dominating class norm).

$\forall c \in R e a l, \forall ka pp a \in R e a l, \forall h c \in 0 \leq c, \forall hka pp a \in 0 < ka pp a, norm (squareDifference (c, ka pp a, h c, hka pp a)) = \frac{2 \cdot sqrt ( 3 ) \cdot spatialMass ( c , ka pp a )}{ka pp a}$

Proof. Machine-checked in Lean as D5/S3/Fourier/Asymptotics/GaussianFrequencyKernel.squareDifference_norm (✓ std3). ∎

Source. Repository-derived.

Commentary.

The fourth difference integral gives the norm 2 sqrt(3) gamma/kappa, with no positivity-of-mass assumption.

Definition 1.13 (Original frequency kernel).

$\forall c \in R e a l, \forall ka pp a \in R e a l, \forall h c \in 0 \leq c, \forall hka pp a \in 0 < ka pp a, \forall v \in R e a l, gaussianFrequency (c, ka pp a, h c, hka pp a, v) = val (frequencyKernel (spatialMeasure (c, ka pp a), v))$

Formalization. D5/S3/Fourier/Asymptotics/GaussianFrequencyKernel.gaussianFrequency (✓ std3).

Source. Repository-derived.

Commentary.

This is the existing frequencyKernel, viewed in the actual symmetric L2 subspace using the derived finite-measure instance. No kernel or noise is replaced.

Theorem 1.14 (Cosine-difference representative).

$\forall c \in R e a l, \forall ka pp a \in R e a l, \forall h c \in 0 \leq c, \forall hka pp a \in 0 < ka pp a, \forall v \in R e a l, AEEq (coeFn (val (gaussianFrequency (c, ka pp a, h c, hka pp a, v))), (z : Prod (R e a l, R e a l) \mapsto cos (\frac{pi ( )}{2} \cdot v \cdot (fst (z) - snd (z))) - 1), prod (spatialMeasure (c, ka pp a), spatialMeasure (c, ka pp a)))$

Proof. Machine-checked in Lean as D5/S3/Fourier/Asymptotics/GaussianFrequencyKernel.gaussianFrequency_coe (✓ std3). ∎

Source. Repository-derived.

Commentary.

For every real frequency v, the representative is cos((pi/2)v(x-y))-1.

Theorem 1.15 (Quadratic zero-frequency bound).

$\forall c \in R e a l, \forall ka pp a \in R e a l, \forall h c \in 0 \leq c, \forall hka pp a \in 0 < ka pp a, \forall v \in R e a l, norm (gaussianFrequency (c, ka pp a, h c, hka pp a, v)) \leq \frac{sqrt ( 3 ) \cdot \frac{pi ( )}{2} ^{2} \cdot spatialMass ( c , ka pp a )}{ka pp a} \cdot v^{2}$

Proof. Machine-checked in Lean as D5/S3/Fourier/Asymptotics/GaussianFrequencyKernel.frequency_norm_bound (✓ std3). ∎

Source. Repository-derived.

Commentary.

The global cosine remainder inequality and exact square-difference norm give ||D_v|| <= sqrt(3)(pi/2)^2 gamma v^2/kappa for every real v, including zero.

Theorem 1.16 (Global frequency regularity).

$\forall c \in R e a l, \forall ka pp a \in R e a l, \forall h c \in 0 \leq c, \forall hka pp a \in 0 < ka pp a, \exists K \in NNR e a l, LipschitzWith (K, (v : R e a l \mapsto gaussianFrequency (c, ka pp a, h c, hka pp a, v)))$

Proof. Machine-checked in Lean as D5/S3/Fourier/Asymptotics/GaussianFrequencyKernel.frequency_lipschitz (✓ std3). ∎

Source. Repository-derived.

Commentary.

There is a finite nonnegative Lipschitz constant for the actual Gaussian frequency kernel on the whole real line. The proof uses the same cosine bound and dominating L2 class 1+(x-y)^2 as frequency continuity, whose proof consumes this helper. The helper adds no mathematical content credit. Composition with the original second integral gives the regularity needed by the existing jointly measurable L2 version theorem, on the original probability space.

Theorem 1.17 (Frequency L2 continuity).

$\forall c \in R e a l, \forall ka pp a \in R e a l, \forall h c \in 0 \leq c, \forall hka pp a \in 0 < ka pp a, Continuous ((v : R e a l \mapsto gaussianFrequency (c, ka pp a, h c, hka pp a, v)))$

Proof. Machine-checked in Lean as D5/S3/Fourier/Asymptotics/GaussianFrequencyKernel.frequency_continuous (✓ std3). ∎

Source. Repository-derived.

Commentary.

The consumed global Lipschitz helper supplies continuity in the actual symmetric product L2 space.

Definition 1.18 (Zero-inclusive quotient).

$\forall c \in R e a l, \forall ka pp a \in R e a l, \forall h c \in 0 \leq c, \forall hka pp a \in 0 < ka pp a, \forall v \in R e a l, quotientFrequency (c, ka pp a, h c, hka pp a, v) = smul (inv (v), gaussianFrequency (c, ka pp a, h c, hka pp a, v))$

Formalization. D5/S3/Fourier/Asymptotics/GaussianFrequencyKernel.quotientFrequency (✓ std3).

Source. Repository-derived.

Commentary.

Real inverse assigns zero at zero, so J_v=v^-1 D_v has J_0=0 and the original D_v/v representative elsewhere.

Theorem 1.19 (Linear quotient bound).

$\forall c \in R e a l, \forall ka pp a \in R e a l, \forall h c \in 0 \leq c, \forall hka pp a \in 0 < ka pp a, \forall v \in R e a l, norm (quotientFrequency (c, ka pp a, h c, hka pp a, v)) \leq \frac{sqrt ( 3 ) \cdot \frac{pi ( )}{2} ^{2} \cdot spatialMass ( c , ka pp a )}{ka pp a} \cdot abs (v)$

Proof. Machine-checked in Lean as D5/S3/Fourier/Asymptotics/GaussianFrequencyKernel.quotientFrequency_norm (✓ std3). ∎

Source. Repository-derived.

Commentary.

Cancellation of one frequency factor gives ||J_v|| <= sqrt(3)(pi/2)^2 gamma |v|/kappa. The zero case is proved separately.

Theorem 1.20 (Continuity at the boundary).

$\forall c \in R e a l, \forall ka pp a \in R e a l, \forall h c \in 0 \leq c, \forall hka pp a \in 0 < ka pp a, Continuous ((v : R e a l \mapsto quotientFrequency (c, ka pp a, h c, hka pp a, v)))$

Proof. Machine-checked in Lean as D5/S3/Fourier/Asymptotics/GaussianFrequencyKernel.quotientFrequency_continuous (✓ std3). ∎

Source. Repository-derived.

Commentary.

Away from zero, continuity follows from inverse and scalar multiplication. At zero, the linear norm bound squeezes J_v to J_0=0.

Theorem 1.21 (Every original finite window).

$\forall c \in R e a l, \forall ka pp a \in R e a l, \forall h c \in 0 \leq c, \forall hka pp a \in 0 < ka pp a, \forall s \in R e a l, IntegrableOn ((v : R e a l \mapsto quotientFrequency (c, ka pp a, h c, hka pp a, v)), Icc (0, exp (s)), v o l u m e)$

Proof. Machine-checked in Lean as D5/S3/Fourier/Asymptotics/GaussianFrequencyKernel.quotientFrequency_integrable (✓ std3). ∎

Source. Repository-derived.

Commentary.

Continuity on the compact closed interval [0,exp(s)] supplies Bochner integrability for every real s. The boundary is included.

Theorem 1.22 (Actual spatial integral representative).

$\forall c \in R e a l, \forall ka pp a \in R e a l, \forall h c \in 0 \leq c, \forall hka pp a \in 0 < ka pp a, \forall s \in R e a l, AEEq coeFn (val (setIntegral ((v : R e a l \mapsto quotientFrequency (c, ka pp a, h c, hka pp a, v)), Icc (0, exp (s)), v o l u m e))), (z : Prod (R e a l, R e a l) \mapsto intervalIntegral (v : R e a l \mapsto \frac{cos ( \frac{pi ( )}{2} \cdot v \cdot ( fst ( z ) - snd ( z ) ) ) - 1}{v}), 0, exp (s), v o l u m e), prod (spatialMeasure (c, ka pp a), spatialMeasure (c, ka pp a))$

Proof. Machine-checked in Lean as D5/S3/Fourier/Asymptotics/GaussianFrequencyKernel.frequency_integral_coe (✓ std3). ∎

Source. Repository-derived.

Commentary.

For each real s, the symmetric L2 Bochner integral on [0,exp(s)] has the almost-everywhere representative obtained by integrating the actual cosine quotient in frequency. The continuous L2 primitive and its jointly measurable spatial quotient supply product integrability and Fubini.

Definition 1.23 (Original finite-frequency kernel).

$\forall c \in R e a l, \forall ka pp a \in R e a l, \forall h c \in 0 \leq c, \forall hka pp a \in 0 < ka pp a, \forall D \in R e a l, \forall s \in R e a l, regularKernel (c, ka pp a, h c, hka pp a, D, s) = smul (1 + 2 \cdot eulerMascheroniConstant () + 2 \cdot D + 2 \cdot s, diagonalKernel (spatialMeasure (c, ka pp a), oneVector (spatialMeasure (c, ka pp a)))) + smul (2, setIntegral ((v : R e a l \mapsto quotientFrequency (c, ka pp a, h c, hka pp a, v)), Icc (0, exp (s)), v o l u m e))$

Formalization. D5/S3/Fourier/Asymptotics/GaussianFrequencyKernel.regularKernel (✓ std3).

Source. Repository-derived.

Commentary.

The original H_s is constructed in the actual symmetric product L2 space. Its constant coefficient is b_+2s, where b_=1+2 Euler+2D, and its frequency integral includes the zero endpoint.

Theorem 1.24 (Off-diagonal Ci identity).

$\forall c \in R e a l, \forall ka pp a \in R e a l, \forall h c \in 0 \leq c, \forall hka pp a \in 0 < ka pp a, \forall D \in R e a l, \forall s \in R e a l, \forall H \in symmetricKernel (spatialMeasure (c, ka pp a)), \forall h H \in AEEq (coeFn (val (H)), (z : Prod (R e a l, R e a l) \mapsto 1 + 2 \cdot D - 2 \cdot log (\frac{pi ( )}{2} \cdot abs ((fst (z) - snd (z))))), prod (spatialMeasure (c, ka pp a), spatialMeasure (c, ka pp a))), AEEq (coeFn (val (regularKernel (c, ka pp a, h c, hka pp a, D, s) - H)), (z : Prod (R e a l, R e a l) \mapsto 2 \cdot cosineIntegral (\frac{pi ( )}{2} \cdot exp (s) \cdot abs ((fst (z) - snd (z))))), prod (spatialMeasure (c, ka pp a), spatialMeasure (c, ka pp a)))$

Proof. Machine-checked in Lean as D5/S3/Fourier/Asymptotics/GaussianFrequencyKernel.regularKernel_difference (✓ std3). ∎

Source. Repository-derived.

Commentary.

For any H with the original logarithmic representative, H_s-H has representative 2Ci((pi/2)exp(s)|x-y|). The actual Gaussian density gives a null spatial diagonal, including c=0. Cosine evenness, positive scaling and the positive Ci/Euler normalization identify the spatial primitive; the desired kernel identity is a conclusion.

Definition 1.25 (Actual same-W quadratic frequency).

Formalization. D5/S3/Fourier/Asymptotics/GaussianFrequencyKernel.quadraticFrequency (✓ std3).

Source. Repository-derived.

Commentary.

For one fixed original isometry W and its centered Gaussian marginal laws on P, the quadratic class is the sum of the centered cosine and sine squares minus the centered constant square.

Theorem 1.26 (Exact same-noise identification).

Proof. Machine-checked in Lean as D5/S3/Fourier/Asymptotics/GaussianFrequencyKernel.quadraticFrequency_representation (✓ std3). ∎

Source. Repository-derived.

Commentary.

The continuous second integral agrees with the finite construction. Trigonometric energy cancels the centering terms, so the displayed representative is |F(v)|^2-Y^2 for the same W and P.

Theorem 1.27 (Bochner commutation and centered remainder).

$\forall c \in R e a l, \forall ka pp a \in R e a l, \forall h c \in 0 \leq c, \forall hka pp a \in 0 < ka pp a, \forall O m e g a \in T y p e, \forall S i g ma O m e g a \in MeasurableSpace (O m e g a), \forall P \in Measure (O m e g a), \forall h p ro b \in IsProbabilityMeasure (P), \forall W \in LinearIsometry (R e a l, Lp (R e a l, 2, spatialMeasure (c, ka pp a)), Lp (R e a l, 2, P)), \forall hW \in (\forall f \in Lp (R e a l, 2, spatialMeasure (c, ka pp a)), HasLaw (coeFn (apply (W, f)), gaussianReal (0, toNNReal (norm (f)^{2})), P)), \forall s \in R e a l, IntegrableOn ((v : R e a l \mapsto smul (inv (v), quadraticFrequency (c, ka pp a, h c, hka pp a, P, W, hW, v))), Icc (0, exp (s)), v o l u m e) \land (apply (secondIntegral (spatialMeasure (c, ka pp a), P, W, hW), setIntegral ((v : R e a l \mapsto quotientFrequency (c, ka pp a, h c, hka pp a, v)), Icc (0, exp (s)), v o l u m e)) = setIntegral ((v : R e a l \mapsto smul (inv (v), quadraticFrequency (c, ka pp a, h c, hka pp a, P, W, hW, v))), Icc (0, exp (s)), v o l u m e) \land (\forall D \in R e a l, \forall H \in symmetricKernel (spatialMeasure (c, ka pp a)), apply (secondIntegral (spatialMeasure (c, ka pp a), P, W, hW), regularKernel (c, ka pp a, h c, hka pp a, D, s) - H) = smul (1 + 2 \cdot eulerMascheroniConstant () + 2 \cdot D + 2 \cdot s, centeredSquare (spatialMeasure (c, ka pp a), P, W, hW, oneVector (spatialMeasure (c, ka pp a)))) + smul (2, setIntegral ((v : R e a l \mapsto smul (inv (v), quadraticFrequency (c, ka pp a, h c, hka pp a, P, W, hW, v))), Icc (0, exp (s)), v o l u m e)) - apply (secondIntegral (spatialMeasure (c, ka pp a), P, W, hW), H)))$

Proof. Machine-checked in Lean as D5/S3/Fourier/Asymptotics/GaussianFrequencyKernel.frequency_integral_sameNoise (✓ std3). ∎

Source. Repository-derived.

Commentary.

The original second integral commutes with the integrable frequency quotient on every finite window. For every D and symmetric H, its image of H_s-H is (b_*+2s) times the centered original Y square, plus twice the same-W quadratic quotient integral, minus I2(H). This is an equality of actual L2(P) classes. Identifying the selected original R and E processes and their common paths requires the corresponding process version identification.

Theorem 1.28 (Two-sided logarithmic control).

$\forall x \in R e a l, \forall h x \in 0 < x, log (x)^{2} \leq 16 \cdot rpow (x, \frac{- 1}{2}) + x^{2}$

Proof. Machine-checked in Lean as D5/S3/Fourier/Asymptotics/GaussianFrequencyKernel.log_square_bound (✓ std3). ∎

Source. Repository-derived.

Commentary.

For every positive x, log(x)^2 <= 16 x^(-1/2)+x^2. Below one, the reciprocal power bound controls the logarithmic singularity; above one, log(x) <= x controls the tail. This estimate is consumed by Gaussian logarithmic integrability.

Theorem 1.29 (Gaussian integrability at the singularity).

$\forall b \in R e a l, \forall hb \in 0 < b, Integrable ((x : R e a l \mapsto log (abs (x))^{2} \cdot exp (- b \cdot x^{2})), v o l u m e)$

Proof. Machine-checked in Lean as D5/S3/Fourier/Asymptotics/GaussianFrequencyKernel.log_square_gaussian_integrable (✓ std3). ∎

Source. Repository-derived.

Commentary.

The actual function log(|x|)^2 exp(-b x^2) is Lebesgue integrable for every b>0. The previous bound is dominated by the pinned Gaussian power integrals with exponents -1/2 and 2 on the positive half-line; reflection covers the negative half-line. The assigned value at zero has no integral effect.

Theorem 1.30 (Logarithmic moment of the actual Gaussian law).

$\forall v \in NNR e a l, \forall h v \in Not (v = 0), Integrable ((x : R e a l \mapsto log (abs (x))^{2}), gaussianReal (0, v))$

Proof. Machine-checked in Lean as D5/S3/Fourier/Asymptotics/GaussianFrequencyKernel.gaussian_log_square_integrable (✓ std3). ∎

Source. Repository-derived.

Commentary.

For every nonzero nonnegative variance v, log(|x|)^2 is integrable under gaussianReal(0,v). The Gaussian density identity directly consumes the proved weighted Lebesgue integrability. No logarithmic moment premise is supplied.

Theorem 1.31 (Singular H and its actual Ci remainder).

$\forall c \in R e a l, \forall ka pp a \in R e a l, \forall h c \in 0 \leq c, \forall hka pp a \in 0 < ka pp a, \forall D \in R e a l, \exists H \in symmetricKernel (spatialMeasure (c, ka pp a)), AEEq (coeFn (val (H)), (z : Prod (R e a l, R e a l) \mapsto 1 + 2 \cdot D - 2 \cdot log (\frac{pi ( )}{2} \cdot abs ((fst (z) - snd (z))))), prod (spatialMeasure (c, ka pp a), spatialMeasure (c, ka pp a))) \land (\forall s \in R e a l, AEEq (coeFn (val (regularKernel (c, ka pp a, h c, hka pp a, D, s) - H)), (z : Prod (R e a l, R e a l) \mapsto 2 \cdot cosineIntegral (\frac{pi ( )}{2} \cdot exp (s) \cdot abs ((fst (z) - snd (z))))), prod (spatialMeasure (c, ka pp a), spatialMeasure (c, ka pp a))))$

Proof. Machine-checked in Lean as D5/S3/Fourier/Asymptotics/GaussianFrequencyKernel.singularKernel_exists (✓ std3). ∎

Source. Repository-derived.

Commentary.

For every real D, nonnegative c and positive kappa, one H in the actual symmetric product L2 space has representative 1+2D-2 log((pi/2)|x-y|), and for every real s its difference from the constructed H_s has the Ci representative. Apply D=D_w for the original kernel. The Gaussian logarithmic moment and unnormalized mass include c=0; the spatial diagonal is null. This assertion gives the spatial kernel and all its fixed-time differences. It does not assert a common pointwise W version or a process limit.

References

Truth anchor: D5/S3/Fourier/Asymptotics/GaussianFrequencyKernel.frequency_continuous
Truth anchor: D5/S3/Fourier/Asymptotics/GaussianFrequencyKernel.frequency_integral_coe
Truth anchor: D5/S3/Fourier/Asymptotics/GaussianFrequencyKernel.frequency_integral_sameNoise
Truth anchor: D5/S3/Fourier/Asymptotics/GaussianFrequencyKernel.frequency_lipschitz
Truth anchor: D5/S3/Fourier/Asymptotics/GaussianFrequencyKernel.frequency_norm_bound
Truth anchor: D5/S3/Fourier/Asymptotics/GaussianFrequencyKernel.gaussianFrequency
Truth anchor: D5/S3/Fourier/Asymptotics/GaussianFrequencyKernel.gaussianFrequency_coe
Truth anchor: D5/S3/Fourier/Asymptotics/GaussianFrequencyKernel.gaussian_difference_law
Truth anchor: D5/S3/Fourier/Asymptotics/GaussianFrequencyKernel.gaussian_fourth
Truth anchor: D5/S3/Fourier/Asymptotics/GaussianFrequencyKernel.gaussian_log_square_integrable
Truth anchor: D5/S3/Fourier/Asymptotics/GaussianFrequencyKernel.log_square_bound
Truth anchor: D5/S3/Fourier/Asymptotics/GaussianFrequencyKernel.log_square_gaussian_integrable
Truth anchor: D5/S3/Fourier/Asymptotics/GaussianFrequencyKernel.quadraticFrequency
Truth anchor: D5/S3/Fourier/Asymptotics/GaussianFrequencyKernel.quadraticFrequency_representation
Truth anchor: D5/S3/Fourier/Asymptotics/GaussianFrequencyKernel.quotientFrequency
Truth anchor: D5/S3/Fourier/Asymptotics/GaussianFrequencyKernel.quotientFrequency_continuous
Truth anchor: D5/S3/Fourier/Asymptotics/GaussianFrequencyKernel.quotientFrequency_integrable
Truth anchor: D5/S3/Fourier/Asymptotics/GaussianFrequencyKernel.quotientFrequency_norm
Truth anchor: D5/S3/Fourier/Asymptotics/GaussianFrequencyKernel.regularKernel
Truth anchor: D5/S3/Fourier/Asymptotics/GaussianFrequencyKernel.regularKernel_difference
Truth anchor: D5/S3/Fourier/Asymptotics/GaussianFrequencyKernel.singularKernel_exists
Truth anchor: D5/S3/Fourier/Asymptotics/GaussianFrequencyKernel.spatialMass
Truth anchor: D5/S3/Fourier/Asymptotics/GaussianFrequencyKernel.spatialMass_eq_integral
Truth anchor: D5/S3/Fourier/Asymptotics/GaussianFrequencyKernel.spatialMeasure
Truth anchor: D5/S3/Fourier/Asymptotics/GaussianFrequencyKernel.spatialMeasure_finite
Truth anchor: D5/S3/Fourier/Asymptotics/GaussianFrequencyKernel.spatialMeasure_normalized
Truth anchor: D5/S3/Fourier/Asymptotics/GaussianFrequencyKernel.spatial_difference_fourth
Truth anchor: D5/S3/Fourier/Asymptotics/GaussianFrequencyKernel.spatial_difference_fourth_integrable
Truth anchor: D5/S3/Fourier/Asymptotics/GaussianFrequencyKernel.squareDifference
Truth anchor: D5/S3/Fourier/Asymptotics/GaussianFrequencyKernel.squareDifference_coe
Truth anchor: D5/S3/Fourier/Asymptotics/GaussianFrequencyKernel.squareDifference_norm
Dependency: D5/S3/Fourier/Asymptotics/CosineNormalizedRemainder
Dependency: D5/S3/Fourier/Asymptotics/L2ContinuousPrimitive
Dependency: D5/S3/Fourier/Asymptotics/SameNoiseSecondChaos

Keyboard shortcuts

trureturing — Discovering truth

Gaussian frequency integration

Abstract

References