L² Bounds for Time Integrals

This file proves L² bounds on time averages and parametric integrals.

Main Results

1. sq_setIntegral_le_measure_mul_setIntegral_sq_proved - Cauchy-Schwarz for set integrals (Hölder)
2. L2_time_average_bound - L² bound for time averages (Cauchy-Schwarz + Fubini)
3. time_average_memLp_two - Time average is in L² (corollary of 2)
4. memLp_prod_of_uniform_slicewise_bound - L² on product from uniform slicewise bounds
5. gff_time_integral_aestronglyMeasurable_proved - Parametric time integral is measurable
6. gff_covariance_norm_integrableOn_slice_proved - Covariance norm integrable on slices
7. double_integral_polynomial_decay_bound_proved - Double integral bound for polynomial decay kernels
8. minkowski_weighted_L2_sum_proved - Minkowski inequality for weighted L² sums

Mathematical Background

The key tools are:

• Cauchy-Schwarz: ‖∫ f‖² ≤ (b-a) · ∫ ‖f‖²
• Fubini-Tonelli: swap order of integration
• L² is a Hilbert space: Minkowski inequality

References

• Billingsley "Probability and Measure", Ch. 7
• Folland "Real Analysis", Thm. 2.37 (Fubini-Tonelli)

L² Bound for Time Averages

The main result: if A : ℝ → Ω → ℂ has uniform L² bound over [0,T], then the time average (1/T)∫₀ᵀ A_s ds is in L² with the same bound.

Proof outline:

1. Cauchy-Schwarz pointwise: ‖∫₀ᵀ A_s(ω) ds‖² ≤ T · ∫₀ᵀ ‖A_s(ω)‖² ds
2. Scale by (1/T)²: ‖(1/T)∫...‖² ≤ (1/T) · ∫₀ᵀ ‖A_s(ω)‖² ds
3. Integrate over Ω: ∫_Ω ‖(1/T)∫...‖² dμ ≤ (1/T) · ∫_Ω ∫₀ᵀ ‖A_s‖² ds dμ
4. Fubini: = (1/T) · ∫₀ᵀ (∫_Ω ‖A_s‖² dμ) ds
5. Uniform bound: ≤ (1/T) · ∫₀ᵀ M_sq ds = (1/T) · T · M_sq = M_sq

Cauchy-Schwarz for Set Integrals

The L² Cauchy-Schwarz inequality |⟨1, f⟩|² ≤ ‖1‖² · ‖f‖² applied to integrals: ‖∫[a,b] f‖² ≤ (b-a) · ∫[a,b] ‖f‖²

Proof uses Hölder's inequality with p = q = 2, taking one function to be constant 1.

theorem OSforGFF.sq_setIntegral_le_measure_mul_setIntegral_sq_proved {f : ℝ → ℂ} {a b : ℝ} (hab : a ≤ b) (hf_sq : MeasureTheory.IntegrableOn (fun (x : ℝ) => ‖f x‖ ^ 2) (Set.Icc a b) MeasureTheory.volume) : ‖∫ (x : ℝ) in Set.Icc a b, f x‖ ^ 2 ≤ (b - a) * ∫ (x : ℝ) in Set.Icc a b, ‖f x‖ ^ 2

Cauchy-Schwarz for set integrals.

For f : ℝ → ℂ with ‖f‖² integrable on [a,b]: ‖∫[a,b] f(x) dx‖² ≤ (b-a) · ∫[a,b] ‖f(x)‖² dx

This is |⟨1, f⟩|² ≤ ‖1‖² · ‖f‖² in L².

theorem OSforGFF.cauchy_schwarz_time_integral_pointwise {Ω : Type u_1} (A : ℝ → Ω → ℂ) (T : ℝ) (hT : T > 0) (ω : Ω) (hf_sq : MeasureTheory.IntegrableOn (fun (s : ℝ) => ‖A s ω‖ ^ 2) (Set.Icc 0 T) MeasureTheory.volume) : ‖∫ (s : ℝ) in Set.Icc 0 T, A s ω‖ ^ 2 ≤ T * ∫ (s : ℝ) in Set.Icc 0 T, ‖A s ω‖ ^ 2

Cauchy-Schwarz for the time integral, pointwise in ω.

theorem OSforGFF.scaled_time_average_pointwise_bound {Ω : Type u_1} (A : ℝ → Ω → ℂ) (T : ℝ) (hT : T > 0) (ω : Ω) (hf_sq : MeasureTheory.IntegrableOn (fun (s : ℝ) => ‖A s ω‖ ^ 2) (Set.Icc 0 T) MeasureTheory.volume) : ‖1 / ↑T * ∫ (s : ℝ) in Set.Icc 0 T, A s ω‖ ^ 2 ≤ 1 / T * ∫ (s : ℝ) in Set.Icc 0 T, ‖A s ω‖ ^ 2

The scaled time average satisfies a pointwise L² bound.

Main Theorem: L² Time Average Bound

We now prove the main theorem by integrating the pointwise bound over Ω and swapping the order of integration via Fubini.

theorem OSforGFF.integral_swap_Icc {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) [MeasureTheory.SFinite μ] (f : ℝ × Ω → ℝ) (T : ℝ) (hf : MeasureTheory.Integrable f ((MeasureTheory.volume.restrict (Set.Icc 0 T)).prod μ)) : ∫ (ω : Ω), ∫ (s : ℝ) in Set.Icc 0 T, f (s, ω) ∂μ = ∫ (s : ℝ) in Set.Icc 0 T, ∫ (ω : Ω), f (s, ω) ∂μ

Helper: Fubini swap for ℝ × Ω with restricted measure.

theorem OSforGFF.setIntegral_L2_bound {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) [MeasureTheory.SFinite μ] (M_sq T : ℝ) (hT : T > 0) (A : ℝ → Ω → ℂ) (h_L2_bound : ∀ s ∈ Set.Icc 0 T, ∫ (ω : Ω), ‖A s ω‖ ^ 2 ∂μ ≤ M_sq) (h_int : MeasureTheory.IntegrableOn (fun (s : ℝ) => ∫ (ω : Ω), ‖A s ω‖ ^ 2 ∂μ) (Set.Icc 0 T) MeasureTheory.volume) : ∫ (s : ℝ) in Set.Icc 0 T, ∫ (ω : Ω), ‖A s ω‖ ^ 2 ∂μ ≤ T * M_sq

Helper: setIntegral bound using uniform L² bound.

theorem OSforGFF.L2_time_average_bound {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) [MeasureTheory.SFinite μ] (A : ℝ → Ω → ℂ) (M_sq T : ℝ) (hT : T > 0) (h_L2_bound : ∀ s ∈ Set.Icc 0 T, ∫ (ω : Ω), ‖A s ω‖ ^ 2 ∂μ ≤ M_sq) (h_joint_meas : MeasureTheory.AEStronglyMeasurable (Function.uncurry A) ((MeasureTheory.volume.restrict (Set.Icc 0 T)).prod μ)) (h_prod_int : MeasureTheory.Integrable (fun (p : ℝ × Ω) => ‖A p.1 p.2‖ ^ 2) ((MeasureTheory.volume.restrict (Set.Icc 0 T)).prod μ)) (h_slice_int : MeasureTheory.IntegrableOn (fun (s : ℝ) => ∫ (ω : Ω), ‖A s ω‖ ^ 2 ∂μ) (Set.Icc 0 T) MeasureTheory.volume) (h_avg_meas : MeasureTheory.AEStronglyMeasurable (fun (ω : Ω) => 1 / ↑T * ∫ (s : ℝ) in Set.Icc 0 T, A s ω) μ) : ∫ (ω : Ω), ‖1 / ↑T * ∫ (s : ℝ) in Set.Icc 0 T, A s ω‖ ^ 2 ∂μ ≤ M_sq

L² bound for time averages.

For A : ℝ → Ω → ℂ with uniform L² bound ∫Ω ‖A_s‖² dμ ≤ M_sq for all s ∈ [0,T], the time average satisfies: $$\int\Omega \left|\frac{1}{T}\int_0^T A_s(\omega),ds\right|^2 d\mu(\omega) \leq M_{sq}$$

Proof outline:

1. Cauchy-Schwarz pointwise: ‖(1/T)∫ A_s(ω) ds‖² ≤ (1/T) ∫ ‖A_s(ω)‖² ds
2. Integrate over Ω: ∫_Ω LHS dμ ≤ (1/T) ∫Ω ∫[0,T] ‖A_s‖² ds dμ
3. Fubini: = (1/T) ∫_[0,T] (∫_Ω ‖A_s‖² dμ) ds
4. Uniform bound: ≤ (1/T) ∫_[0,T] M_sq ds = (1/T) · T · M_sq = M_sq

L² on Product from Slicewise Bounds (Theorem 3 - prove first)

Tonelli's theorem: if each slice is in L² with uniform bound, then the function is in L² on the product.

Key insight: Use integrable_prod_iff (Tonelli) to split product integrability into:

1. Slice integrability (from each A_s ∈ L²)
2. Integrability of slice integrals (constant by uniform bound → trivially integrable on [0,T])

theorem OSforGFF.memLp_prod_of_uniform_slicewise_bound {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) [MeasureTheory.SFinite μ] (A : ℝ → Ω → ℂ) (T : ℝ) (h_meas : MeasureTheory.AEStronglyMeasurable (Function.uncurry A) ((MeasureTheory.volume.restrict (Set.Icc 0 T)).prod μ)) (h_memLp : ∀ (s : ℝ), MeasureTheory.MemLp (A s) 2 μ) (h_uniform : ∀ (s : ℝ), ∫ (ω : Ω), ‖A s ω‖ ^ 2 ∂μ = ∫ (ω : Ω), ‖A 0 ω‖ ^ 2 ∂μ) : MeasureTheory.MemLp (Function.uncurry A) 2 ((MeasureTheory.volume.restrict (Set.Icc 0 T)).prod μ)

L² on product from uniform slicewise bounds.

By Tonelli: ∫∫ |A|² = ∫₀ᵀ (∫_Ω |A_s|² dμ) ds = ∫₀ᵀ C ds = TC

Time Average is in L² (Theorem 2)

This is a corollary using Theorem 3 + Integrable.mono.

theorem OSforGFF.time_average_memLp_two {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) [MeasureTheory.SFinite μ] (A : ℝ → Ω → ℂ) (T : ℝ) (hT : T > 0) (h_memLp : ∀ (s : ℝ), MeasureTheory.MemLp (A s) 2 μ) (h_uniform : ∀ (s : ℝ), ∫ (ω : Ω), ‖A s ω‖ ^ 2 ∂μ = ∫ (ω : Ω), ‖A 0 ω‖ ^ 2 ∂μ) (h_joint_meas : MeasureTheory.AEStronglyMeasurable (Function.uncurry A) ((MeasureTheory.volume.restrict (Set.Icc 0 T)).prod μ)) (h_avg_meas : MeasureTheory.AEStronglyMeasurable (fun (ω : Ω) => 1 / ↑T * ∫ (s : ℝ) in Set.Icc 0 T, A s ω) μ) : MeasureTheory.MemLp (fun (ω : Ω) => 1 / ↑T * ∫ (s : ℝ) in Set.Icc 0 T, A s ω) 2 μ

Time average is in L² (Corollary of memLp_prod)

This follows from product integrability + Integrable.mono with the pointwise bound.

Measurability of Parametric Time Integrals

For a family A : ℝ → Ω → ℂ that is continuous in s and measurable in ω, the parametric integral ω ↦ ∫ A s ω ds is AEStronglyMeasurable.

Key tool: stronglyMeasurable_uncurry_of_continuous_of_stronglyMeasurable gives joint StronglyMeasurable on ℝ × Ω from continuous-in-s + measurable-in-ω. Then swap + integral_prod_right' gives measurability of the marginal integral.

theorem OSforGFF.gff_time_integral_aestronglyMeasurable_proved {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] (A : ℝ → Ω → ℂ) (EA : ℂ) (T : ℝ) (h_cont_s : ∀ (ω : Ω), Continuous fun (s : ℝ) => A s ω) (h_meas : ∀ (s : ℝ), Measurable (A s)) : MeasureTheory.AEStronglyMeasurable (fun (ω : Ω) => 1 / ↑T * ∫ (s : ℝ) in Set.Icc 0 T, A s ω - EA) μ

Measurability of parametric time integrals.

For A : ℝ → Ω → ℂ with s ↦ A s ω continuous for each ω and A s measurable for each s, the time integral ω ↦ (1/T) * ∫ₛ (A s ω - EA) ds is AEStronglyMeasurable.

Proof: continuous-in-s + measurable-in-ω → jointly StronglyMeasurable (Mathlib), then swap product measure and integrate out s via integral_prod_right'.

Integrability of Covariance Norm on Slices

For a continuous covariance function, the norm restricted to any compact slice is integrable. This is immediate from continuity on compact sets.

theorem OSforGFF.gff_covariance_norm_integrableOn_slice_proved {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] (A : ℝ → Ω → ℂ) (EA : ℂ) (s T : ℝ) (h_cov_cont : Continuous fun (p : ℝ × ℝ) => ∫ (ω : Ω), A p.1 ω * (starRingEnd ℂ) (A p.2 ω) ∂μ - EA * (starRingEnd ℂ) EA) : MeasureTheory.IntegrableOn (fun (u : ℝ) => ‖∫ (ω : Ω), A s ω * (starRingEnd ℂ) (A u ω) ∂μ - EA * (starRingEnd ℂ) EA‖) (Set.Icc 0 T) MeasureTheory.volume

Integrability of covariance norm on slices.

If the covariance (s,u) ↦ ∫ A_s · conj(A_u) - EA·conj(EA) is continuous, then u ↦ ‖Cov(s,u)‖ is integrable on [0,T] since continuous functions on compact sets are integrable.

Double Integral Bound for Polynomial Decay Kernels

For kernels K(s,u) = (1 + |s-u|)^{-α} with α > 1, the double integral over [0,T]² is bounded linearly in T. The proof uses:

1. Integrability on ℝ: (1+|t|)^{-α} is integrable via integrableOn_add_rpow_Ioi_of_lt on Ioi 0, transferred to Iio 0 by negation symmetry (g is even, Lebesgue measure is negation-invariant via MeasurePreserving.integrableOn_comp_preimage).
2. Translation invariance: For each s, ∫_{[0,T]} g(s-u) du ≤ ∫_ℝ g = C by setIntegral_le_integral and integral_sub_left_eq_self.
3. Outer integral: ∫_{[0,T]} C ds = C·T.

theorem OSforGFF.double_integral_polynomial_decay_bound_proved (α : ℝ) (hα : α > 1) : ∃ C > 0, ∀ T > 0, ∫ (s : ℝ) (u : ℝ) in Set.Icc 0 T, (1 + |s - u|) ^ (-α) ≤ C * T

Double integral bound for polynomial decay kernels.

For the kernel K(s,u) = (1 + |s-u|)^{-α} with α > 1: ∫₀ᵀ ∫₀ᵀ (1 + |s-u|)^{-α} ds du ≤ C · T

where C = ∫_ℝ (1+|t|)^{-α} dt is the integral of the kernel over all of ℝ.

Key tools: integrableOn_add_rpow_Ioi_of_lt (decay integral), integral_sub_left_eq_self (translation invariance), setIntegral_le_integral (set ≤ full for nonneg integrable functions), MeasurePreserving.integrableOn_comp_preimage (negation symmetry for even functions).

Minkowski Inequality for Weighted L² Sums

The triangle inequality in L²: √(∫(∑ wⱼfⱼ)²) ≤ ∑ wⱼ√(∫ fⱼ²) for nonneg weights and functions. Proved by induction using Cauchy-Schwarz.

theorem OSforGFF.minkowski_weighted_L2_sum_proved {α : Type u_2} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {n : ℕ} {w : Fin n → ℝ} {f : Fin n → α → ℝ} (hw : ∀ (j : Fin n), 0 ≤ w j) (hf : ∀ (j : Fin n) (ω : α), 0 ≤ f j ω) (hf_int : ∀ (j : Fin n), MeasureTheory.Integrable (fun (ω : α) => f j ω ^ 2) μ) (hf_meas : ∀ (j : Fin n), MeasureTheory.AEStronglyMeasurable (f j) μ) : √(∫ (ω : α), (∑ j : Fin n, w j * f j ω) ^ 2 ∂μ) ≤ ∑ j : Fin n, w j * √(∫ (ω : α), f j ω ^ 2 ∂μ)

Minkowski inequality for weighted L² sums (proved theorem)

For nonneg weights wⱼ and nonneg functions fⱼ with fⱼ² integrable: √(∫ (∑ⱼ wⱼfⱼ)² dμ) ≤ ∑ⱼ wⱼ √(∫ fⱼ² dμ)

Proof by induction on n, using Cauchy-Schwarz for integrals at each step.

Variance Bound for Time Averages

The variance of the time average is bounded by the double integral of the covariance: ‖E[‖T⁻¹∫₀ᵀ A_s ds - EA‖²]‖ ≤ T⁻² · ‖∫₀ᵀ∫₀ᵀ Cov(s,u) ds du‖

The proof establishes an equality (the bound is tight):

1. Center: X_s = A_s - EA, which has zero mean
2. Algebra: T⁻¹ * ∫A_s - EA = T⁻¹ * ∫X_s, factor out T⁻²
3. Cast to ℂ: ‖z‖² = Re(z * conj(z)) [RCLike.mul_conj]
4. Product of integrals = double integral [integral_mul_left/right]
5. Fubini swap ω ↔ (s,u) [integral_integral_swap]
6. Recognize E[X_s · conj(X_u)] = Cov(s,u)
7. Re(z) ≤ ‖z‖ for the final inequality [Complex.re_le_norm]

theorem OSforGFF.L2_variance_time_average_bound {Ω : Type u_2} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] (A : ℝ → Ω → ℂ) (EA : ℂ) (T : ℝ) (hT : T > 0) (h_mean : ∀ (s : ℝ), ∫ (ω : Ω), A s ω ∂μ = EA) (h_Fubini : MeasureTheory.Integrable (fun (x : Ω × ℝ × ℝ) => (A x.2.1 x.1 - EA) * (starRingEnd ℂ) (A x.2.2 x.1 - EA)) (μ.prod ((MeasureTheory.volume.restrict (Set.Icc 0 T)).prod (MeasureTheory.volume.restrict (Set.Icc 0 T))))) (h_slice_L2 : ∀ (s : ℝ), MeasureTheory.MemLp (A s) 2 μ) (h_slice_int : ∀ᵐ (ω : Ω) ∂μ, MeasureTheory.Integrable (fun (s : ℝ) => A s ω) (MeasureTheory.volume.restrict (Set.Icc 0 T))) : have Cov := fun (s u : ℝ) => ∫ (ω : Ω), A s ω * (starRingEnd ℂ) (A u ω) ∂μ - EA * (starRingEnd ℂ) EA; ‖∫ (ω : Ω), ‖((↑T)⁻¹ * ∫ (s : ℝ) in Set.Icc 0 T, A s ω) - EA‖ ^ 2 ∂μ‖ ≤ T⁻¹ ^ 2 * ‖∫ (s : ℝ) (u : ℝ) in Set.Icc 0 T, Cov s u‖

Variance of time averages bounded by double integral of covariance (proved theorem)

For an L² stationary process A with constant mean EA: ‖E[‖T⁻¹∫₀ᵀ A_s ds - EA‖²]‖ ≤ T⁻² · ‖∫₀ᵀ∫₀ᵀ Cov(s,u) ds du‖

The proof actually gives equality (the bound is tight).

Fubini Integrability of L² Process Covariance

Proves that (A_s(ω) - c) · conj(A_u(ω) - c) is integrable on the triple product Ω × [0,T] × [0,T], given that A is jointly L² on [0,T] × Ω, continuous in time, and measurable in ω.

Strategy: bound |f·g| ≤ |f|² + |g|² to decouple the product, then use Tonelli to factor the triple integral into ν(univ) × double integral, which is finite by L².

theorem OSforGFF.L2_process_covariance_fubini_integrable {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] (A : ℝ → Ω → ℂ) (c : ℂ) (T : ℝ) (_hT : T > 0) (h_L2 : MeasureTheory.MemLp (Function.uncurry A) 2 ((MeasureTheory.volume.restrict (Set.Icc 0 T)).prod μ)) (h_cont_s : ∀ (ω : Ω), Continuous fun (s : ℝ) => A s ω) (h_sm_slice : ∀ (s : ℝ), MeasureTheory.StronglyMeasurable fun (ω : Ω) => A s ω) : MeasureTheory.Integrable (fun (x : Ω × ℝ × ℝ) => (A x.2.1 x.1 - c) * (starRingEnd ℂ) (A x.2.2 x.1 - c)) (μ.prod ((MeasureTheory.volume.restrict (Set.Icc 0 T)).prod (MeasureTheory.volume.restrict (Set.Icc 0 T))))