The literal normalized covector choice for the next source normal. It has unit length and its inverse-transpose transport is exactly the prescribed old-frame cross direction, with a positive scale.

noncomputable def EulerPacketMovingFrame.activationDirection (F : EulerSmoothLimit.Space ≃L[ℝ] EulerSmoothLimit.Space) (n : EulerSmoothLimit.Space) : EulerSmoothLimit.Space

Activation direction, given by unit (F.toContinuousLinearMap.adjoint n).

Equations

• EulerPacketMovingFrame.activationDirection F n = EulerPacketNormalizedPrimary.unit ((ContinuousLinearMap.adjoint ↑F) n)

noncomputable def EulerPacketMovingFrame.activationRayScale (F : EulerSmoothLimit.Space ≃L[ℝ] EulerSmoothLimit.Space) (n : EulerSmoothLimit.Space) : ℝ

Activation ray scale, given by ‖F.toContinuousLinearMap.adjoint n‖⁻¹.

Equations

• EulerPacketMovingFrame.activationRayScale F n = ‖(ContinuousLinearMap.adjoint ↑F) n‖⁻¹

theorem EulerPacketMovingFrame.inverse_adjoint_forward_adjoint (F : EulerSmoothLimit.Space ≃L[ℝ] EulerSmoothLimit.Space) (n : EulerSmoothLimit.Space) : (ContinuousLinearMap.adjoint ↑F.symm) ((ContinuousLinearMap.adjoint ↑F) n) = n

theorem EulerPacketMovingFrame.forward_adjoint_ne_zero (F : EulerSmoothLimit.Space ≃L[ℝ] EulerSmoothLimit.Space) {n : EulerSmoothLimit.Space} (hn : n ≠ 0) : (ContinuousLinearMap.adjoint ↑F) n ≠ 0

theorem EulerPacketMovingFrame.activationDirection_unit (F : EulerSmoothLimit.Space ≃L[ℝ] EulerSmoothLimit.Space) {n : EulerSmoothLimit.Space} (hn : n ≠ 0) : ‖activationDirection F n‖ = 1

theorem EulerPacketMovingFrame.activationRayScale_pos (F : EulerSmoothLimit.Space ≃L[ℝ] EulerSmoothLimit.Space) {n : EulerSmoothLimit.Space} (hn : n ≠ 0) : 0 < activationRayScale F n

theorem EulerPacketMovingFrame.activationDirection_transport (F : EulerSmoothLimit.Space ≃L[ℝ] EulerSmoothLimit.Space) (n : EulerSmoothLimit.Space) : (ContinuousLinearMap.adjoint ↑F.symm) (activationDirection F n) = activationRayScale F n • n

theorem EulerPacketMovingFrame.actual_normal_of_activation_choice {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : EulerTransversePacketProvider.Data U) (t : ↑(Set.Icc 0 D.T)) (x n : EulerSmoothLimit.Space) (hchoice : D.m₀ = activationDirection (D.deformationEquiv t x) n) : (D.normal.field t) x = activationRayScale (D.deformationEquiv t x) n • n

theorem EulerPacketMovingFrame.actual_activation_scaled_ray {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : EulerTransversePacketProvider.Data U) (m v : ℝ → EulerSmoothLimit.Space) (t₀ : ↑(Set.Icc 0 D.T)) (a ε : ℝ) (hm : m ↑t₀ ≠ 0) (hv : v ↑t₀ ≠ 0) (hmv : inner ℝ (m ↑t₀) (v ↑t₀) = 0) (hchoice : D.m₀ = activationDirection (D.deformationEquiv t₀ 0) (EulerPacketCrossProduct.cross (EulerPacketNormalizedPrimary.unit (m ↑t₀)) (EulerPacketNormalizedPrimary.unit (v ↑t₀)))) : have s₀ := activationRayScale (D.deformationEquiv t₀ 0) (EulerPacketCrossProduct.cross (EulerPacketNormalizedPrimary.unit (m ↑t₀)) (EulerPacketNormalizedPrimary.unit (v ↑t₀))); 0 < s₀ ∧ scaledRay m v (fun (s : ℝ) => (D.normal.field (D.clamp s)) 0) s₀ (↑t₀) a ε 0 = ![0, 0, 1]