English
For χ Dirichlet character, the Fourier transform is given by a Gauss sum with a shift of the additive character: 𝓕 χ(k) = gaussSum χ (stdAddChar.mulShift(-k)).
Русский
Для χ-Дирихле персона сумма Фурье задаётся гауссовой суммой сдвига-additive-character: 𝓕 χ(k) = gaussSum χ (stdAddChar.mulShift(-k)).
LaTeX
$$$\\\\mathcal{F} χ(k) = gaussSum χ (stdAddChar.mulShift (-k))$$$
Lean4
/-- Auxiliary result for the grid-lines lemma. Given a nonnegative function on a finitary product
type indexed by `ι`, and a set `s` in `ι`, consider partially integrating over the variables in
`sᶜ` and performing the "grid-lines operation" (see `GridLines.T`) to the resulting function in the
variables `s`. This theorem states that this operation decreases as the number of grid-lines taken
increases. -/
theorem T_lmarginal_antitone [Fintype ι] [∀ i, SigmaFinite (μ i)] (hp₀ : 0 ≤ p) (hp : (#ι - 1 : ℝ) * p ≤ 1)
{f : (∀ i, A i) → ℝ≥0∞} (hf : Measurable f) : Antitone (fun s ↦ T μ p (∫⋯∫⁻_sᶜ, f ∂μ) s) := by
-- Reformulate (by induction): a function is decreasing on `Finset ι` if it decreases under the
-- insertion of any element to any set.
rw [Finset.antitone_iff_forall_insert_le]
intro s i hi
convert T_insert_le_T_lmarginal_singleton μ hp₀ s ?_ i hi (hf.lmarginal μ) using 2
· rw [← lmarginal_union μ f hf]
· rw [← insert_compl_insert hi]
rfl
rw [Finset.disjoint_singleton_left, notMem_compl]
exact mem_insert_self i s
· -- the main nontrivial point is to check that an exponent `p` satisfying `0 ≤ p` and
-- `(#ι - 1) * p ≤ 1` is in the valid range for the inductive-step lemma
refine le_trans ?_ hp
gcongr
suffices (s.card : ℝ) + 1 ≤ #ι by linarith
rw [← card_add_card_compl s]
norm_cast
gcongr
have hi' : sᶜ.Nonempty := ⟨i, by rwa [Finset.mem_compl]⟩
rwa [← card_pos] at hi'
