# `Hypercontractive.lean` -- Informal Summary

> **Source**: [`GaussianField/Hypercontractive.lean`](../../GaussianField/Hypercontractive.lean)
> **Generated**: 2026-03-03 11:30
> **Note**: Auto-generated by `/lean-summarize`. Re-run to refresh.

## Overview

Proves the Gross log-Sobolev inequality for the Gaussian measure via explicit moment computations. The key steps are: (1) absolute moments of the standard Gaussian via the Gamma function, (2) pointwise bound $x^2 \log(x^2/\sigma^2) \le x^4/\sigma^2 - x^2$ from $\log y \le y - 1$, (3) Gaussian moment identities $E[X^2] = \sigma^2$ and $E[X^4] = 3\sigma^4$, and (4) the full infinite-dimensional log-Sobolev inequality via reduction to the 1D case through `pairing_is_gaussian`.

## Status

**Main result**: Fully proven

None -- file is sorry-free.

**Length**: 441 lines, 0 definition(s) + 10 theorem(s)/lemma(s)

---

## Nelson's hypercontractive estimate

### [`gaussian_abs_moment_std`](../../GaussianField/Hypercontractive.lean#L95) -- Lemma

**Statement**: For $Z \sim N(0,1)$ and $k \ge 0$:
$$E[\lvert Z \rvert^k] = \frac{2^{k/2}\,\Gamma((k+1)/2)}{\sqrt{\pi}}.$$

**Proof uses**: `gaussian_abs_moment_std_aux`, `Real.sqrt_eq_rpow`, `rpow_add`

---

## Helper lemmas for the log-Sobolev inequality

### [`fourth_moment_standard_gaussian`](../../GaussianField/Hypercontractive.lean#L179) -- Lemma

**Statement**: $E[Z^4] = 3$ for $Z \sim N(0,1)$.

**Proof uses**: `iteratedDeriv_mgf_zero`, `mgf_fun_id_gaussianReal`, `hasDerivAt_exp_half_sq`, `hasDerivAt_t_mul_exp`, `hasDerivAt_quad_mul_exp`, `hasDerivAt_cubic_mul_exp`

---

### [`sq_log_div_le`](../../GaussianField/Hypercontractive.lean#L217) -- Lemma

**Statement**: For $x \ne 0$ and $\sigma^2 > 0$: $x^2 \log(x^2/\sigma^2) \le x^4/\sigma^2 - x^2$. Follows from $\log y \le y - 1$ applied to $y = x^2/\sigma^2$.

**Proof uses**: `Real.log_le_sub_one_of_pos`

---

### [`integral_sq_gaussianReal`](../../GaussianField/Hypercontractive.lean#L232) -- Lemma

**Statement**: The second moment of $N(0,v)$ equals $v$: $E[X^2] = v$.

**Proof uses**: `variance_fun_id_gaussianReal`, `variance_of_integral_eq_zero`, `integral_id_gaussianReal`

---

### [`integral_pow4_gaussianReal`](../../GaussianField/Hypercontractive.lean#L244) -- Lemma

**Statement**: The fourth moment of $N(0,v)$ equals $3v^2$: $E[X^4] = 3v^2$. Proved by scaling from the standard Gaussian.

**Proof uses**: [`fourth_moment_standard_gaussian`](../../GaussianField/Hypercontractive.lean#L179), `gaussianReal_map_const_mul`

---

### [`log_sobolev_1d`](../../GaussianField/Hypercontractive.lean#L282) -- Lemma

**Statement**: The 1D log-Sobolev inequality for linear functions: $\int x^2 \log(x^2/\sigma^2)\,d\gamma_{\sigma^2} \le 2\sigma^2$.

**Proof uses**: [`sq_log_div_le`](../../GaussianField/Hypercontractive.lean#L217), [`integral_pow4_gaussianReal`](../../GaussianField/Hypercontractive.lean#L244), [`integral_sq_gaussianReal`](../../GaussianField/Hypercontractive.lean#L232), `memLp_id_gaussianReal`

---

### [`gross_log_sobolev`](../../GaussianField/Hypercontractive.lean#L385) -- Theorem

**Statement**: **Gross log-Sobolev inequality** for the Gaussian measure: for the centered Gaussian measure $\mu = \text{GaussianField.measure}\,T$,
$$\int (\omega(f))^2 \log\Bigl(\frac{(\omega(f))^2}{E[(\omega(f))^2]}\Bigr)\,d\mu \le 2\,\lVert Tf \rVert^2.$$

**Proof uses**: [`second_moment_eq_covariance`](../../GaussianField/Properties.lean), [`pairing_is_gaussian`](../../GaussianField/Properties.lean), [`log_sobolev_1d`](../../GaussianField/Hypercontractive.lean#L282), [`pairing_memLp`](../../GaussianField/Properties.lean), [`measure_centered`](../../GaussianField/Properties.lean)

---

*This file has **0** definitions and **10** theorems/lemmas (0 with sorry).*