Interchanging finite Hilbert sums and L²

This module gives the canonical complex linear isometric equivalence between L²(X; ⨁₂ i, E i) and ⨁₂ i, L²(X; E i) for a finite family of complete complex Hilbert spaces. Its evaluation theorem records the representative identity in every coordinate.

noncomputable def LiebThirring.finiteLpPiLpForward {X : Type u_1} {ι : Type u_2} [MeasurableSpace X] (μ : MeasureTheory.Measure X) [Fintype ι] (E : ι → Type u_3) [(i : ι) → NormedAddCommGroup (E i)] [(i : ι) → InnerProductSpace ℂ (E i)] (f : ↥(MeasureTheory.Lp (PiLp 2 E) 2 μ)) : PiLp 2 fun (i : ι) => ↥(MeasureTheory.Lp (E i) 2 μ)

Send a PiLp-valued L² class to its finite family of coordinate classes.

Equations

• LiebThirring.finiteLpPiLpForward μ E f = WithLp.toLp 2 fun (i : ι) => (ContinuousLinearMap.compLpL 2 μ (PiLp.proj 2 E i)) f

noncomputable def LiebThirring.finiteLpPiLpInverse {X : Type u_1} {ι : Type u_2} [MeasurableSpace X] (μ : MeasureTheory.Measure X) [Fintype ι] (E : ι → Type u_3) [(i : ι) → NormedAddCommGroup (E i)] (f : PiLp 2 fun (i : ι) => ↥(MeasureTheory.Lp (E i) 2 μ)) : ↥(MeasureTheory.Lp (PiLp 2 E) 2 μ)

Assemble a finite family of L² classes from their strongly measurable representatives.

Equations

• LiebThirring.finiteLpPiLpInverse μ E f = MeasureTheory.MemLp.toLp (fun (x : X) => WithLp.toLp 2 fun (i : ι) => ↑↑(f.ofLp i) x) ⋯

theorem LiebThirring.finiteLpPiLpInverse_forward {X : Type u_1} {ι : Type u_2} [MeasurableSpace X] (μ : MeasureTheory.Measure X) [Fintype ι] (E : ι → Type u_3) [(i : ι) → NormedAddCommGroup (E i)] [(i : ι) → InnerProductSpace ℂ (E i)] (f : ↥(MeasureTheory.Lp (PiLp 2 E) 2 μ)) : finiteLpPiLpInverse μ E (finiteLpPiLpForward μ E f) = f

theorem LiebThirring.finiteLpPiLpForward_inverse {X : Type u_1} {ι : Type u_2} [MeasurableSpace X] (μ : MeasureTheory.Measure X) [Fintype ι] (E : ι → Type u_3) [(i : ι) → NormedAddCommGroup (E i)] [(i : ι) → InnerProductSpace ℂ (E i)] (f : PiLp 2 fun (i : ι) => ↥(MeasureTheory.Lp (E i) 2 μ)) : finiteLpPiLpForward μ E (finiteLpPiLpInverse μ E f) = f

theorem LiebThirring.finiteLpPiLpForward_add {X : Type u_1} {ι : Type u_2} [MeasurableSpace X] (μ : MeasureTheory.Measure X) [Fintype ι] (E : ι → Type u_3) [(i : ι) → NormedAddCommGroup (E i)] [(i : ι) → InnerProductSpace ℂ (E i)] (f g : ↥(MeasureTheory.Lp (PiLp 2 E) 2 μ)) : finiteLpPiLpForward μ E (f + g) = finiteLpPiLpForward μ E f + finiteLpPiLpForward μ E g

theorem LiebThirring.finiteLpPiLpForward_smul {X : Type u_1} {ι : Type u_2} [MeasurableSpace X] (μ : MeasureTheory.Measure X) [Fintype ι] (E : ι → Type u_3) [(i : ι) → NormedAddCommGroup (E i)] [(i : ι) → InnerProductSpace ℂ (E i)] (c : ℂ) (f : ↥(MeasureTheory.Lp (PiLp 2 E) 2 μ)) : finiteLpPiLpForward μ E (c • f) = c • finiteLpPiLpForward μ E f

theorem LiebThirring.finiteLpPiLpForward_norm {X : Type u_1} {ι : Type u_2} [MeasurableSpace X] (μ : MeasureTheory.Measure X) [Fintype ι] (E : ι → Type u_3) [(i : ι) → NormedAddCommGroup (E i)] [(i : ι) → InnerProductSpace ℂ (E i)] (f : ↥(MeasureTheory.Lp (PiLp 2 E) 2 μ)) : ‖finiteLpPiLpForward μ E f‖ = ‖f‖

noncomputable def LiebThirring.finiteLpPiLpEquiv {X : Type u_1} {ι : Type u_2} [MeasurableSpace X] (μ : MeasureTheory.Measure X) [Fintype ι] (E : ι → Type u_3) [(i : ι) → NormedAddCommGroup (E i)] [(i : ι) → InnerProductSpace ℂ (E i)] : ↥(MeasureTheory.Lp (PiLp 2 E) 2 μ) ≃ₗᵢ[ℂ] PiLp 2 fun (i : ι) => ↥(MeasureTheory.Lp (E i) 2 μ)

The canonical finite-coordinate interchange L²(X; ⨁₂ i, E i) ≃ ⨁₂ i, L²(X; E i).

Equations

• One or more equations did not get rendered due to their size.

theorem LiebThirring.finiteLpPiLpEquiv_apply_ae {X : Type u_1} {ι : Type u_2} [MeasurableSpace X] (μ : MeasureTheory.Measure X) [Fintype ι] (E : ι → Type u_3) [(i : ι) → NormedAddCommGroup (E i)] [(i : ι) → InnerProductSpace ℂ (E i)] (f : ↥(MeasureTheory.Lp (PiLp 2 E) 2 μ)) (i : ι) : ↑↑(((finiteLpPiLpEquiv μ E) f).ofLp i) =ᵐ[μ] fun (x : X) => (↑↑f x).ofLp i

Componentwise representative characterization of the finite-coordinate interchange.