Joint Convergence of Gaussian Approximation Rows

This is the fixed-row convergence statement for the regular Gaussian-then-quadratic approximation.

Let $E$ be a finite-dimensional real inner-product space with Borel measurable structure, let $\mu$ be a probability measure with finite second moment, and fix $n\in\mathbb N$. Let rowLaw μ n k be the $k$th law in row $n$, and let statistics collect its associated statistics. Then

as $k\to\infty$. The convergence is in the product topology encoded by Tendsto and combines convergence of the law with convergence of the recorded statistics. It is stated row by row and does not assert the diagonal approximation.

Original Lean declaration header

Within namespace FunctionalInequalities.KLS.LogConcave.GaussianSmoothing. Shown in its original module context. Proof omitted.

theorem row_joint_tendsto (μ : ProbabilityMeasure E) (hμ2 : MemLp id 2 (μ : Measure E)) (n : ℕ) :
    Tendsto (fun k : ℕ => (rowLaw μ n k, statistics (rowLaw μ n k)))
      atTop (𝓝 (gaussianSeq μ n, statistics (gaussianSeq μ n)))

Module navigation

Module: KLS/LogConcave/Density/GaussianSmoothing/RegularApproximation.

Supporting theorems: gaussianLaw_exp_norm_integrable, covariance_quadraticTilt_tendsto, integral_quadraticTilt_tendsto.

Source excerpt, lines 75–77 · Frozen source 408915f.