Elementary bounds for the literal source parameters in (39). Polynomial factors include the growing base core constant and inverse time; no parameter depending on the base scale is treated as fixed.

noncomputable def EulerPacketSourceParameterScales.predecessorExponent (J : ℕ) (X : ℝ) (n : ℕ) : ℝ

Predecessor exponent, given by scaleSequence J X n/((J-1+n : ℕ) : ℝ)^3.

Equations

• EulerPacketSourceParameterScales.predecessorExponent J X n = EulerPacketSourceScaleChoice.scaleSequence J X n / ↑(J - 1 + n) ^ 3

def EulerPacketSourceParameterScales.polynomialFactor (J : ℕ) (X : ℝ) (n : ℕ) : ℝ

Polynomial factor, given by ((J+n : ℕ) : ℝ)^20*(scaleSequence J X n)^1000.

Equations

• EulerPacketSourceParameterScales.polynomialFactor J X n = ↑(J + n) ^ 20 * EulerPacketSourceScaleChoice.scaleSequence J X n ^ 1000

theorem EulerPacketSourceParameterScales.sequence_one_le (J : ℕ) (hJ : 1 ≤ J) (X : ℝ) (hX : 1 ≤ X) (n : ℕ) : 1 ≤ EulerPacketSourceScaleChoice.scaleSequence J X n

theorem EulerPacketSourceParameterScales.sequence_initial_le (J : ℕ) (hJ : 1 ≤ J) (X : ℝ) (hX : 0 ≤ X) (n : ℕ) : X ≤ EulerPacketSourceScaleChoice.scaleSequence J X n

theorem EulerPacketSourceParameterScales.predecessorExponent_nonneg (J : ℕ) (hJ : 1 ≤ J) (X : ℝ) (hX : 1 ≤ X) (n : ℕ) : 0 ≤ predecessorExponent J X n

theorem EulerPacketSourceParameterScales.exponential_one_le (J : ℕ) (hJ : 1 ≤ J) (X c : ℝ) (hX : 1 ≤ X) (hc : 0 ≤ c) (n : ℕ) : 1 ≤ Real.exp (c * predecessorExponent J X n)

theorem EulerPacketSourceParameterScales.polynomialFactor_one (J : ℕ) (hJ : 1 ≤ J) (X : ℝ) (hX : 1 ≤ X) (n : ℕ) : 1 ≤ polynomialFactor J X n

theorem EulerPacketSourceParameterScales.monomial_le_polynomialFactor (J : ℕ) (hJ : 1 ≤ J) (X : ℝ) (hX : 1 ≤ X) (n p q : ℕ) (hp : p ≤ 20) (hq : q ≤ 1000) : ↑(J + n) ^ p * EulerPacketSourceScaleChoice.scaleSequence J X n ^ q ≤ polynomialFactor J X n

theorem EulerPacketSourceParameterScales.predecessor_power_le (J : ℕ) (hJ : 2 ≤ J) (X : ℝ) (hX : 1 ≤ X) (n p : ℕ) (hp : 3 ≤ p) : EulerPacketSourceScaleChoice.scaleSequence J X n / ↑(J - 1 + n) ^ p ≤ predecessorExponent J X n

theorem EulerPacketSourceParameterScales.current_power_le (J : ℕ) (hJ : 2 ≤ J) (X : ℝ) (hX : 1 ≤ X) (n p : ℕ) (hp : 3 ≤ p) : EulerPacketSourceScaleChoice.scaleSequence J X n / ↑(J + n) ^ p ≤ predecessorExponent J X n

theorem EulerPacketSourceParameterScales.previousFrequency_power_le (J D : ℕ) (hJ : 2 ≤ J) (X c : ℝ) (hX : 1 ≤ X) (hc : 0 ≤ c) (hbase : X ^ D ≤ Real.exp (X / ↑(J - 1) ^ 4)) (n : ℕ) : EulerPacketSourceScaleSequence.previousFrequency J D X n ^ c ≤ Real.exp (c * predecessorExponent J X n)

theorem EulerPacketSourceParameterScales.previousShear_le_exponential (J : ℕ) (hJ : 2 ≤ J) (X : ℝ) (hX : 1 ≤ X) (hbase : X ^ 1000 ≤ Real.exp (X / ↑(J - 1) ^ 7)) (n : ℕ) : EulerPacketSourceScaleSequence.previousShear J X n ≤ Real.exp (predecessorExponent J X n)

theorem EulerPacketSourceParameterScales.shear_le_exponential (J : ℕ) (hJ : 2 ≤ J) (X : ℝ) (hX : 1 ≤ X) (n : ℕ) : EulerPacketSourceScaleSequence.shear J X n ≤ Real.exp (predecessorExponent J X n)

theorem EulerPacketSourceParameterScales.spike_inverse_le_exponential (J : ℕ) (hJ : 2 ≤ J) (X : ℝ) (hX : 1 ≤ X) (n : ℕ) : (EulerPacketSourceScaleSequence.spike J X n)⁻¹ ≤ Real.exp (predecessorExponent J X n)

theorem EulerPacketSourceParameterScales.base_inverse_time_le (J : ℕ) (hJ : 1 ≤ J) (X : ℝ) (hX : 1 ≤ X) : 12 / EulerPacketBaseGuardScales.baseHorizon J X ≤ 2 * X ^ 1000

theorem EulerPacketSourceParameterScales.inverse_time_le_factor (J : ℕ) (hJ : 1 ≤ J) (X : ℝ) (hX : 1 ≤ X) (n : ℕ) : 12 / EulerPacketBaseGuardScales.baseHorizon J X ≤ 2 * polynomialFactor J X n