Nonnegative trigonometric combinations

This file packages finite trigonometric combinations that are nonnegative on the complex unit circle. It also transfers their pointwise nonnegativity to the closed unit disk and the Taylor series of -log (1 - z), giving a reusable logarithmic inequality.

Main declarations

• TauCeti.trigonometricCombination is a finite weighted cosine combination.
• TauCeti.IsNonnegativeTrigonometricCombination asserts nonnegativity on the unit circle.
• TauCeti.trigonometricCombination_nonneg_of_boundary extends this nonnegativity to the closed unit disk.
• TauCeti.sum_re_neg_log_one_sub_nonneg transfers boundary nonnegativity to logarithms in the open unit disk.

Provenance

The logarithmic transfer generalizes the private lemma re_log_comb_nonneg' in the DirichletCharacter namespace of Mathlib's Mathlib/NumberTheory/LSeries/Nonvanishing.lean, due to Michael Stoll and David Loeffler, from the fixed 3-4-1 weights to an arbitrary finite nonnegative combination.

This is part of Layer 8.2 of TauCetiRoadmap/ArithmeticDirichletSeries/README.md.

def TauCeti.trigonometricCombination {ι : Type u_1} (s : Finset ι) (c : ι → ℝ) (m : ι → ℕ) (z : ℂ) : ℝ

The real trigonometric combination with weights c and frequencies m, evaluated at a complex phase z. On the unit circle, (z ^ k).re is a cosine.

Equations

• TauCeti.trigonometricCombination s c m z = ∑ i ∈ s, c i * (z ^ m i).re

theorem TauCeti.trigonometricCombination_def {ι : Type u_1} (s : Finset ι) (c : ι → ℝ) (m : ι → ℕ) (z : ℂ) : trigonometricCombination s c m z = ∑ i ∈ s, c i * (z ^ m i).re

The defining finite-sum formula for trigonometricCombination.

@[reducible, inline]

abbrev TauCeti.IsNonnegativeTrigonometricCombination {ι : Type u_1} (s : Finset ι) (c : ι → ℝ) (m : ι → ℕ) : Prop

The assertion that a finite trigonometric combination is nonnegative at every complex phase on the unit circle.

Equations

• TauCeti.IsNonnegativeTrigonometricCombination s c m = ∀ (z : ℂ), ‖z‖ = 1 → 0 ≤ TauCeti.trigonometricCombination s c m z

theorem TauCeti.trigonometricCombination_nonneg_of_boundary {ι : Type u_1} {s : Finset ι} {c : ι → ℝ} {m : ι → ℕ} (h : IsNonnegativeTrigonometricCombination s c m) {z : ℂ} (hz : ‖z‖ ≤ 1) : 0 ≤ trigonometricCombination s c m z

Nonnegativity of a trigonometric combination on the unit circle extends to the closed unit disk.

theorem TauCeti.sum_re_neg_log_one_sub_nonneg {ι : Type u_1} {s : Finset ι} {c : ι → ℝ} {m : ι → ℕ} (h : IsNonnegativeTrigonometricCombination s c m) {a : ℝ} (ha₀ : 0 ≤ a) (ha₁ : a < 1) {z : ℂ} (hz : ‖z‖ ≤ 1) : 0 ≤ ∑ i ∈ s, c i * (-Complex.log (1 - ↑a * z ^ m i)).re

Unit-circle nonnegativity of a trigonometric combination transfers to the Taylor series of -log (1 - z) throughout the closed unit disk.