The literal activation times and nested horizons in (38). The same positive initial time interval is available to every finite packet state.

noncomputable def EulerPacketNestedHorizons.stepLength (J : ℕ) (X : ℝ) (a β : ℕ → ℝ) (n : ℕ) : ℝ

Step length, given by scaleSequence J X (n+1)/sqrt (β n*a n*previousShear J X n).

Equations

• EulerPacketNestedHorizons.stepLength J X a β n = EulerPacketSourceScaleChoice.scaleSequence J X (n + 1) / √(β n * a n * EulerPacketSourceScaleSequence.previousShear J X n)

noncomputable def EulerPacketNestedHorizons.activationTime (J : ℕ) (X : ℝ) (a β : ℕ → ℝ) (n : ℕ) : ℝ

Activation time, given by ∑ i ∈ range n, stepLength J X a β i.

Equations

• EulerPacketNestedHorizons.activationTime J X a β n = ∑ i ∈ Finset.range n, EulerPacketNestedHorizons.stepLength J X a β i

noncomputable def EulerPacketNestedHorizons.horizonTime (J : ℕ) (X : ℝ) (a β : ℕ → ℝ) (n : ℕ) : ℝ

Horizon time, given by activationTime J X a β n+2*timeWidth J X n.

Equations

• EulerPacketNestedHorizons.horizonTime J X a β n = EulerPacketNestedHorizons.activationTime J X a β n + 2 * EulerPacketSourceScaleSequence.timeWidth J X n

@[simp]

theorem EulerPacketNestedHorizons.activationTime_zero (J : ℕ) (X : ℝ) (a β : ℕ → ℝ) : activationTime J X a β 0 = 0

theorem EulerPacketNestedHorizons.activationTime_succ (J : ℕ) (X : ℝ) (a β : ℕ → ℝ) (n : ℕ) : activationTime J X a β (n + 1) = activationTime J X a β n + stepLength J X a β n

@[simp]

theorem EulerPacketNestedHorizons.horizonTime_zero (J : ℕ) {X : ℝ} (hX : 0 < X) (a β : ℕ → ℝ) : horizonTime J X a β 0 = EulerPacketBaseGuardScales.baseHorizon J X

theorem EulerPacketNestedHorizons.stepLength_bounds (J : ℕ) (hJ : 1 ≤ J) (X : ℝ) (hX : 0 < X) (a β : ℕ → ℝ) (ha : ∀ (n : ℕ), 1 / 2 ≤ a n) (ha₂ : ∀ (n : ℕ), a n ≤ 2) (hβ : ∀ (n : ℕ), 1 / 2 ≤ β n * EulerPacketSourceScaleChoice.scaleSequence J X n ^ 2) (hβ₂ : ∀ (n : ℕ), β n * EulerPacketSourceScaleChoice.scaleSequence J X n ^ 2 ≤ 2) (n : ℕ) : EulerPacketSourceScaleSequence.timeWidth J X n / 6 ≤ stepLength J X a β n ∧ stepLength J X a β n ≤ 2 * EulerPacketSourceScaleSequence.timeWidth J X n / 3

theorem EulerPacketNestedHorizons.stepLength_pos (J : ℕ) (hJ : 1 ≤ J) (X : ℝ) (hX : 0 < X) (a β : ℕ → ℝ) (ha : ∀ (n : ℕ), 1 / 2 ≤ a n) (ha₂ : ∀ (n : ℕ), a n ≤ 2) (hβ : ∀ (n : ℕ), 1 / 2 ≤ β n * EulerPacketSourceScaleChoice.scaleSequence J X n ^ 2) (hβ₂ : ∀ (n : ℕ), β n * EulerPacketSourceScaleChoice.scaleSequence J X n ^ 2 ≤ 2) (n : ℕ) : 0 < stepLength J X a β n

theorem EulerPacketNestedHorizons.activationTime_strictMono (J : ℕ) (hJ : 1 ≤ J) (X : ℝ) (hX : 0 < X) (a β : ℕ → ℝ) (ha : ∀ (n : ℕ), 1 / 2 ≤ a n) (ha₂ : ∀ (n : ℕ), a n ≤ 2) (hβ : ∀ (n : ℕ), 1 / 2 ≤ β n * EulerPacketSourceScaleChoice.scaleSequence J X n ^ 2) (hβ₂ : ∀ (n : ℕ), β n * EulerPacketSourceScaleChoice.scaleSequence J X n ^ 2 ≤ 2) : StrictMono (activationTime J X a β)

theorem EulerPacketNestedHorizons.activationTime_nonneg (J : ℕ) (hJ : 1 ≤ J) (X : ℝ) (hX : 0 < X) (a β : ℕ → ℝ) (ha : ∀ (n : ℕ), 1 / 2 ≤ a n) (ha₂ : ∀ (n : ℕ), a n ≤ 2) (hβ : ∀ (n : ℕ), 1 / 2 ≤ β n * EulerPacketSourceScaleChoice.scaleSequence J X n ^ 2) (hβ₂ : ∀ (n : ℕ), β n * EulerPacketSourceScaleChoice.scaleSequence J X n ^ 2 ≤ 2) (n : ℕ) : 0 ≤ activationTime J X a β n

theorem EulerPacketNestedHorizons.activationTime_pos (J : ℕ) (hJ : 1 ≤ J) (X : ℝ) (hX : 0 < X) (a β : ℕ → ℝ) (ha : ∀ (n : ℕ), 1 / 2 ≤ a n) (ha₂ : ∀ (n : ℕ), a n ≤ 2) (hβ : ∀ (n : ℕ), 1 / 2 ≤ β n * EulerPacketSourceScaleChoice.scaleSequence J X n ^ 2) (hβ₂ : ∀ (n : ℕ), β n * EulerPacketSourceScaleChoice.scaleSequence J X n ^ 2 ≤ 2) {n : ℕ} (hn : 0 < n) : 0 < activationTime J X a β n

theorem EulerPacketNestedHorizons.horizonTime_pos (J : ℕ) (hJ : 1 ≤ J) (X : ℝ) (hX : 0 < X) (a β : ℕ → ℝ) (ha : ∀ (n : ℕ), 1 / 2 ≤ a n) (ha₂ : ∀ (n : ℕ), a n ≤ 2) (hβ : ∀ (n : ℕ), 1 / 2 ≤ β n * EulerPacketSourceScaleChoice.scaleSequence J X n ^ 2) (hβ₂ : ∀ (n : ℕ), β n * EulerPacketSourceScaleChoice.scaleSequence J X n ^ 2 ≤ 2) (n : ℕ) : 0 < horizonTime J X a β n

theorem EulerPacketNestedHorizons.activationTime_lt_horizon (J : ℕ) (hJ : 1 ≤ J) (X : ℝ) (hX : 0 < X) (a β : ℕ → ℝ) (n : ℕ) : activationTime J X a β n < horizonTime J X a β n

theorem EulerPacketNestedHorizons.horizonTime_succ_le (J : ℕ) (hJ : 1 ≤ J) (X : ℝ) (hX : 0 < X) (a β : ℕ → ℝ) (ha : ∀ (n : ℕ), 1 / 2 ≤ a n) (ha₂ : ∀ (n : ℕ), a n ≤ 2) (hβ : ∀ (n : ℕ), 1 / 2 ≤ β n * EulerPacketSourceScaleChoice.scaleSequence J X n ^ 2) (hβ₂ : ∀ (n : ℕ), β n * EulerPacketSourceScaleChoice.scaleSequence J X n ^ 2 ≤ 2) (n : ℕ) (hw : EulerPacketSourceScaleSequence.timeWidth J X (n + 1) ≤ EulerPacketSourceScaleSequence.timeWidth J X n / 2) : horizonTime J X a β (n + 1) ≤ horizonTime J X a β n

theorem EulerPacketNestedHorizons.horizonTime_antitone (J : ℕ) (hJ : 1 ≤ J) (X : ℝ) (hX : 0 < X) (a β : ℕ → ℝ) (ha : ∀ (n : ℕ), 1 / 2 ≤ a n) (ha₂ : ∀ (n : ℕ), a n ≤ 2) (hβ : ∀ (n : ℕ), 1 / 2 ≤ β n * EulerPacketSourceScaleChoice.scaleSequence J X n ^ 2) (hβ₂ : ∀ (n : ℕ), β n * EulerPacketSourceScaleChoice.scaleSequence J X n ^ 2 ≤ 2) (hw : ∀ (n : ℕ), EulerPacketSourceScaleSequence.timeWidth J X (n + 1) ≤ EulerPacketSourceScaleSequence.timeWidth J X n / 2) : Antitone (horizonTime J X a β)

theorem EulerPacketNestedHorizons.horizonTime_le_base (J : ℕ) (hJ : 1 ≤ J) (X : ℝ) (hX : 0 < X) (a β : ℕ → ℝ) (ha : ∀ (n : ℕ), 1 / 2 ≤ a n) (ha₂ : ∀ (n : ℕ), a n ≤ 2) (hβ : ∀ (n : ℕ), 1 / 2 ≤ β n * EulerPacketSourceScaleChoice.scaleSequence J X n ^ 2) (hβ₂ : ∀ (n : ℕ), β n * EulerPacketSourceScaleChoice.scaleSequence J X n ^ 2 ≤ 2) (hw : ∀ (n : ℕ), EulerPacketSourceScaleSequence.timeWidth J X (n + 1) ≤ EulerPacketSourceScaleSequence.timeWidth J X n / 2) (n : ℕ) : horizonTime J X a β n ≤ EulerPacketBaseGuardScales.baseHorizon J X

theorem EulerPacketNestedHorizons.activationTime_lower (J : ℕ) (hJ : 1 ≤ J) (X : ℝ) (hX : 0 < X) (a β : ℕ → ℝ) (ha : ∀ (n : ℕ), 1 / 2 ≤ a n) (ha₂ : ∀ (n : ℕ), a n ≤ 2) (hβ : ∀ (n : ℕ), 1 / 2 ≤ β n * EulerPacketSourceScaleChoice.scaleSequence J X n ^ 2) (hβ₂ : ∀ (n : ℕ), β n * EulerPacketSourceScaleChoice.scaleSequence J X n ^ 2 ≤ 2) {n : ℕ} (hn : 1 ≤ n) : EulerPacketBaseGuardScales.baseHorizon J X / 12 ≤ activationTime J X a β n

theorem EulerPacketNestedHorizons.common_positive_interval (J : ℕ) (hJ : 1 ≤ J) (X : ℝ) (hX : 0 < X) (a β : ℕ → ℝ) (ha : ∀ (n : ℕ), 1 / 2 ≤ a n) (ha₂ : ∀ (n : ℕ), a n ≤ 2) (hβ : ∀ (n : ℕ), 1 / 2 ≤ β n * EulerPacketSourceScaleChoice.scaleSequence J X n ^ 2) (hβ₂ : ∀ (n : ℕ), β n * EulerPacketSourceScaleChoice.scaleSequence J X n ^ 2 ≤ 2) (n : ℕ) : EulerPacketBaseGuardScales.baseHorizon J X / 12 < horizonTime J X a β n

theorem EulerPacketNestedHorizons.reciprocal_horizon_le (J : ℕ) (hJ : 1 ≤ J) (X : ℝ) (hX : 0 < X) (a β : ℕ → ℝ) (ha : ∀ (n : ℕ), 1 / 2 ≤ a n) (ha₂ : ∀ (n : ℕ), a n ≤ 2) (hβ : ∀ (n : ℕ), 1 / 2 ≤ β n * EulerPacketSourceScaleChoice.scaleSequence J X n ^ 2) (hβ₂ : ∀ (n : ℕ), β n * EulerPacketSourceScaleChoice.scaleSequence J X n ^ 2 ≤ 2) (n : ℕ) : (horizonTime J X a β n)⁻¹ ≤ 12 / EulerPacketBaseGuardScales.baseHorizon J X

theorem EulerPacketNestedHorizons.reciprocal_activation_le (J : ℕ) (hJ : 1 ≤ J) (X : ℝ) (hX : 0 < X) (a β : ℕ → ℝ) (ha : ∀ (n : ℕ), 1 / 2 ≤ a n) (ha₂ : ∀ (n : ℕ), a n ≤ 2) (hβ : ∀ (n : ℕ), 1 / 2 ≤ β n * EulerPacketSourceScaleChoice.scaleSequence J X n ^ 2) (hβ₂ : ∀ (n : ℕ), β n * EulerPacketSourceScaleChoice.scaleSequence J X n ^ 2 ≤ 2) {n : ℕ} (hn : 1 ≤ n) : (activationTime J X a β n)⁻¹ ≤ 12 / EulerPacketBaseGuardScales.baseHorizon J X