The finite initial base used by the limiting construction is the actual first normal forward packet over the actual first packet state.
theorem
EulerPacketInduction.Stage.forwardNext_initial_support
{q : ℕ}
{B : ℝ}
{S : EulerPacketInductionScales.Scales (↑q) B}
(P : Stage S 0)
(hq : EulerParentNeighborThreshold.requiredExponent ≤ q)
(hB :
EulerParentNeighborThreshold.commonThreshold EulerPacketLowConstants.gradientConstant
EulerPacketLowConstants.hessianConstant ≤ B)
(hP : (tsupport fun (x : EulerSmoothLimit.Space) => P.state.evolution.velocity (0, x)) ⊆ Metric.closedBall 0 2)
:
(tsupport fun (x : EulerSmoothLimit.Space) => (P.forwardNext hq hB).state.evolution.velocity (0, x)) ⊆
Metric.closedBall 0 2
theorem
EulerPacketInduction.Stage.forwardNext_initial_field_support
{q : ℕ}
{B : ℝ}
{S : EulerPacketInductionScales.Scales (↑q) B}
(P : Stage S 0)
(hq : EulerParentNeighborThreshold.requiredExponent ≤ q)
(hB :
EulerParentNeighborThreshold.commonThreshold EulerPacketLowConstants.gradientConstant
EulerPacketLowConstants.hessianConstant ≤ B)
(hP : (tsupport fun (x : EulerSmoothLimit.Space) => P.state.evolution.velocity (0, x)) ⊆ Metric.closedBall 0 2)
:
tsupport ((P.forwardNext hq hB).state.regularity.velocity (P.forwardNext hq hB).parent.zeroTime).field ⊆
Metric.closedBall 0 2
theorem
EulerPacketInductionScales.Scales.firstForwardStage_initial_support
{q : ℕ}
{B : ℝ}
(S : Scales (↑q) B)
(hq : EulerParentNeighborThreshold.requiredExponent ≤ q)
(hB :
EulerParentNeighborThreshold.commonThreshold EulerPacketLowConstants.gradientConstant
EulerPacketLowConstants.hessianConstant ≤ B)
:
(tsupport fun (x : EulerSmoothLimit.Space) => (S.firstStage.forwardNext hq hB).state.evolution.velocity (0, x)) ⊆
Metric.closedBall 0 2
theorem
EulerPacketInductionScales.Scales.firstForwardStage_initial_field_support
{q : ℕ}
{B : ℝ}
(S : Scales (↑q) B)
(hq : EulerParentNeighborThreshold.requiredExponent ≤ q)
(hB :
EulerParentNeighborThreshold.commonThreshold EulerPacketLowConstants.gradientConstant
EulerPacketLowConstants.hessianConstant ≤ B)
:
tsupport
((S.firstStage.forwardNext hq hB).state.regularity.velocity
(S.firstStage.forwardNext hq hB).parent.zeroTime).field ⊆
Metric.closedBall 0 2