Weighted closure for positive-definite functions

This file adds the weighted finite-mixture and Schur-power API for TauCeti.IsPositiveDefinite, the positive-definite-function predicate on an involutive additive monoid. The basic file already proves binary sums, nonnegative complex scalar multiples, pointwise products, and unweighted finite sums/products. Here we package the forms used by examples and finite approximations: finite nonnegative weighted sums, real-weighted variants, and powers. The weighted sum API is available in scalar (•) notation.

This advances TauCetiRoadmap/OneParameterSemigroups/README.md, Part C, the positive-definite functions API asking for closure under sums and products before the Bochner and BCR representation milestones. No external formalization is vendored.

Main declarations

• TauCeti.IsPositiveDefinite.real_smul: nonnegative real scalar multiplication.
• TauCeti.IsPositiveDefinite.sum_smul: finite nonnegative weighted sums.
• TauCeti.IsPositiveDefinite.sum_real_smul: finite nonnegative real-weighted sums.
• TauCeti.IsPositiveDefinite.pow: Schur powers of a positive-definite function.
• TauCeti.IsPositiveDefinite.sum_smul_apply_zero_of_apply_zero_eq_one: normalized finite mixtures evaluate at the origin as the sum of their weights.

References

• C. Berg, J. P. R. Christensen, P. Ressel, Harmonic Analysis on Semigroups (GTM 100, 1984), Chapter 3.

theorem TauCeti.IsPositiveDefinite.real_smul {M : Type u_1} [AddMonoid M] [StarAddMonoid M] {r : ℝ} {F : M → ℂ} (hr : 0 ≤ r) (hF : IsPositiveDefinite F) : IsPositiveDefinite fun (x : M) => r • F x

Positive-definite functions are closed under multiplication by a nonnegative real scalar.

theorem TauCeti.IsPositiveDefinite.sum_smul {M : Type u_1} [AddMonoid M] [StarAddMonoid M] {ι : Type u_2} {s : Finset ι} {w : ι → ℂ} {F : ι → M → ℂ} (hw : ∀ i ∈ s, 0 ≤ w i) (hF : ∀ i ∈ s, IsPositiveDefinite (F i)) : IsPositiveDefinite fun (x : M) => ∑ i ∈ s, w i • F i x

Finite nonnegative complex-weighted sums of positive-definite functions are positive definite. This is the finite-mixture form used when the weights are already complex scalars with nonnegative real value.

theorem TauCeti.IsPositiveDefinite.sum_const_mul {M : Type u_1} [AddMonoid M] [StarAddMonoid M] {ι : Type u_2} {s : Finset ι} {w : ι → ℂ} {F : ι → M → ℂ} (hw : ∀ i ∈ s, 0 ≤ w i) (hF : ∀ i ∈ s, IsPositiveDefinite (F i)) : IsPositiveDefinite fun (x : M) => ∑ i ∈ s, w i * F i x

Finite nonnegative complex-weighted sums, written using multiplication rather than scalar notation.

theorem TauCeti.IsPositiveDefinite.sum_real_smul {M : Type u_1} [AddMonoid M] [StarAddMonoid M] {ι : Type u_2} {s : Finset ι} {w : ι → ℝ} {F : ι → M → ℂ} (hw : ∀ i ∈ s, 0 ≤ w i) (hF : ∀ i ∈ s, IsPositiveDefinite (F i)) : IsPositiveDefinite fun (x : M) => ∑ i ∈ s, w i • F i x

Finite nonnegative real-weighted sums of positive-definite functions are positive definite.

theorem TauCeti.IsPositiveDefinite.sum_real_const_mul {M : Type u_1} [AddMonoid M] [StarAddMonoid M] {ι : Type u_2} {s : Finset ι} {w : ι → ℝ} {F : ι → M → ℂ} (hw : ∀ i ∈ s, 0 ≤ w i) (hF : ∀ i ∈ s, IsPositiveDefinite (F i)) : IsPositiveDefinite fun (x : M) => ∑ i ∈ s, ↑(w i) * F i x

Finite nonnegative real-weighted sums, written with the real weight coerced to ℂ and multiplied in the codomain.

theorem TauCeti.IsPositiveDefinite.pow {M : Type u_1} [AddMonoid M] [StarAddMonoid M] {F : M → ℂ} (hF : IsPositiveDefinite F) (n : ℕ) : IsPositiveDefinite fun (x : M) => F x ^ n

Schur powers of a positive-definite function are positive definite.

theorem TauCeti.IsPositiveDefinite.sum_smul_apply_of_apply_eq_one {N : Type u_2} {ι : Type u_3} {s : Finset ι} {w : ι → ℂ} {F : ι → N → ℂ} {x : N} (hFx : ∀ i ∈ s, F i x = 1) : ∑ i ∈ s, w i • F i x = ∑ i ∈ s, w i

If each summand in a finite complex-weighted sum is normalized at a point, then the sum's value at that point is the sum of the weights.

theorem TauCeti.IsPositiveDefinite.sum_smul_apply_eq_one {N : Type u_2} {ι : Type u_3} {s : Finset ι} {w : ι → ℂ} {F : ι → N → ℂ} {x : N} (hFx : ∀ i ∈ s, F i x = 1) (hw_sum : ∑ i ∈ s, w i = 1) : (fun (y : N) => ∑ i ∈ s, w i • F i y) x = 1

A finite complex-weighted sum of functions normalized at a point is normalized at that point when the weights sum to 1.

theorem TauCeti.IsPositiveDefinite.sum_const_mul_apply_of_apply_eq_one {N : Type u_2} {ι : Type u_3} {s : Finset ι} {w : ι → ℂ} {F : ι → N → ℂ} {x : N} (hFx : ∀ i ∈ s, F i x = 1) : ∑ i ∈ s, w i * F i x = ∑ i ∈ s, w i

If each summand in a finite complex-weighted sum is normalized at a point, then the sum's multiplication-form value at that point is the sum of the weights.

theorem TauCeti.IsPositiveDefinite.sum_const_mul_apply_eq_one {N : Type u_2} {ι : Type u_3} {s : Finset ι} {w : ι → ℂ} {F : ι → N → ℂ} {x : N} (hFx : ∀ i ∈ s, F i x = 1) (hw_sum : ∑ i ∈ s, w i = 1) : (fun (y : N) => ∑ i ∈ s, w i * F i y) x = 1

A finite complex-weighted sum, in multiplication form, of functions normalized at a point is normalized at that point when the weights sum to 1.

theorem TauCeti.IsPositiveDefinite.sum_real_smul_apply_of_apply_eq_one {N : Type u_2} {ι : Type u_3} {s : Finset ι} {w : ι → ℝ} {F : ι → N → ℂ} {x : N} (hFx : ∀ i ∈ s, F i x = 1) : ∑ i ∈ s, w i • F i x = ↑(∑ i ∈ s, w i)

If each summand in a finite real-weighted sum is normalized at a point, then the sum's value at that point is the complex coercion of the sum of the real weights.

theorem TauCeti.IsPositiveDefinite.sum_real_smul_apply_eq_one {N : Type u_2} {ι : Type u_3} {s : Finset ι} {w : ι → ℝ} {F : ι → N → ℂ} {x : N} (hFx : ∀ i ∈ s, F i x = 1) (hw_sum : ∑ i ∈ s, w i = 1) : (fun (y : N) => ∑ i ∈ s, w i • F i y) x = 1

A finite real-weighted sum of functions normalized at a point is normalized at that point when the weights sum to 1.

theorem TauCeti.IsPositiveDefinite.sum_real_const_mul_apply_of_apply_eq_one {N : Type u_2} {ι : Type u_3} {s : Finset ι} {w : ι → ℝ} {F : ι → N → ℂ} {x : N} (hFx : ∀ i ∈ s, F i x = 1) : ∑ i ∈ s, ↑(w i) * F i x = ↑(∑ i ∈ s, w i)

If each summand in a finite real-weighted sum is normalized at a point, then the sum's multiplication-form value at that point is the complex coercion of the sum of the real weights.

theorem TauCeti.IsPositiveDefinite.sum_real_const_mul_apply_eq_one {N : Type u_2} {ι : Type u_3} {s : Finset ι} {w : ι → ℝ} {F : ι → N → ℂ} {x : N} (hFx : ∀ i ∈ s, F i x = 1) (hw_sum : ∑ i ∈ s, w i = 1) : (fun (y : N) => ∑ i ∈ s, ↑(w i) * F i y) x = 1

A finite real-weighted sum, in multiplication form, of functions normalized at a point is normalized at that point when the weights sum to 1.

theorem TauCeti.IsPositiveDefinite.sum_smul_apply_zero_of_apply_zero_eq_one {N : Type u_2} [Zero N] {ι : Type u_3} {s : Finset ι} {w : ι → ℂ} {F : ι → N → ℂ} (hF0 : ∀ i ∈ s, F i 0 = 1) : ∑ i ∈ s, w i • F i 0 = ∑ i ∈ s, w i

If each summand in a finite complex-weighted sum is normalized at the origin, then the sum's value at the origin is the sum of the weights.

theorem TauCeti.IsPositiveDefinite.sum_smul_apply_zero_eq_one {N : Type u_2} [Zero N] {ι : Type u_3} {s : Finset ι} {w : ι → ℂ} {F : ι → N → ℂ} (hF0 : ∀ i ∈ s, F i 0 = 1) (hw_sum : ∑ i ∈ s, w i = 1) : (fun (x : N) => ∑ i ∈ s, w i • F i x) 0 = 1

A finite complex-weighted sum of functions normalized at the origin is normalized when the weights sum to 1.

theorem TauCeti.IsPositiveDefinite.sum_const_mul_apply_zero_of_apply_zero_eq_one {N : Type u_2} [Zero N] {ι : Type u_3} {s : Finset ι} {w : ι → ℂ} {F : ι → N → ℂ} (hF0 : ∀ i ∈ s, F i 0 = 1) : ∑ i ∈ s, w i * F i 0 = ∑ i ∈ s, w i

If each summand in a finite complex-weighted sum is normalized at the origin, then the sum's multiplication-form value at the origin is the sum of the weights.

theorem TauCeti.IsPositiveDefinite.sum_const_mul_apply_zero_eq_one {N : Type u_2} [Zero N] {ι : Type u_3} {s : Finset ι} {w : ι → ℂ} {F : ι → N → ℂ} (hF0 : ∀ i ∈ s, F i 0 = 1) (hw_sum : ∑ i ∈ s, w i = 1) : (fun (x : N) => ∑ i ∈ s, w i * F i x) 0 = 1

A finite complex-weighted sum, in multiplication form, of functions normalized at the origin is normalized when the weights sum to 1.

theorem TauCeti.IsPositiveDefinite.sum_real_smul_apply_zero_of_apply_zero_eq_one {N : Type u_2} [Zero N] {ι : Type u_3} {s : Finset ι} {w : ι → ℝ} {F : ι → N → ℂ} (hF0 : ∀ i ∈ s, F i 0 = 1) : ∑ i ∈ s, w i • F i 0 = ↑(∑ i ∈ s, w i)

If each summand in a finite real-weighted sum is normalized at the origin, then the sum's value at the origin is the complex coercion of the sum of the real weights.

theorem TauCeti.IsPositiveDefinite.sum_real_smul_apply_zero_eq_one {N : Type u_2} [Zero N] {ι : Type u_3} {s : Finset ι} {w : ι → ℝ} {F : ι → N → ℂ} (hF0 : ∀ i ∈ s, F i 0 = 1) (hw_sum : ∑ i ∈ s, w i = 1) : (fun (x : N) => ∑ i ∈ s, w i • F i x) 0 = 1

A finite real-weighted sum of functions normalized at the origin is normalized when the weights sum to 1.

theorem TauCeti.IsPositiveDefinite.sum_real_const_mul_apply_zero_of_apply_zero_eq_one {N : Type u_2} [Zero N] {ι : Type u_3} {s : Finset ι} {w : ι → ℝ} {F : ι → N → ℂ} (hF0 : ∀ i ∈ s, F i 0 = 1) : ∑ i ∈ s, ↑(w i) * F i 0 = ↑(∑ i ∈ s, w i)

If each summand in a finite real-weighted sum is normalized at the origin, then the sum's multiplication-form value at the origin is the complex coercion of the sum of the real weights.

theorem TauCeti.IsPositiveDefinite.sum_real_const_mul_apply_zero_eq_one {N : Type u_2} [Zero N] {ι : Type u_3} {s : Finset ι} {w : ι → ℝ} {F : ι → N → ℂ} (hF0 : ∀ i ∈ s, F i 0 = 1) (hw_sum : ∑ i ∈ s, w i = 1) : (fun (x : N) => ∑ i ∈ s, ↑(w i) * F i x) 0 = 1

A finite real-weighted sum, in multiplication form, of functions normalized at the origin is normalized when the weights sum to 1.