Tonelli and seminorms for L² currying

Tonelli and seminorm identities for product-space L² currying.

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

L² mass in extended norm form, valid for arbitrary normed targets.

theorem LiebThirring.l2_slice_eLpNorm_eq {α : Type u_1} {β : Type u_2} {E : Type u_3} [MeasurableSpace α] [MeasurableSpace β] [NormedAddCommGroup E] {ν : MeasureTheory.Measure β} (f : α × β → E) (hf : MeasureTheory.StronglyMeasurable f) (x : α) : MeasureTheory.eLpNorm (fun (y : β) => f (x, y)) 2 ν = (∫⁻ (y : β), ‖f (x, y)‖ₑ ^ 2 ∂ν) ^ (1 / 2)

The L² seminorm of a strongly measurable slice is a Tonelli formula.

theorem LiebThirring.measurable_l2_slice_eLpNorm {α : Type u_1} {β : Type u_2} {E : Type u_3} [MeasurableSpace α] [MeasurableSpace β] [NormedAddCommGroup E] {ν : MeasureTheory.Measure β} [MeasureTheory.SFinite ν] (f : α × β → E) (hf : MeasureTheory.StronglyMeasurable f) : Measurable fun (x : α) => MeasureTheory.eLpNorm (fun (y : β) => f (x, y)) 2 ν

Slice seminorms are measurable, even before slices are known to be L².

theorem LiebThirring.memLp_l2_slice_ae {α : Type u_1} {β : Type u_2} {E : Type u_3} [MeasurableSpace α] [MeasurableSpace β] [NormedAddCommGroup E] {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} [MeasureTheory.SFinite ν] (f : α × β → E) (hf : MeasureTheory.StronglyMeasurable f) (hLp : MeasureTheory.MemLp f 2 (μ.prod ν)) : ∀ᵐ (x : α) ∂μ, MeasureTheory.MemLp (fun (y : β) => f (x, y)) 2 ν

A product L² function has L² slices on almost every outer coordinate.