Exponential moments from bounded support

This file records a small bounded-support integrability principle used by the OrthogonalL2Bases roadmap's moment-determinacy route. If a measure is supported where the argument norm is essentially bounded, multiplying an integrable function by any exponential weight exp (a * ‖x‖) preserves integrability. On ℝ, this gives the corresponding exp (a * |x|) form.

The Chebyshev T measure is supported on [-1, 1], so this is the reusable bookkeeping behind the finite exponential moments needed before the Chebyshev Hilbert-basis construction.

theorem MeasureTheory.Integrable.exp_norm_smul_of_ae_norm_le {α : Type u_1} {𝕜 : Type u_2} {β : Type u_3} [NormedAddCommGroup α] [MeasurableSpace α] [OpensMeasurableSpace α] [RCLike 𝕜] [SecondCountableTopologyEither α 𝕜] [NormedAddCommGroup β] [NormedSpace 𝕜 β] {μ : Measure α} {g : α → β} (hg : Integrable g μ) (a R : ℝ) (hR : ∀ᵐ (x : α) ∂μ, ‖x‖ ≤ R) : Integrable (fun (x : α) => ↑(Real.exp (a * ‖x‖)) • g x) μ

Multiplication by exp (a * ‖x‖) preserves integrability on a measure whose support is essentially contained in a closed ball.

theorem MeasureTheory.Integrable.exp_abs_smul_of_ae_abs_le {𝕜 : Type u_2} {β : Type u_3} [RCLike 𝕜] [NormedAddCommGroup β] [NormedSpace 𝕜 β] {μ : Measure ℝ} {g : ℝ → β} (hg : Integrable g μ) (a R : ℝ) (hR : ∀ᵐ (x : ℝ) ∂μ, |x| ≤ R) : Integrable (fun (x : ℝ) => ↑(Real.exp (a * |x|)) • g x) μ

Real-line version of Integrable.exp_norm_smul_of_ae_norm_le, stated with |x|.