Chang's spectrum theorem and finite Bohr sets

This file was automatically generated by Codex.

Quantitative finite harmonic analysis for arbitrary finite abelian groups. Circle-valued homomorphisms define Bohr sets; additive characters define large spectra. The spectrum argument uses Mathlib's dissociation and Riesz-product randomisation identities. The reference is blueprint lem:Chang, lines 730-764.

noncomputable def TrilinearHT.Auto.finiteBohrSet {G : Type u_1} {ι : Type u_2} [Fintype G] [AddCommGroup G] (phase : ι → G →+ UnitAddCircle) (ρ : ℝ) : Finset G

The source Bohr condition, expressed through the quotient-circle norm.

Equations

• TrilinearHT.Auto.finiteBohrSet phase ρ = {x : G | ∀ (i : ι), ‖(phase i) x‖ < ρ}

theorem TrilinearHT.Auto.mem_finiteBohrSet {G : Type u_1} {ι : Type u_2} [Fintype G] [AddCommGroup G] (phase : ι → G →+ UnitAddCircle) (ρ : ℝ) (x : G) : x ∈ finiteBohrSet phase ρ ↔ ∀ (i : ι), ‖(phase i) x‖ < ρ

noncomputable def TrilinearHT.Auto.unitCircleBin (N : ℕ) (hN : 0 < N) (x : UnitAddCircle) : Fin N

A half-open equal-length partition of the unit circle.

Equations

• TrilinearHT.Auto.unitCircleBin N hN x = ⟨⌊↑N * ↑((AddCircle.equivIco 1 0) x)⌋₊, ⋯⟩

theorem TrilinearHT.Auto.unitCircleBin_norm_sub_lt {N : ℕ} (hN : 0 < N) {x y : UnitAddCircle} (hbin : unitCircleBin N hN x = unitCircleBin N hN y) : ‖x - y‖ < 1 / ↑N

Points in one partition interval differ by less than 1/N in circle norm.

theorem TrilinearHT.Auto.bohr_partition_size {ρ : ℝ} (hρ : 0 < ρ) (hρ1 : ρ < 1) : 0 < ⌈2 / ρ⌉₊ ∧ 1 / ↑⌈2 / ρ⌉₊ ≤ ρ / 2 ∧ ↑⌈2 / ρ⌉₊ ≤ 3 / ρ

The source partition size ceil(2/rho) has mesh at most rho/2 and at most 3/rho intervals.

theorem TrilinearHT.Auto.finiteBohrSet_card_lower {G : Type u_1} {ι : Type u_2} [Fintype G] [AddCommGroup G] [Fintype ι] (phase : ι → G →+ UnitAddCircle) {ρ : ℝ} (hρ : 0 < ρ) (hρhalf : ρ < 1 / 2) : (ρ / 3) ^ Fintype.card ι * ↑(Fintype.card G) ≤ ↑(finiteBohrSet phase ρ).card

Blueprint lem:Chang, lines 735-748: a Bohr set defined by d circle coordinates has at least (rho/3)^d of the group elements. The zero-coordinate case and repeated or zero homomorphisms are included.

Aligned characters and positive Riesz products

noncomputable def TrilinearHT.Auto.characterMean {G : Type u_1} [AddCommGroup G] (X : Finset G) (ψ : AddChar G ℂ) : ℂ

The probability-normalized average of a character on a finite set.

Equations

• TrilinearHT.Auto.characterMean X ψ = X.expect fun (x : G) => ψ x

theorem TrilinearHT.Auto.characterMean_phase {G : Type u_1} [AddCommGroup G] (X : Finset G) (ψ : AddChar G ℂ) : ∃ (ω : ℂ), ‖ω‖ = 1 ∧ (X.expect fun (x : G) => (ω * ψ x).re) = ‖characterMean X ψ‖

Rotate a Fourier coefficient so its real part is its norm.

noncomputable def TrilinearHT.Auto.finiteRieszProduct {G : Type u_1} [AddCommGroup G] (Λ : Finset (AddChar G ℂ)) (ω : AddChar G ℂ → ℂ) (t : ℝ) (x : G) : ℝ

The real Riesz product for finitely many additive characters.

Equations

• TrilinearHT.Auto.finiteRieszProduct Λ ω t x = ∏ ψ ∈ Λ, (1 + t * (ω ψ * ψ x).re)

theorem TrilinearHT.Auto.character_rotated_re_abs_le {G : Type u_1} [Finite G] [AddCommGroup G] (ψ : AddChar G ℂ) {ω : ℂ} (hω : ‖ω‖ = 1) (x : G) : |(ω * ψ x).re| ≤ 1

theorem TrilinearHT.Auto.finiteRieszProduct_pos {G : Type u_1} [Finite G] [AddCommGroup G] (Λ : Finset (AddChar G ℂ)) (ω : AddChar G ℂ → ℂ) (hω : ∀ ψ ∈ Λ, ‖ω ψ‖ = 1) {t : ℝ} (ht : 0 ≤ t) (ht1 : t ≤ 1 / 2) (x : G) : 0 < finiteRieszProduct Λ ω t x

Every factor in the source product is strictly positive for 0 <= t <= 1/2.

theorem TrilinearHT.Auto.finiteRieszProduct_mean_one {G : Type u_1} [Fintype G] [AddCommGroup G] (Λ : Finset (AddChar G ℂ)) (hΛ : AddDissociated ↑Λ) (ω : AddChar G ℂ → ℂ) (t : ℝ) : (Finset.univ.expect fun (x : G) => finiteRieszProduct Λ ω t x) = 1

Blueprint lem:Chang, lines 749-757: dissociation annihilates all nonconstant terms, so the finite Riesz product has normalized mean one.

The logarithmic estimate and entropy bound

theorem TrilinearHT.Auto.log_one_add_quadratic_lower {v : ℝ} (hv : |v| ≤ 1 / 2) : v - v ^ 2 ≤ Real.log (1 + v)

The elementary logarithm estimate on the entire source interval.

theorem TrilinearHT.Auto.log_riesz_factor_lower {u t : ℝ} (hu : |u| ≤ 1) (ht : 0 ≤ t) (ht1 : t ≤ 1 / 2) : t * u - t ^ 2 ≤ Real.log (1 + t * u)

Blueprint lem:Chang, line 758: log(1+t*u) >= t*u-t^2 for |u| <= 1 and 0 <= t <= 1/2.

theorem TrilinearHT.Auto.finiteRieszProduct_log_mean_lower {G : Type u_1} [Finite G] [AddCommGroup G] (X : Finset G) (hX : X.Nonempty) (Λ : Finset (AddChar G ℂ)) (ω : AddChar G ℂ → ℂ) (hω : ∀ ψ ∈ Λ, ‖ω ψ‖ = 1) {η : ℝ} (hη : 0 < η) (hη1 : η ≤ 1) (halign : ∀ ψ ∈ Λ, η ≤ X.expect fun (x : G) => (ω ψ * ψ x).re) : ↑Λ.card * η ^ 2 / 4 ≤ X.expect fun (x : G) => Real.log (finiteRieszProduct Λ ω (η / 2) x)

Averaging the source logarithm estimate over a nonempty set.

theorem TrilinearHT.Auto.finite_log_mean_le_log_mean {α : Type u_1} (X : Finset α) (hX : X.Nonempty) (F : α → ℝ) (hF : ∀ x ∈ X, 0 < F x) : (X.expect fun (x : α) => Real.log (F x)) ≤ Real.log (X.expect fun (x : α) => F x)

Finite Jensen in the logarithmic form used by the entropy argument.

theorem TrilinearHT.Auto.finite_log_mean_le_log_density_inv {G : Type u_1} [Fintype G] (X : Finset G) (hX : X.Nonempty) (F : G → ℝ) (hF : ∀ (x : G), 0 < F x) (hmean : (Finset.univ.expect fun (x : G) => F x) = 1) : (X.expect fun (x : G) => Real.log (F x)) ≤ Real.log (↑(Fintype.card G) / ↑X.card)

A positive function of global mean one has mean logarithm on X at most the logarithm of the reciprocal density of X.

theorem TrilinearHT.Auto.dissociated_spectrum_card_bound {G : Type u_1} [Fintype G] [AddCommGroup G] (X : Finset G) (hX : X.Nonempty) (Λ : Finset (AddChar G ℂ)) (hΛ : AddDissociated ↑Λ) {η : ℝ} (hη : 0 < η) (hη1 : η ≤ 1) (hlarge : ∀ ψ ∈ Λ, η ≤ ‖characterMean X ψ‖) : ↑Λ.card ≤ 4 / η ^ 2 * Real.log (↑(Fintype.card G) / ↑X.card)

Blueprint lem:Chang, lines 749-763: every dissociated family of characters with average norm at least eta has cardinality at most 4 eta^(-2) log(1/beta), where beta = |X|/|G|.

Generating the large spectrum

noncomputable def TrilinearHT.Auto.largeCharacterSpectrum {G : Type u_1} [Fintype G] [AddCommGroup G] (X : Finset G) (η : ℝ) : Finset (AddChar G ℂ)

The large spectrum of a uniform finite-set measure, in the character dual.

Equations

• TrilinearHT.Auto.largeCharacterSpectrum X η = {ψ : AddChar G ℂ | η ≤ ‖TrilinearHT.Auto.characterMean X ψ‖}

theorem TrilinearHT.Auto.mem_largeCharacterSpectrum {G : Type u_1} [Fintype G] [AddCommGroup G] (X : Finset G) (η : ℝ) (ψ : AddChar G ℂ) : ψ ∈ largeCharacterSpectrum X η ↔ η ≤ ‖characterMean X ψ‖

theorem TrilinearHT.Auto.characterSpectrum_generators {G : Type u_1} [Fintype G] [AddCommGroup G] (X : Finset G) (hX : X.Nonempty) {η : ℝ} (hη : 0 < η) (hη1 : η ≤ 1) : ∃ Λ ⊆ largeCharacterSpectrum X η, ↑Λ.card ≤ 4 / η ^ 2 * Real.log (↑(Fintype.card G) / ↑X.card) ∧ largeCharacterSpectrum X η ⊆ Λ.addSpan

Chang's spectrum-generating conclusion for an arbitrary finite abelian group. The span is Mathlib's signed span with coefficients in {-1,0,1}.

theorem TrilinearHT.Auto.addSpan_image_equiv {G : Type u_1} {H : Type u_2} [AddCommGroup G] [AddCommGroup H] [Fintype G] [Fintype H] [DecidableEq G] [DecidableEq H] (e : G ≃+ H) (S : Finset G) : (Finset.image (⇑e) S).addSpan = Finset.image (⇑e) S.addSpan

Signed spans commute with an additive equivalence.

Cyclic frequencies and Bohr sets

noncomputable def TrilinearHT.Auto.cyclicFrequencyEquiv (q : ℕ) [NeZero q] : ZMod q ≃+ AddChar (ZMod q) ℂ

Identify a cyclic frequency with its negative-exponent Fourier character.

Equations

• TrilinearHT.Auto.cyclicFrequencyEquiv q = AddEquiv.ofBijective { toFun := fun (ξ : ZMod q) => ZMod.stdAddChar.mulShift (-ξ), map_zero' := ⋯, map_add' := ⋯ } ⋯

theorem TrilinearHT.Auto.cyclicFrequencyEquiv_apply (q : ℕ) [NeZero q] (ξ x : ZMod q) : ((cyclicFrequencyEquiv q) ξ) x = ZMod.stdAddChar (-(ξ * x))

noncomputable def TrilinearHT.Auto.cyclicBohrSet {q : ℕ} [NeZero q] (S : Finset (ZMod q)) (ρ : ℝ) : Finset (ZMod q)

The source cyclic Bohr set, using the exact quotient-circle norm of s*x/q.

Equations

• TrilinearHT.Auto.cyclicBohrSet S ρ = TrilinearHT.Auto.finiteBohrSet (fun (s : ↥S) => ZMod.toAddCircle.comp (AddMonoidHom.mulLeft ↑s)) ρ

theorem TrilinearHT.Auto.mem_cyclicBohrSet {q : ℕ} [NeZero q] (S : Finset (ZMod q)) (ρ : ℝ) (x : ZMod q) : x ∈ cyclicBohrSet S ρ ↔ ∀ s ∈ S, ‖ZMod.toAddCircle (s * x)‖ < ρ

theorem TrilinearHT.Auto.cyclicBohrSet_card_lower {q : ℕ} [NeZero q] (S : Finset (ZMod q)) {ρ : ℝ} (hρ : 0 < ρ) (hρhalf : ρ < 1 / 2) : (ρ / 3) ^ S.card * ↑q ≤ ↑(cyclicBohrSet S ρ).card

Blueprint lem:Chang, first conclusion in its cyclic form.