The literal base horizon and core radius satisfy the local-existence and localized coercivity guards after the final choice of the base scale.

noncomputable def EulerPacketBaseGuardScales.baseHorizon (J : ℕ) (X : ℝ) : ℝ

Base horizon, given by 6*(J : ℝ)^2*X^(-498 : ℝ).

Equations

• EulerPacketBaseGuardScales.baseHorizon J X = 6 * ↑J ^ 2 * X ^ (-498)

noncomputable def EulerPacketBaseGuardScales.baseRadius (X : ℝ) : ℝ

Base radius, given by X^(-1000 : ℝ).

Equations

• EulerPacketBaseGuardScales.baseRadius X = X ^ (-1000)

noncomputable def EulerPacketBaseGuardScales.baseGuardCost (J : ℕ) (K Be CM Cboundary X : ℝ) : ℝ

Base guard cost, given by K*(baseHorizon J X^2/2)+Be*baseHorizon J X + Cboundary*(CM*X^1000+2)*baseRadius X^3*baseHorizon J X.

Equations

• One or more equations did not get rendered due to their size.

theorem EulerPacketBaseGuardScales.baseHorizon_pos (J : ℕ) (hJ : 1 ≤ J) {X : ℝ} (hX : 0 < X) : 0 < baseHorizon J X

theorem EulerPacketBaseGuardScales.baseRadius_pos {X : ℝ} (hX : 0 < X) : 0 < baseRadius X

theorem EulerPacketBaseGuardScales.baseHorizon_eq_timeWidth (J : ℕ) {X : ℝ} (hX : 0 < X) : baseHorizon J X = 2 * EulerPacketSourceScaleSequence.timeWidth J X 0

theorem EulerPacketBaseGuardScales.baseHorizon_tendsto_zero (J : ℕ) : Filter.Tendsto (baseHorizon J) Filter.atTop (nhds 0)

theorem EulerPacketBaseGuardScales.baseRadius_tendsto_zero : Filter.Tendsto baseRadius Filter.atTop (nhds 0)

theorem EulerPacketBaseGuardScales.baseGuardCost_tendsto_zero (J : ℕ) (K Be CM Cboundary : ℝ) : Filter.Tendsto (baseGuardCost J K Be CM Cboundary) Filter.atTop (nhds 0)

theorem EulerPacketBaseGuardScales.eventually_base_guards (J : ℕ) (hJ : 1 ≤ J) (K Be CM Cboundary T₀ : ℝ) (hT₀ : 0 < T₀) : ∀ᶠ (X : ℝ) in Filter.atTop, 1 < X ∧ 0 < baseHorizon J X ∧ baseHorizon J X ≤ T₀ ∧ 0 < baseRadius X ∧ baseRadius X ≤ 1 / 4 ∧ baseGuardCost J K Be CM Cboundary X ≤ 1 / 2