Stat.Nonparametric
Nonparametric methods: approximation theory, fixed-weight linear smoothers, local-polynomial coercivity and derivative bounds, series/sieve estimators, projection-kernel risk building blocks, and moment-problem tools.
GaussianTransfer 2 core · 2 supporting The variance recipe is the ordinary integral with design factor 16 and design interval [-1/2,1/2]. ★ shiftedVariance_le
Transferring a weighted energy to a Gaussian shifted design integral
The variance recipe is the ordinary integral with design factor 16 and design interval [-1/2,1/2]. The full joint integrability hypothesis is a standard Fubini hypothesis; no quantitative variance inequality is assumed. A shift costs at most the κ-th Gaussian moment times σ^κ times the zeroth physical energy.
Primary source fetched at the installed Mathlib revision
db584cd6d46c92f209a44c0f1c829460d327499d:
https://github.com/leanprover-community/mathlib4/blob/db584cd6d46c92f209a44c0f1c829460d327499d/Mathlib/Probability/Distributions/Gaussian/Real.lean
This supplies memLp_id_gaussianReal, integral_id_gaussianReal, and
variance_id_gaussianReal; no exact moment formula needs to be reimplemented.
A moment exponent, a Gaussian noise scale, and a complex physical-space kernel determine the Gaussian-shifted design variance integral as sixteen times the integral, over the design interval [-1/2, 1/2], of the absolute design point raised to the moment exponent times the standard-Gaussian average of the squared modulus of the kernel evaluated at the design point plus the noise scale times the Gaussian draw.
Definition (Lean source)
A complex physical-space kernel, a moment exponent in the interval from zero to two, a nonnegative Gaussian noise scale, finite ordinary and weighted squared energies, and integrability of the weighted joint squared norm imply that the Gaussian-shifted design variance integral is at most 32 · (W + 2 σ^κ E), where W is the kernel's κ-weighted squared energy and E its ordinary squared energy.
Formal statement
Proof (Lean source)
2 supporting declarations (lemmas, instances)
-
shiftedVariance_realPart_letheorem — A complex physical-space kernel, a moment exponent and Gaussian noise scale, kernel measurability, and integrability of its weighted joint squared norm imply that taking the real part cannot increase the Gaussian-shifted design variance.hypothesesg :ℝ → ℂκ σ :ℝhg :hjoint :Integrable (fun p : ℝ × ℝ => |p.1| ^ κ * ‖g (p.1 + σ * p.2)‖ ^ 2) (volume.prod (gaussianReal 0 1))conclusionshiftedVariance κ σ (fun v => ((g v).re : ℂ)) ≤ shiftedVariance κ σ gProof (Lean source)
theorem shiftedVariance_realPart_le (g : ℝ → ℂ) (κ σ : ℝ) (hg : Measurable g) (hjoint : Integrable (fun p : ℝ × ℝ => |p.1| ^ κ * ‖g (p.1 + σ * p.2)‖ ^ 2) (volume.prod (gaussianReal 0 1))) : shiftedVariance κ σ (fun v => ((g v).re : ℂ)) ≤ shiftedVariance κ σ g := by have hp (v : ℝ) : ‖((g v).re : ℂ)‖ ^ 2 ≤ ‖g v‖ ^ 2 := by simpa only [Complex.norm_real, Real.norm_eq_abs] using pow_le_pow_left₀ (abs_nonneg (g v).re) (Complex.abs_re_le_norm (g v)) 2 have hw (t z : ℝ) : |t| ^ κ * ‖((g (t + σ * z)).re : ℂ)‖ ^ 2 ≤ |t| ^ κ * ‖g (t + σ * z)‖ ^ 2 := mul_le_mul_of_nonneg_left (hp _) (Real.rpow_nonneg (abs_nonneg t) κ) have hr : Integrable (fun p : ℝ × ℝ => |p.1| ^ κ * ‖((g (p.1 + σ * p.2)).re : ℂ)‖ ^ 2) (volume.prod (gaussianReal 0 1)) := by apply hjoint.mono' · fun_prop · filter_upwards [] with p rw [Real.norm_eq_abs, abs_of_nonneg (mul_nonneg (Real.rpow_nonneg (abs_nonneg p.1) κ) (sq_nonneg _))] exact hw _ _ have ho := hr.integral_prod_left have hoc := hjoint.integral_prod_left simp only [integral_const_mul] at ho hoc unfold shiftedVariance apply mul_le_mul_of_nonneg_left _ (by norm_num) apply integral_mono_ae ho.restrict hoc.restrict -- Keep the weight inside each slice. Integral linearity also holds when it -- vanishes, so no unweighted integrability is required on zero-weight slices. have hs : ∀ᵐ t ∂volume, |t| ^ κ * (∫ z, ‖((g (t + σ * z)).re : ℂ)‖ ^ 2 ∂gaussianReal 0 1) ≤ |t| ^ κ * (∫ z, ‖g (t + σ * z)‖ ^ 2 ∂gaussianReal 0 1) := by filter_upwards [hr.prod_right_ae, hjoint.prod_right_ae] with t ht htc simpa only [integral_const_mul] using integral_mono ht htc (hw t) exact ae_restrict_of_ae hs -
gaussian_abs_moment_le_twotheorem — A moment exponent in the interval from zero to two has a finite standard-Gaussian absolute moment bounded by two.hypothesesκ :ℝhκ0 :0 ≤ κhκ2 :κ ≤ 2conclusionconclusion 1Integrable (fun z : ℝ => |z| ^ κ) (gaussianReal 0 1)conclusion 2(∫ z : ℝ, |z| ^ κ ∂gaussianReal 0 1) ≤ 2Proof (Lean source)
theorem gaussian_abs_moment_le_two (κ : ℝ) (hκ0 : 0 ≤ κ) (hκ2 : κ ≤ 2) : Integrable (fun z : ℝ => |z| ^ κ) (gaussianReal 0 1) ∧ (∫ z : ℝ, |z| ^ κ ∂gaussianReal 0 1) ≤ 2 := by have hsq : Integrable (fun z : ℝ => z ^ 2) (gaussianReal 0 1) := (memLp_id_gaussianReal (μ := 0) (v := 1) 2).integrable_sq have hsqi : (∫ z : ℝ, z ^ 2 ∂gaussianReal 0 1) = 1 := by have h := variance_id_gaussianReal (μ := 0) (v := 1) rw [variance_eq_integral measurable_id.aemeasurable] at h simpa [integral_id_gaussianReal] using h have hb (z : ℝ) : |z| ^ κ ≤ 1 + z ^ 2 := by by_cases hz : |z| ≤ 1 · have := Real.rpow_le_one (abs_nonneg z) hz hκ0 nlinarith [sq_nonneg z] · have := Real.rpow_le_rpow_of_exponent_le (le_of_not_ge hz) hκ2 simp only [Real.rpow_two, sq_abs] at this linarith have hm : AEStronglyMeasurable (fun z : ℝ => |z| ^ κ) (gaussianReal 0 1) := by fun_prop have hi := (integrable_const (1 : ℝ)).add hsq have hiκ : Integrable (fun z : ℝ => |z| ^ κ) (gaussianReal 0 1) := hi.mono' hm (Filter.Eventually.of_forall fun z => by rw [Real.norm_eq_abs, abs_of_nonneg (Real.rpow_nonneg (abs_nonneg z) κ)] exact hb z) refine ⟨hiκ, ?_⟩ calc _ ≤ ∫ z : ℝ, (1 + z ^ 2) ∂gaussianReal 0 1 := integral_mono hiκ hi hb _ = 2 := by rw [integral_add (integrable_const _) hsq, hsqi] norm_num
Specialization 1 core · 0 supporting A caller supplies a compact C¹ profile F with the sinc-six support and two uniform heights. ★ inverseGaussian_shiftedVariance_le
Inverse Gaussian sinc-six specialization recipe
A caller supplies a compact C¹ profile F with the sinc-six support and two uniform
heights. The sixth convolution of the normalized sinc boxes has exactly the support
radius 3/(πh) and heights of orders h and h². No paper-specific construction is
imported. Standard absolute integrability of the inverse multiplier, of its derivative
transform, and of the design/noise joint integrand may be supplied.
The recipe derives the whole quantitative estimate, including Gaussian averaging:
Vq ≤ C h^(κ+1) (1+σ/h)^10 exp(36 (σ/h)^2) with an explicit C depending
only on the two profile heights. For a real-valued kernel represented by the real
part of the complex inverse transform, Complex.abs_re_le_norm transfers the
same upper bound to its squared real variance integral.
A compact continuously differentiable frequency profile, a moment exponent in the interval from zero to two, a nonnegative Gaussian noise scale σ and a bandwidth h in (0, 1/4], nonnegative envelope constants, support of the profile within 3/(πh) of the origin, the uniform bound a h on the profile and the uniform bound b h² on its derivative, and integrable inverse-transform and joint design-noise quantities imply that the Gaussian-shifted design variance integral of the inverse Fourier transform of the inverse-Gaussian multiplier of the profile is at most 32 · (6/π) · (3a² + (2π)⁻² (b + 12πa)²) · h^(κ+1) · (1 + σ/h)^10 · exp(36 (σ/h)²).