The L² derivative-field construction is a contraction between the actual Banach spaces.

noncomputable def EulerLpDerivative.bundlingLinear {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) : ↥(MeasureTheory.Lp (P →L[ℝ] V) 2 μ) →ₗ[ℝ] P →L[ℝ] ↥(MeasureTheory.Lp V 2 μ)

Bundling linear, bundling toFun, map_add, map_smul.

Equations

• EulerLpDerivative.bundlingLinear μ = { toFun := EulerLpDerivative.derivativeMap μ, map_add' := ⋯, map_smul' := ⋯ }

noncomputable def EulerLpDerivative.derivativeBundling {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) : ↥(MeasureTheory.Lp (P →L[ℝ] V) 2 μ) →L[ℝ] P →L[ℝ] ↥(MeasureTheory.Lp V 2 μ)

Derivative bundling, bundling toLinearMap, cont.

Equations

• EulerLpDerivative.derivativeBundling μ = { toLinearMap := EulerLpDerivative.bundlingLinear μ, cont := ⋯ }

@[simp]

theorem EulerLpDerivative.derivativeBundling_apply {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) (D : ↥(MeasureTheory.Lp (P →L[ℝ] V) 2 μ)) : (derivativeBundling μ) D = derivativeMap μ D

theorem EulerLpDerivative.derivativeBundling_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) : ‖derivativeBundling μ‖ ≤ 1