English
For primitive χ, the same transform equals χ⁻¹(-k) times gaussSum χ stdAddChar.
Русский
Для примитивной χ имеется 𝓕 χ(k) = χ⁻¹(-k) · gaussSum χ stdAddChar.
LaTeX
$$$\\\\mathcal{F} χ(k) = χ^{-1}(-k) \\\\cdot gaussSum χ stdAddChar$$$
Lean4
/-- The "grid-lines lemma" (not a standard name), stated with a general parameter `p` as the
exponent. Compare with `lintegral_prod_lintegral_pow_le`.
For any finite dependent product `Π i : ι, A i` of sigma-finite measure spaces, for any
nonnegative real number `p` such that `(#ι - 1) * p ≤ 1`, for any function `f` from `Π i, A i` into
the extended nonnegative reals, we consider an associated "grid-lines quantity", the integral of an
associated function from `Π i, A i` into the extended nonnegative reals. The value of this function
at `x : Π i, A i` is obtained by multiplying a certain power of `f` with the product, for each
co-ordinate `i`, of a certain power of the integral of `f` along the "grid line" in the `i`
direction through `x`.
This lemma bounds the Lebesgue integral of the grid-lines quantity by a power of the Lebesgue
integral of `f`. -/
theorem lintegral_mul_prod_lintegral_pow_le [Fintype ι] [∀ i, SigmaFinite (μ i)] {p : ℝ} (hp₀ : 0 ≤ p)
(hp : (#ι - 1 : ℝ) * p ≤ 1) {f : (∀ i : ι, A i) → ℝ≥0∞} (hf : Measurable f) :
∫⁻ x, f x ^ (1 - (#ι - 1 : ℝ) * p) * ∏ i, (∫⁻ xᵢ, f (update x i xᵢ) ∂μ i) ^ p ∂.pi μ ≤
(∫⁻ x, f x ∂.pi μ) ^ (1 + p) :=
by
cases isEmpty_or_nonempty (∀ i, A i)
· simp_rw [lintegral_of_isEmpty]; refine zero_le _
inhabit ∀ i, A i
have H : (∅ : Finset ι) ≤ Finset.univ := Finset.empty_subset _
simpa [lmarginal_univ] using GridLines.T_lmarginal_antitone μ hp₀ hp hf H default
