Smoothness and actual time differentiation of the normalized cross multiplier.

@[instance_reducible]

noncomputable def EulerPacketCrossProduct.instPacketPotentialMultiplier1 : NormedAddCommGroup (EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space)

Cache the standard NormedAddCommGroup (Space →L[ℝ] Space) instance to shorten typeclass synthesis.

Equations

• EulerPacketCrossProduct.instPacketPotentialMultiplier1 = inferInstance

@[instance_reducible]

noncomputable def EulerPacketCrossProduct.instPacketPotentialMultiplier2 : NormedSpace ℝ (EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space)

Cache the standard NormedSpace ℝ (Space →L[ℝ] Space) instance to shorten typeclass synthesis.

Equations

• EulerPacketCrossProduct.instPacketPotentialMultiplier2 = inferInstance

@[instance_reducible]

noncomputable def EulerPacketCrossProduct.instPacketPotentialMultiplier3 : AddCommGroup (EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space)

Cache the standard AddCommGroup (Space →L[ℝ] Space) instance to shorten typeclass synthesis.

Equations

• EulerPacketCrossProduct.instPacketPotentialMultiplier3 = inferInstance.toAddCommGroup

@[instance_reducible]

noncomputable def EulerPacketCrossProduct.instPacketPotentialMultiplier4 : Module ℝ (EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space)

Cache the standard Module ℝ (Space →L[ℝ] Space) instance to shorten typeclass synthesis.

Equations

• EulerPacketCrossProduct.instPacketPotentialMultiplier4 = inferInstance.toModule

@[instance_reducible]

noncomputable def EulerPacketCrossProduct.instPacketPotentialMultiplier5 : TopologicalSpace (EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space)

Cache the standard TopologicalSpace (Space →L[ℝ] Space) instance to shorten typeclass synthesis.

Equations

• EulerPacketCrossProduct.instPacketPotentialMultiplier5 = PseudoMetricSpace.toUniformSpace.toTopologicalSpace

noncomputable def EulerPacketCrossProduct.crossOperatorLinear : EulerSmoothLimit.Space →ₗ[ℝ] EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space

Cross operator linear, bundling toFun, map_add, map_smul.

Equations

• EulerPacketCrossProduct.crossOperatorLinear = { toFun := EulerPacketCrossProduct.crossLeft, map_add' := ⋯, map_smul' := ⋯ }

noncomputable def EulerPacketCrossProduct.crossOperator : EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space

Cross operator, given by crossOperatorLinear.mkContinuous 1 (fun a => by change ‖crossLeft a‖ ≤ 1*‖a‖ simpa only [one_mul] using crossLeft_norm_le a).

Equations

• EulerPacketCrossProduct.crossOperator = EulerPacketCrossProduct.crossOperatorLinear.mkContinuous 1 ⋯

@[simp]

theorem EulerPacketCrossProduct.crossOperator_apply (a : EulerSmoothLimit.Space) : crossOperator a = crossLeft a

theorem EulerPacketCrossProduct.potentialMultiplier_eq_inner (m : EulerSmoothLimit.Space) : potentialMultiplier m = -(inner ℝ m m)⁻¹ • crossOperator m

theorem EulerPacketCrossProduct.potentialMultiplier_contDiff {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] (m : X → EulerSmoothLimit.Space) (hm : ContDiff ℝ (↑⊤) m) (hnz : ∀ (x : X), m x ≠ 0) : ContDiff ℝ ↑⊤ fun (x : X) => potentialMultiplier (m x)

noncomputable def EulerPacketCrossProduct.potentialMultiplierDerivative (m mt : EulerSmoothLimit.Space) : EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space

Potential multiplier derivative, given by (2*⟪m,mt⟫_ℝ/(‖m‖^2)^2) • crossLeft m - ((‖m‖^2)⁻¹) • crossLeft mt.

Equations

• EulerPacketCrossProduct.potentialMultiplierDerivative m mt = (2 * inner ℝ m mt / (‖m‖ ^ 2) ^ 2) • EulerPacketCrossProduct.crossLeft m - (‖m‖ ^ 2)⁻¹ • EulerPacketCrossProduct.crossLeft mt

theorem EulerPacketCrossProduct.potentialMultiplier_hasDerivWithinAt (s : Set ℝ) (t : ℝ) (m : ℝ → EulerSmoothLimit.Space) (mt : EulerSmoothLimit.Space) (hm : HasDerivWithinAt m mt s t) (hnz : m t ≠ 0) : HasDerivWithinAt (fun (r : ℝ) => potentialMultiplier (m r)) (potentialMultiplierDerivative (m t) mt) s t

The derivative formula is valid for a time curve on its actual time set.