One positive growth profile and one scalar amplitude determine all grade profiles.

theorem EulerPacketCylinderField.timeProfileChange_smul {T T' : ℝ} (g : C(↑(Set.Icc 0 T), ℝ)) (h : T = T') (c : ℝ) : timeProfileChange (c • g) h = c • timeProfileChange g h

theorem EulerPacketTimeProfile.Scales.high_eq_smul_growth {K : Type u_1} [TopologicalSpace K] (S : Scales K) (p : ℕ) : S.high p = meanScale S.H0 p • S.growth

theorem EulerPacketTimeProfile.Scales.high_timeProfile_eq {T T' : ℝ} (S : Scales ↑(Set.Icc 0 T)) (h : T = T') (g : C(↑(Set.Icc 0 T'), ℝ)) (α : ℝ) (hgrowth : EulerPacketCylinderField.timeProfileChange S.growth h = α • g) (p : ℕ) : EulerPacketCylinderField.timeProfileChange (S.high p) h = (α * meanScale S.H0 p) • g

noncomputable def EulerPacketTimeProfile.Scales.ofTimeProfile {T T' : ℝ} (g : C(↑(Set.Icc 0 T), ℝ)) (hg : ∀ (t : ↑(Set.Icc 0 T)), 0 < g t) (h : T = T') (α : ℝ) (hα : 0 < α) : Scales ↑(Set.Icc 0 T')

Of time profile, given by ofGrowth (α • timeProfileChange g h) (fun t => mul_pos hα (timeProfileChange_pos g hg h t)).

Equations

• EulerPacketTimeProfile.Scales.ofTimeProfile g hg h α hα = EulerPacketTimeProfile.Scales.ofGrowth (α • EulerPacketCylinderField.timeProfileChange g h) ⋯

theorem EulerPacketTimeProfile.Scales.ofTimeProfile_growth {T T' : ℝ} (g : C(↑(Set.Icc 0 T), ℝ)) (hg : ∀ (t : ↑(Set.Icc 0 T)), 0 < g t) (h : T = T') (α : ℝ) (hα : 0 < α) : EulerPacketCylinderField.timeProfileChange (ofTimeProfile g hg h α hα).growth ⋯ = α • g

theorem EulerPacketTimeProfile.Scales.ofTimeProfile_high {T T' : ℝ} (g : C(↑(Set.Icc 0 T), ℝ)) (hg : ∀ (t : ↑(Set.Icc 0 T)), 0 < g t) (h : T = T') (α : ℝ) (hα : 0 < α) (p : ℕ) : EulerPacketCylinderField.timeProfileChange ((ofTimeProfile g hg h α hα).high p) ⋯ = (α * meanScale (ofTimeProfile g hg h α hα).H0 p) • g

theorem EulerPacketTimeProfile.Scales.gradeFactor_pos {K : Type u_1} [TopologicalSpace K] (S : Scales K) (α : ℝ) (hα : 0 < α) (p : ℕ) : 0 < α * meanScale S.H0 p