Differentiating the actual normalized ray and primary velocity. The rates are derived from the physical ODEs; no normalized-frame equation is assumed.

noncomputable def EulerPacketNormalizedPrimary.unit {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (x : E) : E

Unit, given by ‖x‖⁻¹ • x.

Equations

• EulerPacketNormalizedPrimary.unit x = ‖x‖⁻¹ • x

theorem EulerPacketNormalizedPrimary.unit_norm {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {x : E} (hx : x ≠ 0) : ‖unit x‖ = 1

theorem EulerPacketNormalizedPrimary.unit_inner_self {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {x : E} (hx : x ≠ 0) : inner ℝ (unit x) (unit x) = 1

theorem EulerPacketNormalizedPrimary.unit_inner_zero {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {x y : E} (hxy : inner ℝ x y = 0) : inner ℝ (unit x) (unit y) = 0

theorem EulerPacketNormalizedPrimary.norm_hasDerivAt {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {f : ℝ → E} {f' : E} {t : ℝ} (hf : HasDerivAt f f' t) (hft : f t ≠ 0) : HasDerivAt (fun (s : ℝ) => ‖f s‖) (inner ℝ (f t) f' / ‖f t‖) t

theorem EulerPacketNormalizedPrimary.unit_hasDerivAt {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {f : ℝ → E} {f' : E} {t : ℝ} (hf : HasDerivAt f f' t) (hft : f t ≠ 0) : HasDerivAt (fun (s : ℝ) => unit (f s)) (‖f t‖⁻¹ • f' - (inner ℝ (f t) f' / ‖f t‖ ^ 3) • f t) t

theorem EulerPacketNormalizedPrimary.norm_hasDerivWithinAt {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {f : ℝ → E} {f' : E} {t : ℝ} {S : Set ℝ} (hf : HasDerivWithinAt f f' S t) (hft : f t ≠ 0) : HasDerivWithinAt (fun (s : ℝ) => ‖f s‖) (inner ℝ (f t) f' / ‖f t‖) S t

theorem EulerPacketNormalizedPrimary.unit_hasDerivWithinAt {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {f : ℝ → E} {f' : E} {t : ℝ} {S : Set ℝ} (hf : HasDerivWithinAt f f' S t) (hft : f t ≠ 0) : HasDerivWithinAt (fun (s : ℝ) => unit (f s)) (‖f t‖⁻¹ • f' - (inner ℝ (f t) f' / ‖f t‖ ^ 3) • f t) S t

noncomputable def EulerPacketNormalizedPrimary.rayRate {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (B : E →L[ℝ] E) (p : E) : E

Ray rate, given by -B.adjoint p + ⟪p,B p⟫_ℝ • p.

Equations

• EulerPacketNormalizedPrimary.rayRate B p = -(ContinuousLinearMap.adjoint B) p + inner ℝ p (B p) • p

def EulerPacketNormalizedPrimary.velocityRate {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (B : E →L[ℝ] E) (p q : E) : E

Velocity rate, given by -B q + (2*⟪p,B q⟫_ℝ) • p + ⟪q,B q⟫_ℝ • q.

Equations

• EulerPacketNormalizedPrimary.velocityRate B p q = -B q + (2 * inner ℝ p (B q)) • p + inner ℝ q (B q) • q

theorem EulerPacketNormalizedPrimary.normalized_ray_hasDerivAt {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (B : E →L[ℝ] E) {m : ℝ → E} {t : ℝ} (hm : HasDerivAt m (-(ContinuousLinearMap.adjoint B) (m t)) t) (hm0 : m t ≠ 0) : HasDerivAt (fun (s : ℝ) => unit (m s)) (rayRate B (unit (m t))) t

theorem EulerPacketNormalizedPrimary.normalized_velocity_hasDerivAt {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (B : E →L[ℝ] E) {m v : ℝ → E} {t : ℝ} (hv : HasDerivAt v (-B (v t) + (2 * inner ℝ (m t) (B (v t)) / ‖m t‖ ^ 2) • m t) t) (hv0 : v t ≠ 0) (hmv : inner ℝ (m t) (v t) = 0) : HasDerivAt (fun (s : ℝ) => unit (v s)) (velocityRate B (unit (m t)) (unit (v t))) t

theorem EulerPacketNormalizedPrimary.normalized_ray_hasDerivWithinAt {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (B : E →L[ℝ] E) {m : ℝ → E} {t : ℝ} {S : Set ℝ} (hm : HasDerivWithinAt m (-(ContinuousLinearMap.adjoint B) (m t)) S t) (hm0 : m t ≠ 0) : HasDerivWithinAt (fun (s : ℝ) => unit (m s)) (rayRate B (unit (m t))) S t

theorem EulerPacketNormalizedPrimary.normalized_velocity_hasDerivWithinAt {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (B : E →L[ℝ] E) {m v : ℝ → E} {t : ℝ} {S : Set ℝ} (hv : HasDerivWithinAt v (-B (v t) + (2 * inner ℝ (m t) (B (v t)) / ‖m t‖ ^ 2) • m t) S t) (hv0 : v t ≠ 0) (hmv : inner ℝ (m t) (v t) = 0) : HasDerivWithinAt (fun (s : ℝ) => unit (v s)) (velocityRate B (unit (m t)) (unit (v t))) S t