Currying an actual L² field of derivatives into a bounded derivative operator.

noncomputable def EulerLpDerivative.applyDerivative {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 μ)) (a : P) : ↥(MeasureTheory.Lp V 2 μ)

Apply derivative, given by (ContinuousLinearMap.apply ℝ V a).compLpL 2 μ D.

Equations

• EulerLpDerivative.applyDerivative μ D a = (ContinuousLinearMap.compLpL 2 μ ((ContinuousLinearMap.apply ℝ V) a)) D

theorem EulerLpDerivative.applyDerivative_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) (D : ↥(MeasureTheory.Lp (P →L[ℝ] V) 2 μ)) (a : P) : ↑↑(applyDerivative μ D a) =ᵐ[μ] fun (x : X) => (↑↑D x) a

theorem EulerLpDerivative.applyDerivative_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) (D : ↥(MeasureTheory.Lp (P →L[ℝ] V) 2 μ)) (a : P) : ‖applyDerivative μ D a‖ ≤ ‖D‖ * ‖a‖

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

Derivative linear, bundling toFun, map_add, map_smul.

Equations

• EulerLpDerivative.derivativeLinear μ D = { toFun := EulerLpDerivative.applyDerivative μ D, map_add' := ⋯, map_smul' := ⋯ }

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

This is a concrete bounded derivative with values in the actual L² function space.

Equations

• EulerLpDerivative.derivativeMap μ D = (EulerLpDerivative.derivativeLinear μ D).mkContinuous ‖D‖ ⋯

theorem EulerLpDerivative.derivativeMap_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) (D : ↥(MeasureTheory.Lp (P →L[ℝ] V) 2 μ)) (a : P) : ↑↑((derivativeMap μ D) a) =ᵐ[μ] fun (x : X) => (↑↑D x) a

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