The product L² currying linear isometry

The unique class characterization supplies both linearity and the Tonelli norm identity. No choices of slice representatives enter the public API.

noncomputable def LiebThirring.l2Curry {α : Type u_1} {β : Type u_2} {E : Type u_3} [MeasurableSpace α] [MeasurableSpace β] [NormedAddCommGroup E] {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} [MeasureTheory.SFinite ν] [SecondCountableTopology ↥(MeasureTheory.Lp E 2 ν)] (f : ↥(MeasureTheory.Lp E 2 (μ.prod ν))) : ↥(MeasureTheory.Lp (↥(MeasureTheory.Lp E 2 ν)) 2 μ)

Currying is the unique outer class with the nested slice formula.

Equations

• LiebThirring.l2Curry f = Exists.choose ⋯

theorem LiebThirring.l2Curry_ae {α : Type u_1} {β : Type u_2} {E : Type u_3} [MeasurableSpace α] [MeasurableSpace β] [NormedAddCommGroup E] {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} [MeasureTheory.SFinite ν] [SecondCountableTopology ↥(MeasureTheory.Lp E 2 ν)] (f : ↥(MeasureTheory.Lp E 2 (μ.prod ν))) : ∀ᵐ (x : α) ∂μ, ∀ᵐ (y : β) ∂ν, ↑↑(↑↑(l2Curry f) x) y = ↑↑f (x, y)

The exact representative characterization of product currying.

theorem LiebThirring.l2Curry_norm {α : Type u_1} {β : Type u_2} {E : Type u_3} [MeasurableSpace α] [MeasurableSpace β] [NormedAddCommGroup E] {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} [MeasureTheory.SFinite ν] [SecondCountableTopology ↥(MeasureTheory.Lp E 2 ν)] (f : ↥(MeasureTheory.Lp E 2 (μ.prod ν))) : ‖l2Curry f‖ = ‖f‖

The iterated L² norm of the curried class is the original L² norm.

theorem LiebThirring.l2Curry_add {α : Type u_1} {β : Type u_2} {E : Type u_3} [MeasurableSpace α] [MeasurableSpace β] [NormedAddCommGroup E] {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} [MeasureTheory.SFinite ν] [SecondCountableTopology ↥(MeasureTheory.Lp E 2 ν)] (f h : ↥(MeasureTheory.Lp E 2 (μ.prod ν))) : l2Curry (f + h) = l2Curry f + l2Curry h

Product currying commutes with addition.

theorem LiebThirring.l2Curry_smul {α : Type u_1} {β : Type u_2} {E : Type u_3} [MeasurableSpace α] [MeasurableSpace β] [NormedAddCommGroup E] {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} [MeasureTheory.SFinite ν] [SecondCountableTopology ↥(MeasureTheory.Lp E 2 ν)] [NormedSpace ℂ E] (a : ℂ) (f : ↥(MeasureTheory.Lp E 2 (μ.prod ν))) : l2Curry (a • f) = a • l2Curry f

Product currying commutes with complex scalar multiplication.

noncomputable def LiebThirring.l2CurryLinearIsometry {α : Type u_1} {β : Type u_2} {E : Type u_3} [MeasurableSpace α] [MeasurableSpace β] [NormedAddCommGroup E] {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} [MeasureTheory.SFinite ν] [SecondCountableTopology ↥(MeasureTheory.Lp E 2 ν)] [NormedSpace ℂ E] : ↥(MeasureTheory.Lp E 2 (μ.prod ν)) →ₗᵢ[ℂ] ↥(MeasureTheory.Lp (↥(MeasureTheory.Lp E 2 ν)) 2 μ)

The generic complex linear isometry from product L² to iterated L².

Equations

• LiebThirring.l2CurryLinearIsometry = { toFun := LiebThirring.l2Curry, map_add' := ⋯, map_smul' := ⋯, norm_map' := ⋯ }