The limiting initial datum of the actual recursive packet family. Its genuine Euler solutions have a positive, finite maximal horizon.

An actual stage family with convergent initial data has a genuine positive-time Euler solution for its limiting datum. Only the already proved common packet interval and actual stability are used.

theorem EulerOrdinarySobolev.tensorNorm_sub_triangle (A B C : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (s : ℕ) : tensorNorm s (fieldSub A B) ≤ tensorNorm s (fieldSub A C) + tensorNorm s (fieldSub B C)

theorem EulerPacketInduction.Stage.exists_local_evolution {c B : ℝ} {S : EulerPacketInductionScales.Scales c B} (P : (n : ℕ) → Stage S n) (u₀ : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (hinit : ∀ (q : ℕ), Filter.Tendsto (fun (n : ℕ) => EulerPhysicalL2Scaling.derivativeSum q ((fun (x : EulerSmoothLimit.Space) => (P n).state.evolution.velocity (0, x)) - u₀.field)) Filter.atTop (nhds 0)) : ∃ (L : ℝ) (hL : 0 < L), L ≤ EulerPacketBaseGuardScales.baseHorizon S.J S.X / 12 ∧ ∃ (E : EulerOrdinarySobolev.Evolution L ⋯), (E.velocity ⟨0, ⋯⟩).field = u₀.field

noncomputable def EulerPacketInduction.initialDatum : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space

Initial datum, given by Stage.initialDataLimit packets le_rfl le_rfl.

Equations

• EulerPacketInduction.initialDatum = EulerPacketInduction.Stage.initialDataLimit EulerPacketInduction.packets ⋯ EulerPacketInduction.initialDatum._proof_1

theorem EulerPacketInduction.initialDatum_Hm (s : ℕ) : Filter.Tendsto (fun (n : ℕ) => EulerPhysicalL2Scaling.derivativeSum s ((fun (x : EulerSmoothLimit.Space) => (packets n).state.evolution.velocity (0, x)) - initialDatum.field)) Filter.atTop (nhds 0)

theorem EulerPacketInduction.initialDatum_local : ∃ (T : ℝ), EulerOrdinarySobolev.HasEulerEvolution initialDatum T

theorem EulerPacketInduction.initialDatum_no_base : ¬EulerOrdinarySobolev.HasEulerEvolution initialDatum (EulerPacketBaseGuardScales.baseHorizon constructionScales.J constructionScales.X)

theorem EulerPacketInduction.initialDatum_solenoidal : initialDatum.toLp ∈ EulerMeanSolenoidal.solenoidalSpace

theorem EulerPacketInduction.initialDatum_divergence (x : EulerSmoothLimit.Space) : EulerSmoothLimit.divergence initialDatum.field x = 0

theorem EulerPacketInduction.initialDatum_finite_lifespan : ∃ (L : EulerOrdinarySobolev.FiniteLifespan initialDatum), L.duration ≤ EulerPacketBaseGuardScales.baseHorizon constructionScales.J constructionScales.X

noncomputable def EulerPacketInduction.lifespan : EulerOrdinarySobolev.FiniteLifespan initialDatum

Lifespan, given by initialDatum_finite_lifespan.choose.

Equations

• EulerPacketInduction.lifespan = EulerPacketInduction.initialDatum_finite_lifespan.choose

theorem EulerPacketInduction.lifespan_le_base : lifespan.duration ≤ EulerPacketBaseGuardScales.baseHorizon constructionScales.J constructionScales.X