The source deformation can be equipped with the actual activation normal. The new reference plane is the literal orthogonal complement, and the history hypotheses are inherited without any new analytic input.

noncomputable def EulerTransversePacketProvider.Data.reframe {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : Data U) (m : EulerSmoothLimit.Space) (hm : ‖m‖ = 1) : Data ↥(EulerTransverseFrameCoordinates.referencePlane m)

Reframe, bundling T, T_pos, support, support_compact and the required compatibility proofs.

Equations

• One or more equations did not get rendered due to their size.

def EulerTransversePacketProvider.HistoryData.reframe {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] {D : Data U} (B : HistoryData D) (m : EulerSmoothLimit.Space) (hm : ‖m‖ = 1) : HistoryData (D.reframe m hm)

Reframe, bundling H, jacobi, potential, potential_nonneg and the required compatibility proofs.

Equations

• B.reframe m hm = { H := B.H, jacobi := ⋯, potential := B.potential, potential_nonneg := ⋯, potential_bound := ⋯, small := ⋯ }

noncomputable def EulerTransversePacketProvider.Data.activation {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : Data U) (t₀ : ↑(Set.Icc 0 D.T)) (n : EulerSmoothLimit.Space) (hn : n ≠ 0) : Data ↥(EulerTransverseFrameCoordinates.referencePlane (EulerPacketMovingFrame.activationDirection (D.deformationEquiv t₀ 0) n))

Activation, given by D.reframe (activationDirection (D.deformationEquiv t₀ 0) n) (activationDirection_unit _ hn).

Equations

• D.activation t₀ n hn = D.reframe (EulerPacketMovingFrame.activationDirection (D.deformationEquiv t₀ 0) n) ⋯

theorem EulerTransversePacketProvider.Data.activation_normal {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : Data U) (t₀ : ↑(Set.Icc 0 D.T)) (n : EulerSmoothLimit.Space) (hn : n ≠ 0) : ((D.activation t₀ n hn).normal.field t₀) 0 = EulerPacketMovingFrame.activationRayScale (D.deformationEquiv t₀ 0) n • n

noncomputable def EulerTransversePacketProvider.HistoryData.activation {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] {D : Data U} (B : HistoryData D) (t₀ : ↑(Set.Icc 0 D.T)) (n : EulerSmoothLimit.Space) (hn : n ≠ 0) : HistoryData (D.activation t₀ n hn)

Activation, given by B.reframe (activationDirection (D.deformationEquiv t₀ 0) n) (activationDirection_unit _ hn).

Equations

• B.activation t₀ n hn = B.reframe (EulerPacketMovingFrame.activationDirection (D.deformationEquiv t₀ 0) n) ⋯

theorem EulerTransversePacketProvider.Data.activationRayScale_bounds {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : Data U) (t₀ : ↑(Set.Icc 0 D.T)) (n : EulerSmoothLimit.Space) (hn : ‖n‖ = 1) : 0 < EulerPacketMovingFrame.activationRayScale (D.deformationEquiv t₀ 0) n ∧ EulerPacketMovingFrame.activationRayScale (D.deformationEquiv t₀ 0) n ≤ D.inverseBound ∧ (EulerPacketMovingFrame.activationRayScale (D.deformationEquiv t₀ 0) n)⁻¹ ≤ D.frameBound