Surjectivity of product L² currying

Product currying is onto when the target is complete. The proof puts finite-measure outer indicators in the range by an explicit product-space representative, then uses density of L² simple functions and closedness of the range of an isometry.

theorem LiebThirring.l2CurryLinearIsometry_surjective {α : Type u_1} {β : Type u_2} {E : Type u_3} [MeasurableSpace α] [MeasurableSpace β] [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E] {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} [MeasureTheory.SFinite ν] [SecondCountableTopology ↥(MeasureTheory.Lp E 2 ν)] : Function.Surjective ⇑l2CurryLinearIsometry

Every iterated L² class is the curry of a product-space L² class.

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

Product L² and iterated L² are canonically complex-linearly isometric.

Equations

• LiebThirring.l2CurryLinearIsometryEquiv = LinearIsometryEquiv.ofSurjective LiebThirring.l2CurryLinearIsometry ⋯

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

The equivalence has the expected nested representative formula.