A jointly measurable field which represents an actual Bochner L² family belongs to the product L² space, with exactly the same norm. This realizes nested space/angle or time/space estimates without changing any derivative constants.

theorem EulerLpBochnerRealization.norm_sq_eq_integral {α : Type u_1} {E : Type u_3} [MeasurableSpace α] [NormedAddCommGroup E] {μ : MeasureTheory.Measure α} (u : ↥(MeasureTheory.Lp E 2 μ)) : ‖u‖ ^ 2 = ∫ (x : α), ‖↑↑u x‖ ^ 2 ∂μ

theorem EulerLpBochnerRealization.fiber_integral {α : Type u_1} {β : Type u_2} {E : Type u_3} [MeasurableSpace α] [MeasurableSpace β] [NormedAddCommGroup E] {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} (w : ↥(MeasureTheory.Lp (↥(MeasureTheory.Lp E 2 ν)) 2 μ)) (f : α × β → E) (hrep : ∀ᵐ (x : α) ∂μ, ↑↑(↑↑w x) =ᵐ[ν] fun (y : β) => f (x, y)) : (fun (x : α) => ∫ (y : β), ‖f (x, y)‖ ^ 2 ∂ν) =ᵐ[μ] fun (x : α) => ‖↑↑w x‖ ^ 2

theorem EulerLpBochnerRealization.field_memLp {α : Type u_1} {β : Type u_2} {E : Type u_3} [MeasurableSpace α] [MeasurableSpace β] [NormedAddCommGroup E] {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} [MeasureTheory.SFinite ν] (w : ↥(MeasureTheory.Lp (↥(MeasureTheory.Lp E 2 ν)) 2 μ)) (f : α × β → E) (hf : MeasureTheory.AEStronglyMeasurable f (μ.prod ν)) (hrep : ∀ᵐ (x : α) ∂μ, ↑↑(↑↑w x) =ᵐ[ν] fun (y : β) => f (x, y)) : MeasureTheory.MemLp f 2 (μ.prod ν)

noncomputable def EulerLpBochnerRealization.realization {α : Type u_1} {β : Type u_2} {E : Type u_3} [MeasurableSpace α] [MeasurableSpace β] [NormedAddCommGroup E] {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} [MeasureTheory.SFinite ν] (w : ↥(MeasureTheory.Lp (↥(MeasureTheory.Lp E 2 ν)) 2 μ)) (f : α × β → E) (hf : MeasureTheory.AEStronglyMeasurable f (μ.prod ν)) (hrep : ∀ᵐ (x : α) ∂μ, ↑↑(↑↑w x) =ᵐ[ν] fun (y : β) => f (x, y)) : ↥(MeasureTheory.Lp E 2 (μ.prod ν))

The genuine product-space representative of the given nested L² element.

Equations

• EulerLpBochnerRealization.realization w f hf hrep = MeasureTheory.MemLp.toLp f ⋯

theorem EulerLpBochnerRealization.realization_ae {α : Type u_1} {β : Type u_2} {E : Type u_3} [MeasurableSpace α] [MeasurableSpace β] [NormedAddCommGroup E] {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} [MeasureTheory.SFinite ν] (w : ↥(MeasureTheory.Lp (↥(MeasureTheory.Lp E 2 ν)) 2 μ)) (f : α × β → E) (hf : MeasureTheory.AEStronglyMeasurable f (μ.prod ν)) (hrep : ∀ᵐ (x : α) ∂μ, ↑↑(↑↑w x) =ᵐ[ν] fun (y : β) => f (x, y)) : ↑↑(realization w f hf hrep) =ᵐ[μ.prod ν] f

theorem EulerLpBochnerRealization.realization_norm {α : Type u_1} {β : Type u_2} {E : Type u_3} [MeasurableSpace α] [MeasurableSpace β] [NormedAddCommGroup E] {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} [MeasureTheory.SFinite ν] [MeasureTheory.SFinite μ] (w : ↥(MeasureTheory.Lp (↥(MeasureTheory.Lp E 2 ν)) 2 μ)) (f : α × β → E) (hf : MeasureTheory.AEStronglyMeasurable f (μ.prod ν)) (hrep : ∀ᵐ (x : α) ∂μ, ↑↑(↑↑w x) =ᵐ[ν] fun (y : β) => f (x, y)) : ‖realization w f hf hrep‖ = ‖w‖

Fubini preserves the exact L² norm, with no angle or dimension factor.