The actual finite initial base of the induction is compactly supported: it is the compact smooth datum plus its first packet's literal compact initial increment.
theorem
EulerBaseDatum.packetBase_initial_support
(β : ℝ)
(hβ : |β| ≤ 1)
(ell : ℝ)
(hell : 0 < ell)
(hell1 : ell ≤ 1)
(T : ℝ)
(hT : 0 < T)
(hTB : T ≤ initialTime)
:
(tsupport fun (x : EulerSmoothLimit.Space) =>
(packetBaseState β hβ ell hell hell1 T hT hTB).evolution.velocity (0, x)) ⊆
Metric.closedBall 0 2
theorem
EulerBaseDatum.FirstPacketChoice.initial_support
{β : ℝ}
{hβ : |β| ≤ 1}
{ell : ℝ}
{hell : 0 < ell}
{hell1 : ell ≤ 1}
{T : ℝ}
{hT : 0 < T}
{hTB : T ≤ initialTime}
{δ : ℝ}
{hδ : 0 < δ}
{hchild k : ℝ}
{hk : EulerPacketSourceFrequency.UniversalFrequency k}
{nextEll : ℝ}
{hnext : 0 < nextEll}
{hnext1 : nextEll ≤ 1}
(F : FirstPacketChoice β hβ ell hell hell1 T hT hTB δ hδ hchild k hk nextEll hnext hnext1)
:
(tsupport fun (x : EulerSmoothLimit.Space) =>
(state β hβ ell hell hell1 T hT hTB δ hδ hchild k hk nextEll hnext hnext1 F).evolution.velocity (0, x)) ⊆
Metric.closedBall 0 2
theorem
EulerBaseDatum.FirstPacketChoice.initial_compact
{β : ℝ}
{hβ : |β| ≤ 1}
{ell : ℝ}
{hell : 0 < ell}
{hell1 : ell ≤ 1}
{T : ℝ}
{hT : 0 < T}
{hTB : T ≤ initialTime}
{δ : ℝ}
{hδ : 0 < δ}
{hchild k : ℝ}
{hk : EulerPacketSourceFrequency.UniversalFrequency k}
{nextEll : ℝ}
{hnext : 0 < nextEll}
{hnext1 : nextEll ≤ 1}
(F : FirstPacketChoice β hβ ell hell hell1 T hT hTB δ hδ hchild k hk nextEll hnext hnext1)
:
HasCompactSupport fun (x : EulerSmoothLimit.Space) =>
(state β hβ ell hell hell1 T hT hTB δ hδ hchild k hk nextEll hnext hnext1 F).evolution.velocity (0, x)
theorem
EulerPacketInductionScales.Scales.firstStage_initial_support
{c B : ℝ}
(S : Scales c B)
:
(tsupport fun (x : EulerSmoothLimit.Space) => S.firstStage.state.evolution.velocity (0, x)) ⊆ Metric.closedBall 0 2
theorem
EulerPacketInductionScales.Scales.firstStage_initial_compact
{c B : ℝ}
(S : Scales c B)
:
HasCompactSupport fun (x : EulerSmoothLimit.Space) => S.firstStage.state.evolution.velocity (0, x)
theorem
EulerPacketInductionScales.Scales.firstStage_initial_field_support
{c B : ℝ}
(S : Scales c B)
: