Documentation

TauCeti.Analysis.PositiveDefinite.Function.Difference

Differences of bounded positive-definite functions #

On an involutive commutative additive monoid M, a bounded positive-definite function F dominates each of its translates by a self-adjoint element: if star s = s, then

x ↦ F x - F (x + s)

is again positive definite. This is the function-level form of TauCeti.posSemidef_sub_comp_shift; self-adjointness of s is exactly what makes translation by s a symmetric shift of the kernel (a, b) ↦ F (a + star b).

That difference is the negative of Mathlib's forward difference Δ_[s] F, so iterating gives that the alternating iterated differences (-1) ^ n Δ_[s]^[n] F are positive definite too, in operator form and in the explicit binomial form

x ↦ ∑ k ≤ n, (-1) ^ k (n choose k) F (x + k • s).

Positive definiteness is a statement about quadratic forms, not a pointwise sign; the values themselves are nonnegative at the "norm points" a + star a.

Boundedness is only ever assumed at the "norm points" a + star a, the diagonal of the kernel: Cauchy--Schwarz propagates a bound there to every point of the form p + star q. It is essential and is not a technical artefact: t ↦ exp t is positive definite on the involutive monoid (ℝ≥0, +) with the trivial involution, and it increases. The statement is proved by a purely numerical moment-problem estimate on the finite quadratic forms; no topology, measurability, or representing measure is assumed or produced here.

This advances TauCetiRoadmap/OneParameterSemigroups/README.md, Part C: it is the closure property of the generic IsPositiveDefinite predicate that the Berg--Christensen--Ressel representation (Milestone 2) runs on. The zero-spatial time axis t ↦ F (t, 0) of a bounded positive-definite function on ℝ≥0 × V is such a function, for the trivial involution on ℝ≥0, and TauCeti/Analysis/PositiveDefinite/SemigroupGroup/Time/Difference.lean reads its complete monotonicity off the results below. The two-variable statements on ℝ≥0 × V itself are not instances of them — the involutive-monoid wrapper carrying the Berg--Christensen--Ressel involution is private to TauCeti/Analysis/PositiveDefinite/SemigroupGroup/Basic.lean — and are proved there from the Kolmogorov decomposition of the Berg--Christensen--Ressel kernel; only the forward-difference bookkeeping below is shared.

Main declarations #

References #

Forward-difference bookkeeping #

Pure identities about Mathlib's forward difference operator; no positive definiteness is involved.

source
theorem TauCeti.neg_one_pow_mul_fwdDiff_iter_succ {M : Type u_1} [AddCommMonoid M] (n : ℕ) (F : M → ℂ) (s : M) :
(fun (x : M) => (-1) ^ n * (fwdDiff s)^[n] (-fwdDiff s F) x) = fun (x : M) => (-1) ^ (n + 1) * (fwdDiff s)^[n + 1] F x

Differencing once advances the alternating iterated forward difference by one step. This is the bookkeeping behind every induction on the number of differencing steps.

source
theorem TauCeti.neg_one_pow_mul_fwdDiff_iter_eq_alternating_sum {M : Type u_1} [AddCommMonoid M] (n : ℕ) (F : M → ℂ) (s x : M) :
(-1) ^ n * (fwdDiff s)^[n] F x = ∑ k ∈ Finset.range (n + 1), (-1) ^ k * ↑(n.choose k) * F (x + k • s)

The alternating iterated forward difference as an explicit alternating binomial sum.

Differences of bounded positive-definite functions #

source
theorem TauCeti.IsPositiveDefinite.norm_apply_add_star_le {M : Type u_1} [AddCommMonoid M] [StarAddMonoid M] {F : M → ℂ} {C : ℝ} (hF : IsPositiveDefinite F) (hbdd : ∀ (a : M), ‖F (a + star a)‖ ≤ C) (p q : M) :
‖F (p + star q)‖ ≤ C

A positive-definite function bounded at the "norm points" a + star a is bounded at every point of the form p + star q, by Cauchy--Schwarz for its kernel.

source
theorem TauCeti.IsPositiveDefinite.sub_shift {M : Type u_1} [AddCommMonoid M] [StarAddMonoid M] {F : M → ℂ} {C : ℝ} {s : M} (hF : IsPositiveDefinite F) (hbdd : ∀ (a : M), ‖F (a + star a)‖ ≤ C) (hs : star s = s) :
IsPositiveDefinite fun (x : M) => F x - F (x + s)

A bounded positive-definite function dominates its translate by a self-adjoint element. Translation by s with star s = s is a symmetric shift of the kernel (a, b) ↦ F (a + star b), so the bounded-kernel estimate TauCeti.posSemidef_sub_comp_shift applies; only the diagonal of that kernel, the values at the "norm points" a + star a, has to be bounded. Boundedness cannot be dropped: t ↦ exp t is positive definite on ℝ≥0 with the trivial involution and increases.

source
theorem TauCeti.IsPositiveDefinite.sub_shift_add_star_self_nonneg {M : Type u_1} [AddCommMonoid M] [StarAddMonoid M] {F : M → ℂ} {C : ℝ} {s : M} (hF : IsPositiveDefinite F) (hbdd : ∀ (a : M), ‖F (a + star a)‖ ≤ C) (hs : star s = s) (a : M) :
0 ≤ F (a + star a) - F (a + star a + s)

The difference of a bounded positive-definite function and its translate by a self-adjoint element is nonnegative at every "norm point" a + star a.

source
theorem TauCeti.IsPositiveDefinite.neg_one_pow_mul_fwdDiff_iter {M : Type u_1} [AddCommMonoid M] [StarAddMonoid M] {F : M → ℂ} {C : ℝ} {s : M} (n : ℕ) (hF : IsPositiveDefinite F) (hbdd : ∀ (a : M), ‖F (a + star a)‖ ≤ C) (hs : star s = s) :
IsPositiveDefinite fun (x : M) => (-1) ^ n * (fwdDiff s)^[n] F x

The alternating iterated differences of a bounded positive-definite function are positive definite. This is the iterate of IsPositiveDefinite.sub_shift: each differencing step doubles the admissible bound, which is harmless because only the existence of some bound is used.

source
theorem TauCeti.IsPositiveDefinite.neg_one_pow_mul_fwdDiff_iter_add_star_self_nonneg {M : Type u_1} [AddCommMonoid M] [StarAddMonoid M] {F : M → ℂ} {C : ℝ} {s : M} (n : ℕ) (hF : IsPositiveDefinite F) (hbdd : ∀ (a : M), ‖F (a + star a)‖ ≤ C) (hs : star s = s) (a : M) :
0 ≤ (-1) ^ n * (fwdDiff s)^[n] F (a + star a)

The alternating iterated difference of a bounded positive-definite function is nonnegative at every "norm point" a + star a.

source
theorem TauCeti.IsPositiveDefinite.alternating_sum {M : Type u_1} [AddCommMonoid M] [StarAddMonoid M] {F : M → ℂ} {C : ℝ} {s : M} (n : ℕ) (hF : IsPositiveDefinite F) (hbdd : ∀ (a : M), ‖F (a + star a)‖ ≤ C) (hs : star s = s) :
IsPositiveDefinite fun (x : M) => ∑ k ∈ Finset.range (n + 1), (-1) ^ k * ↑(n.choose k) * F (x + k • s)

The alternating iterated differences, expanded as binomial sums, are positive definite. This is IsPositiveDefinite.neg_one_pow_mul_fwdDiff_iter with the forward-difference operator resolved into the explicit alternating sum over an arithmetic progression of translates.

source
theorem TauCeti.IsPositiveDefinite.alternating_sum_add_star_self_nonneg {M : Type u_1} [AddCommMonoid M] [StarAddMonoid M] {F : M → ℂ} {C : ℝ} {s : M} (n : ℕ) (hF : IsPositiveDefinite F) (hbdd : ∀ (a : M), ‖F (a + star a)‖ ≤ C) (hs : star s = s) (a : M) :
0 ≤ ∑ k ∈ Finset.range (n + 1), (-1) ^ k * ↑(n.choose k) * F (a + star a + k • s)

The alternating binomial sums of a bounded positive-definite function are nonnegative at every "norm point" a + star a: complete monotonicity in the finite-difference sense, along the arithmetic progression starting there.