Dependence of the actual Bochner multiplier on its coefficient

The coefficient-to-operator map is constructed as a bounded linear map. Thus parameter derivatives of time-dependent coefficients give actual operator-norm derivatives, rather than an assumed regular family of solution operators.

theorem EulerTimeLpCoefficientMap.timeMultiplier_add {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (T : ℝ) (hT : 0 ≤ T) (A B : C(↑(Set.Icc 0 T), E →L[ℝ] F)) : EulerTimeLp.timeMultiplier T hT (A + B) = EulerTimeLp.timeMultiplier T hT A + EulerTimeLp.timeMultiplier T hT B

The genuine multiplier is additive in the coefficient.

theorem EulerTimeLpCoefficientMap.timeMultiplier_smul {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (T : ℝ) (hT : 0 ≤ T) (r : ℝ) (A : C(↑(Set.Icc 0 T), E →L[ℝ] F)) : EulerTimeLp.timeMultiplier T hT (r • A) = r • EulerTimeLp.timeMultiplier T hT A

The genuine multiplier is homogeneous in the coefficient.

theorem EulerTimeLpCoefficientMap.timeMultiplier_norm {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (T : ℝ) (hT : 0 ≤ T) (A : C(↑(Set.Icc 0 T), E →L[ℝ] F)) : ‖EulerTimeLp.timeMultiplier T hT A‖ ≤ ‖A‖

The operator norm is bounded by the actual uniform coefficient norm.

noncomputable def EulerTimeLpCoefficientMap.coefficientLinear {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (T : ℝ) (hT : 0 ≤ T) : C(↑(Set.Icc 0 T), E →L[ℝ] F) →ₗ[ℝ] ↥(EulerTimeLp.TimeLp T E) →L[ℝ] ↥(EulerTimeLp.TimeLp T F)

The actual bounded linear coefficient-to-Bochner-multiplier map.

Equations

• EulerTimeLpCoefficientMap.coefficientLinear T hT = { toFun := EulerTimeLp.timeMultiplier T hT, map_add' := ⋯, map_smul' := ⋯ }

noncomputable def EulerTimeLpCoefficientMap.coefficientMap {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (T : ℝ) (hT : 0 ≤ T) : C(↑(Set.Icc 0 T), E →L[ℝ] F) →L[ℝ] ↥(EulerTimeLp.TimeLp T E) →L[ℝ] ↥(EulerTimeLp.TimeLp T F)

The coefficient map is bounded for the actual uniform and operator norms.

Equations

• EulerTimeLpCoefficientMap.coefficientMap T hT = { toLinearMap := EulerTimeLpCoefficientMap.coefficientLinear T hT, cont := ⋯ }

theorem EulerTimeLpCoefficientMap.hasDerivAt_timeMultiplier {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (T : ℝ) (hT : 0 ≤ T) (A : ℝ → C(↑(Set.Icc 0 T), E →L[ℝ] F)) (A₁ : C(↑(Set.Icc 0 T), E →L[ℝ] F)) (x : ℝ) (hA : HasDerivAt A A₁ x) : HasDerivAt (fun (r : ℝ) => EulerTimeLp.timeMultiplier T hT (A r)) (EulerTimeLp.timeMultiplier T hT A₁) x

Coefficient derivatives give genuine operator-norm derivatives of the time multiplier.

theorem EulerTimeLpCoefficientMap.contDiff_timeMultiplier {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (T : ℝ) (hT : 0 ≤ T) {P : Type u_3} [NormedAddCommGroup P] [NormedSpace ℝ P] (A : P → C(↑(Set.Icc 0 T), E →L[ℝ] F)) {n : WithTop ℕ∞} (hA : ContDiff ℝ n A) : ContDiff ℝ n fun (x : P) => EulerTimeLp.timeMultiplier T hT (A x)

Every order of actual coefficient regularity passes to operator norm regularity.

theorem EulerTimeLpCoefficientMap.hasDerivAt_productDerivative {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (T : ℝ) (hT : 0 ≤ T) (A B : ℝ → C(↑(Set.Icc 0 T), E →L[ℝ] F)) (A₁ B₁ : C(↑(Set.Icc 0 T), E →L[ℝ] F)) (x : ℝ) (hA : HasDerivAt A A₁ x) (hB : HasDerivAt B B₁ x) : HasDerivAt (fun (r : ℝ) => EulerTimeH1OperatorProduct.productDerivative T hT (A r) (B r)) (EulerTimeLp.timeMultiplier T hT B₁ ∘SL EulerTerminalTimePrimitive.primitiveTimeLp T hT + EulerTimeLp.timeMultiplier T hT A₁) x

Differentiating the actual frame H¹ transport with respect to an external parameter.

theorem EulerTimeLpCoefficientMap.contDiff_productDerivative {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (T : ℝ) (hT : 0 ≤ T) {P : Type u_3} [NormedAddCommGroup P] [NormedSpace ℝ P] (A B : P → C(↑(Set.Icc 0 T), E →L[ℝ] F)) {n : WithTop ℕ∞} (hA : ContDiff ℝ n A) (hB : ContDiff ℝ n B) : ContDiff ℝ n fun (x : P) => EulerTimeH1OperatorProduct.productDerivative T hT (A x) (B x)

Arbitrary-order parameter regularity of the genuine H¹ frame transport.