Actual integration of uniformly L²-bounded parameter families. The result is proved directly on raw jointly measurable representatives, without assuming a pre-existing Bochner path in the L² space.
theorem
EulerLpParameterIntegral.integral_norm_sq_eq
{α : Type u_1}
{E : Type u_3}
[MeasurableSpace α]
[NormedAddCommGroup E]
(μ : MeasureTheory.Measure α)
(f : α → E)
(hf : MeasureTheory.MemLp f 2 μ)
:
theorem
EulerLpParameterIntegral.norm_integral_sq_le
{α : Type u_1}
{E : Type u_3}
[MeasurableSpace α]
[NormedAddCommGroup E]
[NormedSpace ℝ E]
(ν : MeasureTheory.Measure α)
[MeasureTheory.IsFiniteMeasure ν]
(f : α → E)
(hf : MeasureTheory.MemLp f 2 ν)
:
Bochner Cauchy--Schwarz against the constant function one.
theorem
EulerLpParameterIntegral.integral_memLp_and_bound
{α : Type u_1}
{β : Type u_2}
{E : Type u_3}
[MeasurableSpace α]
[MeasurableSpace β]
[NormedAddCommGroup E]
[NormedSpace ℝ E]
(ν : MeasureTheory.Measure α)
[MeasureTheory.IsFiniteMeasure ν]
(μ : MeasureTheory.Measure β)
[MeasureTheory.SFinite μ]
(f : α × β → E)
(hf : MeasureTheory.AEStronglyMeasurable f (ν.prod μ))
(C : ℝ)
(hC : 0 ≤ C)
(hbound :
∀ᵐ (s : α) ∂ν, MeasureTheory.MemLp (fun (x : β) => f (s, x)) 2 μ ∧ (MeasureTheory.eLpNorm (fun (x : β) => f (s, x)) 2 μ).toReal ≤ C)
:
The integral of a raw family with uniform L² bound C has L² bound
measure(parameter space) * C. This applies to time integration on a
finite interval and to periodic parameter averaging.
theorem
EulerLpParameterIntegral.intervalIntegral_memLp_and_bound
{β : Type u_2}
{E : Type u_3}
[MeasurableSpace β]
[NormedAddCommGroup E]
[NormedSpace ℝ E]
(T : ℝ)
(hT : 0 ≤ T)
(μ : MeasureTheory.Measure β)
[MeasureTheory.SFinite μ]
(f : ℝ × β → E)
(hf : MeasureTheory.AEStronglyMeasurable f ((MeasureTheory.volume.restrict (Set.Icc 0 T)).prod μ))
(C : ℝ)
(hC : 0 ≤ C)
(hbound :
∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict (Set.Icc 0 T), MeasureTheory.MemLp (fun (x : β) => f (s, x)) 2 μ ∧ (MeasureTheory.eLpNorm (fun (x : β) => f (s, x)) 2 μ).toReal ≤ C)
: