Profile budgets and their actual path witnesses transport across equal time endpoints.
theorem
EulerPacketCylinderField.ProfileBudget.changeTime
{P T T' : ℝ}
[Fact (0 < P)]
{hT : 0 ≤ T}
{support : Set EulerSmoothLimit.Space}
{a : EulerPacketProfileRecursion.Profile}
{G : ProfileRegularity P T hT support a}
{S : EulerPacketTimeProfile.Scales ↑(Set.Icc 0 T)}
{R : ℝ}
{p : ℕ}
(B : ProfileBudget G S R p)
(h : T = T')
(hT' : 0 ≤ T')
:
ProfileBudget (G.changeTime h hT') (S.changeTime h) R p
theorem
EulerPacketTimeProfile.Scales.growth_changeTime
{T T' : ℝ}
(S : Scales ↑(Set.Icc 0 T))
(h : T = T')
: