On this page

GaussianAnalysiscomparisongauss_smoothing

Gaussian smoothing of Lipschitz functions

GaussianAnalysis.comparison.gauss_smoothinglibrary/comparison/gauss_smoothing.v476 lines15 lemmas and theorems, 2 definitionssource

Imports 8 library modules and 28 external

External: HB.structures, mathcomp.classical.all_ssreflect_compat, mathcomp.algebra.algebraic_hierarchy.ssralg, mathcomp.algebra.numeric_hierarchy.ssrnum, mathcomp.algebra.interval, mathcomp.algebra.matrix, mathcomp.algebra.ring_tactic, mathcomp.algebra.field_tactic, mathcomp.algebra.arithmetic_tactic, mathcomp.classical.boolp, mathcomp.classical.classical_sets, mathcomp.classical.functions, mathcomp.reals.reals, mathcomp.analysis.ereal, mathcomp.analysis.topology_theory.topology, mathcomp.analysis.normedtype_theory.normedtype, mathcomp.analysis.sequences, mathcomp.analysis.derive, mathcomp.analysis.realfun, mathcomp.analysis.exp, mathcomp.analysis.measure_theory.measure, mathcomp.analysis.lebesgue_stieltjes_measure, mathcomp.analysis.lebesgue_measure, mathcomp.analysis.numfun, mathcomp.analysis.measurable_realfun, mathcomp.analysis.lebesgue_integral_theory.lebesgue_integral, mathcomp.analysis.probability_theory.probability, mathcomp.analysis.probability_theory.normal_distribution

Imported by 20

Required by 10 files of the paper proofs

For G : 'rV[R]_n -> R and eps > 0, gauss_smooth eps G x is E[G (x + eps y)] for y of law gauss n. If G is bounded by K and L-Lipschitz for the Euclidean norm, then gauss_smooth eps G is bounded by K (gauss_smooth_bounded) and L-Lipschitz (gauss_smooth_lipschitz). Its partial derivatives are gauss_smooth_partial eps G j x = E[G (x + eps y) y_j] / eps (gauss_smooth_derive), computed with the Cameron-Martin formula of gauss_shift.v and differentiation under the integral sign. They are continuous (continuous_gauss_smooth_partial), so gauss_smooth eps G is differentiable (gauss_smooth_differentiable), and its gradient has Euclidean norm at most L (gauss_smooth_grad). Finally |gauss_smooth eps G x - G x| <= L eps E[|y|] (gauss_smooth_close).

The file also proves that a function that is Lipschitz for the Euclidean norm is continuous (lipschitz_frobenius_continuous), that the gradient of a function of class C^1 that is L-Lipschitz has Euclidean norm at most L (lipschitz_frobenius_grad), and an is_derive form of differentiation under the integral sign (is_derive_Rintegral).

`gauss_smooth eps G x`	E[G (x + eps y)], y of law gauss n
`gauss_smooth_partial eps G j x`	E[G (x + eps y) y_j] / eps

Main results

Results	Statement
gauss_smooth_derivegauss_smooth_differentiablegauss_smooth_gradgauss_smooth_close	For `G` bounded and `L`-Lipschitz (Euclidean norm) and `eps > 0`, the Gaussian smoothing `x \|-> E[G (x + eps y)]` is differentiable, with partial derivatives `E[G (x + eps y) y_j] / eps`, continuous, of gradient norm at most `L`, and within `L eps E[\|y\|]` of `G`.
lipschitz_frobenius_grad	The gradient of a function of class C^1 that is `L`-Lipschitz for the Euclidean norm has Euclidean norm at most `L`.

Declarations17 exported, 11 local

sectionfrobenius_mx_norm

Context {R : realType}.

lemma frobenius_le_mx_norm source, line 55

forall {R : realType} [m n : nat] (A : 'M_(m, n)), frobenius A <= (m * n)%:R * `|A|

Statement as written in the source

Lemma frobenius_le_mx_norm m n (A : 'M[R]_(m, n)) :
  frobenius A <= (m * n)%:R * `|A|.

Used by 6 declarations in 4 files

this file: lipschitz_frobenius_continuous, integrable_gauss_frobenius
GaussianAnalysis.comparison.gauss_concentration: gauss_poincare_lipschitz
GaussianAnalysis.comparison.cgmt: continuous_frobenius_mulmx
GaussianAnalysis.comparison.brascamp_lieb: gauss_ibp_unit, mxdot_le_mx_norm

sectionlipschitz_frobenius

Context {R : realType} {n : nat}.
Implicit Types F : 'rV[R]_n -> R.

lemma lipschitz_frobenius_continuous source, line 79

forall {R : realType} {n : nat} [F : 'rV_n -> R] [L : R],
(forall x y : 'rV_n, `|F x - F y| <= L * frobenius (x - y)) -> continuous F

Statement as written in the source

Lemma lipschitz_frobenius_continuous F (L : R) :
  (forall x y, `|F x - F y| <= L * frobenius (x - y)) -> continuous F.

Used by 38 declarations in 15 files

GaussianAnalysis.matrix.covering: colmax_sep
GaussianAnalysis.probability.subgaussian_matrix: measurable_opnorm
GaussianAnalysis.random_matrix.goe: polyfun_goe_clip, goe_opnorm_tail_small
GaussianAnalysis.random_matrix.goe_edge: measurable_goe_lambda_max, measurable_goe_lambda_maxN
GaussianAnalysis.random_matrix.wigner: polyfun_goe_stat_clip, continuous_goe_stat, wigner, wigner_uniform
GaussianAnalysis.random_matrix.matrix_series: measurable_series_opnorm
GaussianAnalysis.random_matrix.goe_entries: measurable_goe_opnorm_ge
this file: cG, continuous_gauss_smooth_partial, integrable_gauss_frobenius
GaussianAnalysis.comparison.gauss_concentration: cF, mA, mF, gauss_poincare_lipschitz
GaussianAnalysis.comparison.escape: gordon_escape_tail, measurable_escape_proj, gauss_opnorm_tail, gauss_frobenius_mean_le, gauss_proj_mean_ge
GaussianAnalysis.comparison.cgmt: cgmt_tail, measurable_escape_inf, measurable_cgmt_aux
GaussianAnalysis.comparison.cone_escape: cone_sup_attained, mF
GaussianAnalysis.comparison.gauss_law: mG, gauss_smooth_partial_stein, gauss_law_lipschitz, measurable_lipschitz_gt0, lipschitz_pos_agree, gauss_mulmx_law
GaussianAnalysis.fourier.inversion: lipschitz_add_gauss, cf_rV_inversion
GaussianApplications.SKGap.Disorder: measurable_sk_coupling_opnorm

lemma lipschitz_frobenius_grad main result source, line 100

forall {R : realType} {n : nat} [F : 'rV_n -> R] [DF : 'I_n -> 'rV_n -> R] [L : R],
(forall (j : 'I_n)
   (x : 'rV[R]_n),
 is_derive x (delta_mx 0 j) F (DF j x)) ->
(forall j : 'I_n, continuous (DF j)) ->
(forall x y : 'rV_n, `|F x - F y| <= L * frobenius (x - y)) ->
forall x : 'rV_n, mxdot (\row_j DF j x) (\row_j DF j x) <= L ^+ 2

A function of class C^1 that is L-Lipschitz for the Euclidean norm has a gradient of Euclidean norm at most L.

Main result, as the README states it

The gradient of a function of class C^1 that is L-Lipschitz for the Euclidean norm has Euclidean norm at most L.

Statement as written in the source

Lemma lipschitz_frobenius_grad F (DF : 'I_n -> 'rV[R]_n -> R) (L : R) :
    (forall j x, is_derive x (delta_mx 0 j) F (DF j x)) ->
    (forall j, continuous (DF j)) ->
    (forall x y, `|F x - F y| <= L * frobenius (x - y)) ->
  forall x, mxdot (\row_j DF j x) (\row_j DF j x) <= L ^+ 2.

Used by 1 declaration in 1 file

this file: gauss_smooth_grad

sectionis_derive_Rintegral

Context {R : realType} d {Y : measurableType d} (mu : {measure set Y -> \bar R}).

lemma is_derive_Rintegral source, line 133

forall {R : realType} [d : measure_display] {Y : measurableType d} 
  [mu : measure Y R] [f df : R -> Y -> R] [D : Y -> R] [u v a : R],
a \in `]u, v[ ->
(forall x : R, x \in `]u, v[ -> mu.-integrable [set: Y] (EFin \o f x)) ->
(forall (x : R) (y : Y), x \in `]u, v[ -> is_derive x 1 (f^~ y) (df x y)) ->
(forall y : Y, 0 <= D y) ->
mu.-integrable [set: Y] (EFin \o D) ->
(forall (x : R) (y : Y), x \in `]u, v[ -> `|df x y| <= D y) ->
is_derive a 1
  (fun x : R => \int[mu]_y f x y)
  (\int[mu]_y df a y)

Differentiation under the integral sign, in the form of is_derive.

Statement as written in the source

Lemma is_derive_Rintegral (f df : R -> Y -> R) (D : Y -> R) (u v a : R) :
    a \in `]u, v[ ->
    (forall x, x \in `]u, v[ -> mu.-integrable [set: Y] (EFin \o f x)) ->
    (forall x y, x \in `]u, v[ -> is_derive x 1 (f ^~ y) (df x y)) ->
    (forall y, 0 <= D y) -> mu.-integrable [set: Y] (EFin \o D) ->
    (forall x y, x \in `]u, v[ -> `|df x y| <= D y) ->
  is_derive a 1 (fun x => \int[mu]_y f x y) (\int[mu]_y df a y).

Used by 7 declarations in 5 files

this file: gauss_smooth_derive
GaussianAnalysis.comparison.gauss_concentration: herbst_phi_derive, herbst_mgf_derive
GaussianAnalysis.comparison.ornstein_uhlenbeck: is_derive_normal_kernel
GaussianAnalysis.comparison.brascamp_lieb: is_derive_Lambda
GaussianAnalysis.fourier.charfun: derive_cf_re_normal, derive_cf_im_normal

sectiongauss_integrable

Context {R : realType}.
Local Notation N := (@normal_prob R 0 1).

lemma integrable_gauss_bounded source, line 162

forall {R : realType} [n : nat] [f : 'rV_n -> R] [C : R],
measurable_fun [set: 'rV_n] f ->
(forall y : 'rV_n, `|f y| <= C) -> (gauss n).-integrable [set: 'rV_n] (EFin \o f)

Statement as written in the source

Lemma integrable_gauss_bounded n (f : 'rV[R]_n -> R) (C : R) :
  measurable_fun [set: 'rV[R]_n] f -> (forall y, `|f y| <= C) ->
  (gauss n).-integrable [set: 'rV[R]_n] (EFin \o f).

Used by 12 declarations in 3 files

this file: iGa, gauss_smooth_bounded, gauss_smooth_lipschitz, gauss_smooth_close
GaussianAnalysis.comparison.gauss_law: gauss_smooth_partial_stein, normr_Rintegral_gauss_le, gauss_law_lipschitz, gauss_mulmx_law
GaussianAnalysis.comparison.brascamp_lieb: gauss_ibp_unit, integrable_G, dLambda_le0, Lambda_lip

lemma integrable_normal_expR_abs source, line 171

forall {R : realType} (c : R),
(normal_prob 0 1).-integrable [set: R]
  (fun
     u : g_sigma_algebraType
           (R.-ocitv).-measurable =>
   (expR (c * `|u|))%:E)

Statement as written in the source

Lemma integrable_normal_expR_abs (c : R) :
  N.-integrable [set: R] (fun u => (expR (c * `|u|))%:E).

Used by 2 declarations in 2 files

this file: integrable_gauss_expR_abs_coord
GaussianAnalysis.comparison.ornstein_uhlenbeck: is_derive_normal_kernel

lemma integrable_gauss_expR_abs_coord source, line 186

forall {R : realType} [n : nat] (j : 'I_n) (c : R),
(gauss n).-integrable [set: 'rV_n] (fun y : 'rV_n => (expR (c * `|y 0 j|))%:E)

Statement as written in the source

Lemma integrable_gauss_expR_abs_coord n (j : 'I_n) (c : R) :
  (gauss n).-integrable [set: 'rV[R]_n] (fun y => (expR (c * `|y 0 j|))%:E).

Used by 1 declaration in 1 file

this file: gauss_smooth_derive

sectiongauss_smooth

Context {R : realType} {n : nat}.

definition gauss_smooth source, line 202

Type

forall {R : realType} {n : nat}, R -> ('rV_n -> R) -> 'rV_n -> R

Definition

Definition gauss_smooth (eps : R) (G : 'rV[R]_n -> R) (x : 'rV[R]_n) : R :=
  \int[gauss n]_y G (x + eps *: y).

The Gaussian smoothing of G at scale eps, x |-> E[G (x + eps y)] for y of law gauss n, and its candidate partial derivatives.

Used by 17 declarations in 3 files

this file: gauss_smooth_bounded, gauss_smooth_lipschitz, gauss_smooth_shift, gauss_smooth_derive, gauss_smooth_differentiable, gauss_smooth_close
GaussianAnalysis.comparison.gauss_concentration: lip_approx
GaussianAnalysis.comparison.gauss_law: FK, FL, Fd, gauss_smooth_partial_stein, H_partial, DH_partial, H_poly, DH_poly, gauss_law_double_smooth, gauss_law_lipschitz

definition gauss_smooth_partial source, line 205

Type

forall {R : realType} {n : nat}, R -> ('rV_n -> R) -> 'I_n -> 'rV_n -> R

Definition

Definition gauss_smooth_partial (eps : R) (G : 'rV[R]_n -> R) (j : 'I_n)
    (x : 'rV[R]_n) : R :=
  eps^-1 * \int[gauss n]_y (G (x + eps *: y) * y 0 j).

Used by 15 declarations in 3 files

this file: gauss_smooth_derive, continuous_gauss_smooth_partial, gauss_smooth_grad
GaussianAnalysis.comparison.gauss_concentration: lip_approx_mgf
GaussianAnalysis.comparison.gauss_law: gauss_smooth_partial_bounded, gauss_smooth_partial_lipschitz, FjK, FjL, Fd, gauss_smooth_partial_stein, H_partial, DH_partial, D2H_cont, DH_poly, D2H_poly

Variables (G : 'rV[R]_n -> R) (K L eps : R).
Hypothesis GK : forall x, `|G x| <= K.
Hypothesis GL : forall x y, `|G x - G y| <= L * frobenius (x - y).
Hypothesis eps0 : 0 < eps.

let K0 section-local source, line 214

Let K0 : 0 <= K := le_trans (normr_ge0 _) (GK 0).

let cG section-local source, line 215

Let cG : continuous G := lipschitz_frobenius_continuous GL.

Used by 1 declaration in 1 file

this file: mG

let mG section-local source, line 216

Let mG : measurable_fun [set: 'rV[R]_n] G := continuous_measurable_mx cG.

Used by 1 declaration in 1 file

this file: mGa

let maff section-local source, line 218

Let maff (x : 'rV[R]_n) (c : R) :
  measurable_fun [set: 'rV[R]_n] (fun y : 'rV[R]_n => x + c *: y).

Used by 1 declaration in 1 file

this file: mGa

let mGa section-local source, line 225

Let mGa x c : measurable_fun [set: 'rV[R]_n] (fun y => G (x + c *: y)) :=
  measurableT_comp mG (maff x c).

Used by 2 declarations in 1 file

this file: iGa, gauss_smooth_derive

let iGa section-local source, line 228

Let iGa x c : (gauss n).-integrable [set: 'rV[R]_n] (EFin \o (fun y => G (x + c *: y))) :=
  integrable_gauss_bounded (mGa x c) (fun y => GK _).

Used by 1 declaration in 1 file

this file: gauss_smooth_close

let iGa_coord section-local source, line 231

Let iGa_coord x c j :
  (gauss n).-integrable [set: 'rV[R]_n] (EFin \o (fun y => G (x + c *: y) * y 0 j)).

Used by 2 declarations in 1 file

this file: gauss_smooth_derive, continuous_gauss_smooth_partial

lemma gauss_smooth_bounded source, line 242

forall {R : realType} {n : nat} [G : 'rV_n -> R] [K L : R] (eps : R),
(forall x : 'rV_n, `|G x| <= K) ->
(forall x y : 'rV_n, `|G x - G y| <= L * frobenius (x - y)) ->
forall x : 'rV_n, `|gauss_smooth eps G x| <= K

Statement as written in the source

Lemma gauss_smooth_bounded x : `|gauss_smooth eps G x| <= K.

Used by 6 declarations in 2 files

GaussianAnalysis.comparison.gauss_concentration: lip_approx_mgf, gauss_concentration
GaussianAnalysis.comparison.gauss_law: FK, H_poly, DH_poly, gauss_law_lipschitz

lemma gauss_smooth_lipschitz source, line 254

forall {R : realType} {n : nat} [G : 'rV_n -> R] [K L : R] (eps : R),
(forall x : 'rV_n, `|G x| <= K) ->
(forall x y : 'rV_n, `|G x - G y| <= L * frobenius (x - y)) ->
forall x x' : 'rV_n,
`|gauss_smooth eps G x - gauss_smooth eps G x'| <= L * frobenius (x - x')

Statement as written in the source

Lemma gauss_smooth_lipschitz x x' :
  `|gauss_smooth eps G x - gauss_smooth eps G x'| <= L * frobenius (x - x').

Used by 4 declarations in 3 files

this file: gauss_smooth_grad
GaussianAnalysis.comparison.gauss_concentration: mA
GaussianAnalysis.comparison.gauss_law: FL, gauss_law_lipschitz

let e0 section-local source, line 275

Let e0 : eps != 0 := lt0r_neq0 eps0.

let q section-local source, line 279

Let q (u a : R) := a * (u / eps) - a ^+ 2 / (2 * eps ^+ 2).

The exponent of the Cameron-Martin density for the shift a along a coordinate u of y, after the scaling by eps.

Used by 3 declarations in 1 file

this file: is_derive_q, gauss_smooth_shift, gauss_smooth_derive

let is_derive_q section-local source, line 281

Let is_derive_q (u a : R) : is_derive a 1 (q u) (u / eps - a / eps ^+ 2).

Used by 1 declaration in 1 file

this file: gauss_smooth_derive

let gauss_smooth_shift section-local source, line 294

Let gauss_smooth_shift x j (a : R) :
  gauss_smooth eps G (a *: delta_mx 0 j + x) =
  \int[gauss n]_y (G (x + eps *: y) * expR (q (y 0 j) a)).

By the Cameron-Martin formula, shifting x along the j-th coordinate by a multiplies the law of y by expR (q (y 0 j) a).

Used by 1 declaration in 1 file

this file: gauss_smooth_derive

lemma gauss_smooth_derive main result source, line 311

forall {R : realType} {n : nat} [G : 'rV_n -> R] [K L eps : R],
(forall x : 'rV_n, `|G x| <= K) ->
(forall x y : 'rV_n, `|G x - G y| <= L * frobenius (x - y)) ->
0 < eps ->
forall (x : 'rV[R]_n)
  (j : 'I_n),
is_derive x (delta_mx 0 j) (gauss_smooth eps G) (gauss_smooth_partial eps G j x)

Main result, as the README states it

For G bounded and L-Lipschitz (Euclidean norm) and eps > 0, the Gaussian smoothing x |-> E[G (x + eps y)] is differentiable, with partial derivatives E[G (x + eps y) y_j] / eps, continuous, of gradient norm at most L, and within L eps E[|y|] of G.

Statement as written in the source

Lemma gauss_smooth_derive x j :
  is_derive x (delta_mx 0 j) (gauss_smooth eps G) (gauss_smooth_partial eps G j x).

Used by 6 declarations in 3 files

this file: gauss_smooth_differentiable, gauss_smooth_grad
GaussianAnalysis.comparison.gauss_concentration: lip_approx_mgf
GaussianAnalysis.comparison.gauss_law: Fd, H_partial, DH_partial

lemma continuous_gauss_smooth_partial source, line 386

forall {R : realType} {n : nat} [G : 'rV_n -> R] [K L eps : R],
(forall x : 'rV_n, `|G x| <= K) ->
(forall x y : 'rV_n, `|G x - G y| <= L * frobenius (x - y)) ->
0 < eps -> forall [j : 'I_n], continuous (gauss_smooth_partial eps G j)

Statement as written in the source

Lemma continuous_gauss_smooth_partial j : continuous (gauss_smooth_partial eps G j).

Used by 4 declarations in 3 files

this file: gauss_smooth_differentiable, gauss_smooth_grad
GaussianAnalysis.comparison.gauss_concentration: lip_approx_mgf
GaussianAnalysis.comparison.gauss_law: D2H_cont

theorem gauss_smooth_differentiable main result source, line 421

forall {R : realType} {n : nat} [G : 'rV_n -> R] [K L eps : R],
(forall x : 'rV_n, `|G x| <= K) ->
(forall x y : 'rV_n, `|G x - G y| <= L * frobenius (x - y)) ->
0 < eps ->
forall x : 'rV[R]_n,
differentiable (gauss_smooth eps G : 'rV_n -> R^o) x

Main result

Stated in the README together with gauss_smooth_derive.

Statement as written in the source

Theorem gauss_smooth_differentiable x :
  differentiable (gauss_smooth eps G : 'rV[R]_n -> R^o) x.

theorem gauss_smooth_grad main result source, line 428

forall {R : realType} {n : nat} [G : 'rV_n -> R] [K L eps : R],
(forall x : 'rV_n, `|G x| <= K) ->
(forall x y : 'rV_n, `|G x - G y| <= L * frobenius (x - y)) ->
0 < eps ->
forall x : 'rV_n,
mxdot (\row_j gauss_smooth_partial eps G j x) (\row_j gauss_smooth_partial eps G j x) <=
L ^+ 2

Main result

Stated in the README together with gauss_smooth_derive.

Statement as written in the source

Theorem gauss_smooth_grad x :
  mxdot (\row_j gauss_smooth_partial eps G j x) (\row_j gauss_smooth_partial eps G j x)
    <= L ^+ 2.

Used by 1 declaration in 1 file

GaussianAnalysis.comparison.gauss_concentration: lip_approx_mgf

lemma integrable_gauss_frobenius source, line 436

forall {R : realType} {n : nat},
(gauss n).-integrable [set: 'rV_n] (EFin \o [eta frobenius (n:=n)])

Statement as written in the source

Lemma integrable_gauss_frobenius :
  (gauss n).-integrable [set: 'rV[R]_n] (EFin \o (fun y : 'rV[R]_n => frobenius y)).

Used by 11 declarations in 7 files

GaussianAnalysis.random_matrix.goe: gauss_frobenius_mean
GaussianAnalysis.random_matrix.goe_edge: goe_form_max_mean
this file: gauss_smooth_close
GaussianAnalysis.comparison.gauss_concentration: integrable_gauss_lipschitz
GaussianAnalysis.comparison.escape: gordon_escape, gordon_minmax, gauss_opnorm_mean
GaussianAnalysis.comparison.cgmt: infsup_compare, cgmt_lower, cgmt_upper
GaussianAnalysis.comparison.gauss_law: iF

lemma gauss_smooth_close main result source, line 447

forall {R : realType} {n : nat} [G : 'rV_n -> R] [K L eps : R],
(forall x : 'rV_n, `|G x| <= K) ->
(forall x y : 'rV_n, `|G x - G y| <= L * frobenius (x - y)) ->
0 < eps ->
forall x : 'rV_n, `|gauss_smooth eps G x - G x| <= L * eps * \int[gauss n]_y frobenius y

Main result

Stated in the README together with gauss_smooth_derive.

Statement as written in the source

Lemma gauss_smooth_close x :
  `|gauss_smooth eps G x - G x| <= L * eps * \int[gauss n]_y frobenius y.

Used by 3 declarations in 2 files

GaussianAnalysis.comparison.gauss_concentration: lip_approx_dom, lip_approx_cvg
GaussianAnalysis.comparison.gauss_law: gauss_law_lipschitz

Generated from commit 9046883 (tag phase12) of the ellipsoid fitting repository. Signatures are printed by Rocq 9.1.1; links in the source statements come from the compiled .glob files. The source links open the files on GitHub at this commit, in the now-public repository.