The actual grade scale is controlled by the source bound on alpha*g. No reciprocal of alpha or extremum ratio of g enters this estimate.

theorem EulerPacketTimeProfile.Scales.ofGrowth_H0_le {K : Type u_1} [TopologicalSpace K] [CompactSpace K] (g : C(K, ℝ)) (hg : ∀ (t : K), 0 < g t) (B : ℝ) (hB : 1 ≤ B) (hbound : ∀ (t : K), g t ≤ B) : (ofGrowth g hg).H0 ≤ B

theorem EulerPacketTimeProfile.Scales.ofTimeProfile_H0_le {T T' : ℝ} (g : C(↑(Set.Icc 0 T), ℝ)) (hg : ∀ (t : ↑(Set.Icc 0 T)), 0 < g t) (h : T = T') (α : ℝ) (hα : 0 < α) (B : ℝ) (hB : 1 ≤ B) (hbound : ∀ (t : ↑(Set.Icc 0 T)), α * g t ≤ B) : (ofTimeProfile g hg h α hα).H0 ≤ B

theorem EulerElapsedTimePathGluing.smul_profile_le (S τ : ℝ) (hτ0 : 0 ≤ τ) (hτS : τ ≤ S) (g : C(↑(Set.Icc 0 (S - τ)), ℝ)) (hg0 : g ⟨0, ⋯⟩ = 1) (α B : ℝ) (hα : α ≤ B) (hbound : ∀ (t : ↑(Set.Icc 0 (S - τ))), α * g t ≤ B) (t : ↑(Set.Icc 0 S)) : α * (profile S τ hτ0 hτS g hg0) t ≤ B