# `HypercontractiveNat.lean` -- Informal Summary

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

## Overview

Proves the hypercontractive inequality for even integer $p = 2m$, bypassing the Gamma function entirely via a combinatorial argument on double factorials. The proof has three parts: (1) bridge from Gamma moments to double factorials via $E[Z^{2n}] = (2n-1)!!$, (2) a combinatorial inequality $(2mn-1)!! \le (2m-1)^{mn} \cdot ((2n-1)!!)^m$ proved by partitioning products into blocks, and (3) lifting through variance scaling and pushforward to obtain the full Nelson hypercontractive estimate for even $p$.

## Status

**Main result**: Fully proven

None -- file is sorry-free.

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

---

## Part 1: Bridge from Gamma moments to double factorials

### [`gaussian_even_moment_eq_doubleFactorial`](../../GaussianField/HypercontractiveNat.lean#L47) -- Theorem

**Statement**: For $Z \sim N(0,1)$, $E[\lvert Z \rvert^{2n}] = (2n-1)!!$.

**Proof uses**: [`gaussian_abs_moment_std`](../../GaussianField/Hypercontractive.lean#L95), `Real.Gamma_nat_add_half`

---

### [`gaussian_even_moment_pow_eq_doubleFactorial`](../../GaussianField/HypercontractiveNat.lean#L66) -- Theorem

**Statement**: Same as above in the $\mathbb{N}$-power form: $\int \lvert x \rvert^{2n}\,d\gamma = (2n-1)!!$.

**Proof uses**: [`gaussian_even_moment_eq_doubleFactorial`](../../GaussianField/HypercontractiveNat.lean#L47), `Real.rpow_natCast`

---

## Part 2: Combinatorial double-factorial inequality

### [`doubleFactorial_hypercontractive_bound`](../../GaussianField/HypercontractiveNat.lean#L138) -- Theorem

**Statement**: **Core combinatorial inequality**: $(2mn - 1)!! \le (2m-1)^{mn} \cdot ((2n-1)!!)^m$. Proved by partitioning $\prod_{k=0}^{mn-1}(2k+1)$ into $n$ blocks of $m$ terms, bounding each block.

**Proof uses**: `doubleFactorial_as_prod`, `prod_repartition`, `block_prod_bound`

---

## Part 3: Hypercontractive inequality for even integer p

### [`hypercontractive_1d_even`](../../GaussianField/HypercontractiveNat.lean#L164) -- Theorem

**Statement**: For $Z \sim N(0,1)$, $m \ge 1$, $n \in \mathbb{N}$: $E[\lvert Z \rvert^{2mn}] \le (2m-1)^{mn} \cdot (E[\lvert Z \rvert^{2n}])^m$.

**Proof uses**: [`gaussian_even_moment_pow_eq_doubleFactorial`](../../GaussianField/HypercontractiveNat.lean#L66), [`doubleFactorial_hypercontractive_bound`](../../GaussianField/HypercontractiveNat.lean#L138)

---

### [`hypercontractive_1d_p4`](../../GaussianField/HypercontractiveNat.lean#L181) -- Theorem

**Statement**: Corollary for $p = 4$ ($m = 2$): $E[Z^{4n}] \le 3^{2n} \cdot (E[Z^{2n}])^2$.

**Proof uses**: [`hypercontractive_1d_even`](../../GaussianField/HypercontractiveNat.lean#L164)

---

## Full hypercontractive chain for even integer p

### [`hypercontractive_1d`](../../GaussianField/HypercontractiveNat.lean#L205) -- Lemma

**Statement**: For $Z \sim N(0,1)$, $p = 2m \ge 2$: $E[\lvert Z \rvert^{pn}] \le (p-1)^{pn/2} \cdot (E[\lvert Z \rvert^{2n}])^{p/2}$.

**Proof uses**: [`hypercontractive_1d_even`](../../GaussianField/HypercontractiveNat.lean#L164)

---

### [`hypercontractive_gaussianReal`](../../GaussianField/HypercontractiveNat.lean#L225) -- Lemma

**Statement**: For $X \sim N(0,v)$, $p = 2m \ge 2$: $E[\lvert X \rvert^{pn}] \le (p-1)^{pn/2} \cdot (E[\lvert X \rvert^{2n}])^{p/2}$. Reduces to the standard case by scaling.

**Proof uses**: [`hypercontractive_1d`](../../GaussianField/HypercontractiveNat.lean#L205), `gaussianReal_map_const_mul`

---

### [`gaussian_hypercontractive`](../../GaussianField/HypercontractiveNat.lean#L299) -- Theorem

**Statement**: **Nelson's hypercontractive estimate** for the Gaussian measure (even $p$): for the centered Gaussian measure $\mu = \text{GaussianField.measure}\,T$ on $\text{Configuration}\,E$, with $p = 2m \ge 2$:
$$\int \lvert \omega(f) \rvert^{pn}\,d\mu \le (p-1)^{pn/2} \cdot \Bigl(\int \lvert \omega(f) \rvert^{2n}\,d\mu\Bigr)^{p/2}.$$

**Proof uses**: [`hypercontractive_gaussianReal`](../../GaussianField/HypercontractiveNat.lean#L225), [`pairing_is_gaussian`](../../GaussianField/Properties.lean), [`configuration_eval_measurable`](../../GaussianField/Properties.lean)

---

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