Exact scalar homogeneity of the actual compact terminal-data primary.

noncomputable def EulerTransversePacketProvider.InitialData.smul {P : ℝ} [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] {D : Data U} (Y : InitialData P D) (a : ℝ) : InitialData P D

Smul, bundling value, orbit, mean_zero.

Equations

• Y.smul a = { value := a • Y.value, orbit := ⋯, mean_zero := ⋯ }

theorem EulerTransversePacketPrimary.forwardInitial_eq_smul {P : ℝ} [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {D : EulerTransversePacketProvider.Data U} (τ : ℝ) (hτ : 0 < τ) (hτT : τ < D.T) (B : EulerTransversePacketProvider.HistoryData (D.initial τ hτ ⋯)) (Y Z : EulerTransversePacketProvider.InitialData P D) (a : ℝ) (h : Z.value = a • Y.value) : (forwardInitial τ hτ hτT B Z).value = a • (forwardInitial τ hτ hτT B Y).value

theorem EulerTransversePacketPrimary.pastVelocity_eq_smul {P : ℝ} [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {D : EulerTransversePacketProvider.Data U} (τ : ℝ) (hτ : 0 < τ) (hτT : τ < D.T) (B : EulerTransversePacketProvider.HistoryData (D.initial τ hτ ⋯)) (Y Z : EulerTransversePacketProvider.InitialData P D) (a : ℝ) (h : Z.value = a • Y.value) : pastVelocity τ hτ hτT B Z = a • pastVelocity τ hτ hτT B Y

theorem EulerTransversePacketPrimary.pastDerivative_eq_smul {P : ℝ} [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {D : EulerTransversePacketProvider.Data U} (τ : ℝ) (hτ : 0 < τ) (hτT : τ < D.T) (B : EulerTransversePacketProvider.HistoryData (D.initial τ hτ ⋯)) (Y Z : EulerTransversePacketProvider.InitialData P D) (a : ℝ) (h : Z.value = a • Y.value) : pastDerivative τ hτ hτT B Z = a • pastDerivative τ hτ hτT B Y

theorem EulerTransversePacketPrimary.futureVelocity_eq_smul {P : ℝ} [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {D : EulerTransversePacketProvider.Data U} (τ : ℝ) (hτ : 0 < τ) (hτT : τ < D.T) (B : EulerTransversePacketProvider.HistoryData (D.initial τ hτ ⋯)) (Y Z : EulerTransversePacketProvider.InitialData P D) (a : ℝ) (h : Z.value = a • Y.value) : futureVelocity τ hτ hτT B Z = a • futureVelocity τ hτ hτT B Y

theorem EulerTransversePacketPrimary.futureDerivative_eq_smul {P : ℝ} [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {D : EulerTransversePacketProvider.Data U} (τ : ℝ) (hτ : 0 < τ) (hτT : τ < D.T) (B : EulerTransversePacketProvider.HistoryData (D.initial τ hτ ⋯)) (Y Z : EulerTransversePacketProvider.InitialData P D) (a : ℝ) (h : Z.value = a • Y.value) : futureDerivative τ hτ hτT B Z = a • futureDerivative τ hτ hτT B Y

theorem EulerTransversePacketPrimary.velocityPath_eq_smul {P : ℝ} [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {D : EulerTransversePacketProvider.Data U} (τ : ℝ) (hτ : 0 < τ) (hτT : τ < D.T) (B : EulerTransversePacketProvider.HistoryData (D.initial τ hτ ⋯)) (Y Z : EulerTransversePacketProvider.InitialData P D) (a : ℝ) (h : Z.value = a • Y.value) : velocityPath τ hτ hτT B Z = a • velocityPath τ hτ hτT B Y

theorem EulerTransversePacketPrimary.derivativePath_eq_smul {P : ℝ} [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {D : EulerTransversePacketProvider.Data U} (τ : ℝ) (hτ : 0 < τ) (hτT : τ < D.T) (B : EulerTransversePacketProvider.HistoryData (D.initial τ hτ ⋯)) (Y Z : EulerTransversePacketProvider.InitialData P D) (a : ℝ) (h : Z.value = a • Y.value) : derivativePath τ hτ hτT B Z = a • derivativePath τ hτ hτT B Y