Pointwise multilinear L² fields define genuine bounded multilinear maps into L².

noncomputable def EulerLpDerivative.multilinearBundling {X : Type u_1} {P : Type u_2} {V : Type u_3} [MeasurableSpace X] [NormedAddCommGroup P] [NormedSpace ℝ P] [NormedAddCommGroup V] [NormedSpace ℝ V] (μ : MeasureTheory.Measure X) (n : ℕ) : ↥(MeasureTheory.Lp (P [×n]→L[ℝ] V) 2 μ) →L[ℝ] P [×n]→L[ℝ] ↥(MeasureTheory.Lp V 2 μ)

Multilinear bundling as an element of Lp (P [×n]→L[ℝ] V) 2 μ →L[ℝ] (P [×n]→L[ℝ] Lp V 2 μ).

Equations

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

theorem EulerLpDerivative.multilinearBundling_ae {X : Type u_1} {P : Type u_2} {V : Type u_3} [MeasurableSpace X] [NormedAddCommGroup P] [NormedSpace ℝ P] [NormedAddCommGroup V] [NormedSpace ℝ V] (μ : MeasureTheory.Measure X) (n : ℕ) (D : ↥(MeasureTheory.Lp (P [×n]→L[ℝ] V) 2 μ)) (v : Fin n → P) : ↑↑(((multilinearBundling μ n) D) v) =ᵐ[μ] fun (x : X) => (↑↑D x) v

theorem EulerLpDerivative.multilinearBundling_apply_norm_le {X : Type u_1} {P : Type u_2} {V : Type u_3} [MeasurableSpace X] [NormedAddCommGroup P] [NormedSpace ℝ P] [NormedAddCommGroup V] [NormedSpace ℝ V] (μ : MeasureTheory.Measure X) (n : ℕ) (D : ↥(MeasureTheory.Lp (P [×n]→L[ℝ] V) 2 μ)) : ‖(multilinearBundling μ n) D‖ ≤ ‖D‖

theorem EulerLpDerivative.multilinearBundling_norm_le_one {X : Type u_1} {P : Type u_2} {V : Type u_3} [MeasurableSpace X] [NormedAddCommGroup P] [NormedSpace ℝ P] [NormedAddCommGroup V] [NormedSpace ℝ V] (μ : MeasureTheory.Measure X) (n : ℕ) : ‖multilinearBundling μ n‖ ≤ 1