Vanishing moments force a function to be zero

Roadmap milestone B1 of the OrthogonalL2Bases roadmap, in both the forms the completeness step uses. TauCeti.Probability.Moments.Determinacy pins down a measure from its moments; this file transfers that to functions.

Both forms assume exponential control at a single positive rate; they differ in what carries it.

• TauCeti.ae_eq_zero_of_forall_moment_eq_zero (function level) assumes the product e^{a|x|} · g is integrable for some a > 0, and concludes for a real g.
• TauCeti.ae_eq_zero_of_forall_moment_eq_zero_of_exists_integrable_exp (measure level) assumes it of the weight alone -- e^{a|x|} ∈ L¹(ν) for some a > 0 -- and of g only that it lies in L²(ν), for scalars in any RCLike field. Cauchy-Schwarz bridges the two. The roadmap name ae_eq_zero_of_forall_moment_eq_zero_of_finite_expMoments, taking the stronger all-rates hypothesis its name implies, is provided as a public wrapper.

The measure-level form is the usable one: hexp becomes a statement about the weight alone (Gaussian decay, or automatic for a finite compactly supported measure), independent of g. Compact support alone does not suffice: on a compactly supported measure of infinite mass even the constant 1 fails to be integrable. In the measure-level form finiteness of ν is not a separate hypothesis: there hexp integrates the weight e^{a|x|} ≥ 1 itself, which dominates the constant 1. The function-level form carries no such implication -- its hexp integrates the product e^{a|x|} · g, which g = 0 satisfies over any measure, finite or infinite.

The same exponential-moment hypothesis also makes every polynomial moment finite, so the result that records this -- TauCeti.integrable_pow_of_exp_moment, a symmetric-moment adaptation of ProbabilityTheory.integrable_pow_of_integrable_exp_mul -- lives here with it rather than with any one consumer.

Exponential moments control polynomial moments

theorem TauCeti.integrable_pow_of_exp_moment {ν : MeasureTheory.Measure ℝ} (hexp : ∃ (a : ℝ), 0 < a ∧ MeasureTheory.Integrable (fun (x : ℝ) => Real.exp (a * |x|)) ν) (k : ℕ) : MeasureTheory.Integrable (fun (x : ℝ) => x ^ k) ν

One finite exponential moment makes every polynomial moment finite.

The two-sided moment hypothesis of ProbabilityTheory.integrable_pow_of_integrable_exp_mul is what a single symmetric moment e^{a|x|} ∈ L¹(ν) supplies: ±x ≤ |x| makes e^{a|x|} dominate both e^{ax} and e^{-ax}.

This is the bridge to the family-agnostic polynomial interface of TauCeti.MeasureTheory.Function.PolynomialMemLp, whose hypothesis is exactly "every polynomial moment is finite"; the MemLp statements of TauCeti.Analysis.InnerProductSpace.PolynomialCompleteness are that interface applied through this.

Vanishing moments at the level of functions

theorem TauCeti.ae_eq_zero_of_forall_moment_eq_zero {ν : MeasureTheory.Measure ℝ} (g : ℝ → ℝ) (hexp : ∃ (a : ℝ), 0 < a ∧ MeasureTheory.Integrable (fun (x : ℝ) => Real.exp (a * |x|) * g x) ν) (hmom : ∀ (n : ℕ), ∫ (x : ℝ), x ^ n * g x ∂ν = 0) : g =ᵐ[ν] 0

Roadmap B1 (function level). A real function on ℝ whose exponentially-weighted product e^{a|x|} · g is integrable for some a > 0, and all of whose polynomial moments ∫ xⁿ g vanish, is a.e. zero.

This is the internal transfer step, not the form the completeness step consumes — that is the measure-level ae_eq_zero_of_forall_moment_eq_zero_of_exists_integrable_exp below, which wraps this one. Measure.ext_of_forall_integral_pow_eq_of_exists_integrable_exp in TauCeti.Probability.Moments.Determinacy pins down a measure from its moments, and this transfers that to a function by applying it to the positive and negative parts of g as densities against ν.

The exponential hypothesis is the existential ∃ a > 0, matching the engine's convention; a caller holding a bound at every rate supplies it at any single one.

The reference measure is arbitrary, not just volume, and carries no σ-finiteness hypothesis: the argument splits g into g⁺/g⁻ as densities, and integrability of g already bounds the positive density's lintegral, which is what lets equality of the two withDensity measures be read back as equality of the densities. That generality is what lets weighted orthogonal families against a measure other than Lebesgue (Hermite against a Gaussian, Chebyshev against (1-x²)^{-1/2} on [-1,1]) reach the completeness step, through the measure-level form below.

Vanishing moments at the level of measures

theorem TauCeti.ae_eq_zero_of_forall_moment_eq_zero_of_exists_integrable_exp {ν : MeasureTheory.Measure ℝ} {𝕜 : Type u_1} [RCLike 𝕜] (hexp : ∃ (a : ℝ), 0 < a ∧ MeasureTheory.Integrable (fun (x : ℝ) => Real.exp (a * |x|)) ν) {g : ℝ → 𝕜} (hg : MeasureTheory.MemLp g 2 ν) (hmom : ∀ (n : ℕ), ∫ (x : ℝ), (algebraMap ℝ 𝕜) x ^ n * g x ∂ν = 0) : g =ᵐ[ν] 0

Roadmap B1, measure level. A measure ν on ℝ carrying one finite exponential moment is moment-determinate, so a g ∈ L²(ν) orthogonal to every monomial is a.e. 0.

The rate is existential, matching the convention of the engine this wraps and of the function-level form above; a caller holding a bound at every rate supplies it at any single one. Requiring it at every rate would exclude exponentially-tailed weights such as e^{-|x|}, for which ∫ e^{a|x|} dν is finite only for a < 1, even though they are moment-determinate all the same. The _of_exists_integrable_exp suffix names the hypothesis exactly — existence of one positive rate with e^{a|x|} integrable — and matches the adjacent determinacy API (Measure.ext_of_forall_integral_pow_eq_of_exists_integrable_exp). The roadmap name _of_finite_expMoments, with the matching all-rates hypothesis, wraps this one immediately below.

Finiteness of ν is not a separate hypothesis: e^{a|x|} ≥ 1.

theorem TauCeti.ae_eq_zero_of_forall_moment_eq_zero_of_finite_expMoments {ν : MeasureTheory.Measure ℝ} {𝕜 : Type u_1} [RCLike 𝕜] (hexp : ∀ (a : ℝ), 0 ≤ a → MeasureTheory.Integrable (fun (x : ℝ) => Real.exp (a * |x|)) ν) {g : ℝ → 𝕜} (hg : MeasureTheory.MemLp g 2 ν) (hmom : ∀ (n : ℕ), ∫ (x : ℝ), (algebraMap ℝ 𝕜) x ^ n * g x ∂ν = 0) : g =ᵐ[ν] 0

Roadmap B1, measure level (roadmap-specified API name). The name _of_finite_expMoments is accurate here: the hypothesis is that every exponential moment is finite -- e^{a|x|} is integrable at every rate a ≥ 0 -- which is the roadmap signature. This is strictly stronger than the primary _of_exists_integrable_exp, and follows from it immediately by using the moment at any single positive rate.