The literal sequences in (37), including the polynomial initial shear and frequency. Their first two exceptional stages are retained explicitly.

Pointwise bounds for the literal scale expressions in (37)--(39). They exhibit a finite list of exponential costs to which the existing uniform scale-choice theorem applies. The estimates here contain no field data.

Packet Source Scales

noncomputable def EulerPacketSourceScales.sourceTheta (J : ℕ) (C : ℝ) (x : ℕ → ℝ) (n : ℕ) : ℝ

A fixed polynomial majorant for the dimensionless stage horizon.

Equations

• EulerPacketSourceScales.sourceTheta J C x n = C * (1 + ↑(J + n) ^ 2 * x n ^ 2)

noncomputable def EulerPacketSourceScales.sourceEpsilon (J : ℕ) (x : ℕ → ℝ) (n : ℕ) : ℝ

The source upper bound for the square-root inverse parent shear.

Equations

• EulerPacketSourceScales.sourceEpsilon J x n = 2 * Real.exp (-x n / (2 * ↑(J - 1 + n) ^ 7))

noncomputable def EulerPacketSourceScales.sourceOlderGradient (J : ℕ) (x : ℕ → ℝ) (n : ℕ) : ℝ

The older gradient bound expressed using the quadratic recurrence.

Equations

• EulerPacketSourceScales.sourceOlderGradient J x n = 1 + Real.exp (x n / (↑(J - 1 + n) ^ 2 * ↑(J - 2 + n) ^ 7))

noncomputable def EulerPacketSourceScales.sourcePriorError (J : ℕ) (x : ℕ → ℝ) (n : ℕ) : ℝ

The inverse fourth root of the preceding packet frequency.

Equations

• EulerPacketSourceScales.sourcePriorError J x n = Real.exp (-x n / (4 * ↑(J - 1 + n) ^ 4))

noncomputable def EulerPacketSourceScales.sourceNeighborError (J : ℕ) (c : ℝ) (x : ℕ → ℝ) (n : ℕ) : ℝ

The neighbor error with the support, frequency, and shear scales of (37).

Equations

• EulerPacketSourceScales.sourceNeighborError J c x n = Real.exp (-x n / ↑(J + n) ^ (7 / 2) + c * x n / ↑(J - 1 + n) ^ 4 + c * x n / ↑(J - 1 + n) ^ 7)

noncomputable def EulerPacketSourceScales.sourceCoefficientError (J : ℕ) (C c : ℝ) (x : ℕ → ℝ) (n : ℕ) : ℝ

The full coefficient error entering the normalized ray and velocity equations.

Equations

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

theorem EulerPacketSourceScales.sourceTheta_bounds {J : ℕ} (hJ : 1 ≤ J) {C : ℝ} (hC : 1 ≤ C) {x : ℕ → ℝ} (hx : ∀ (n : ℕ), 1 ≤ x n) (n : ℕ) : 1 ≤ sourceTheta J C x n ∧ sourceTheta J C x n ≤ 2 * C * ↑(J + n) ^ 2 * x n ^ 2

The horizon majorant is bounded by a single monomial.

theorem EulerPacketSourceScales.polynomial_source_scale_summable (J d B : ℕ) (hJ : d < J) (x : ℕ → ℝ) (hx0 : 0 < x 0) (hx : ∀ (n : ℕ), x (n + 1) = ↑(J + n) ^ 2 * x n) (A b c C : ℝ) (p q : ℕ) (hA : 0 ≤ A) (hAB : A < ↑B) (hb : 0 < b) (hC : 0 < C) : Summable fun (n : ℕ) => C * ↑(J + n) ^ p * x n ^ q * Real.exp (-b * (x n / ↑(J + n) ^ A) + c * (x n / ↑(J - d + n) ^ B))

The explicit logarithmic scale comparison also allows an arbitrary fixed polynomial prefactor.

theorem EulerPacketSourceScales.source_neighbor_error_summable (J : ℕ) (hJ : 3 ≤ J) (x : ℕ → ℝ) (hx0 : 1 ≤ x 0) (hx : ∀ (n : ℕ), x (n + 1) = ↑(J + n) ^ 2 * x n) (C c : ℝ) (hC : 1 ≤ C) (hc : 0 ≤ c) (A : ℕ) : Summable fun (n : ℕ) => sourceNeighborError J c x n * sourceTheta J C x n ^ A

Every polynomially weighted neighbor error in (25) is summable.

theorem EulerPacketSourceScales.theta_weighted_source_exponential_summable (J d B : ℕ) (hJ : d < J) (x : ℕ → ℝ) (hx0 : 1 ≤ x 0) (hx : ∀ (n : ℕ), x (n + 1) = ↑(J + n) ^ 2 * x n) (C a b c : ℝ) (hC : 1 ≤ C) (ha : 0 ≤ a) (haB : a < ↑B) (hb : 0 < b) (A : ℕ) : Summable fun (n : ℕ) => sourceTheta J C x n ^ A * Real.exp (-b * (x n / ↑(J + n) ^ a) + c * (x n / ↑(J - d + n) ^ B))

Multiplying any decaying source exponential by a fixed horizon power preserves summability.

theorem EulerPacketSourceScales.source_prior_error_summable (J : ℕ) (hJ : 3 ≤ J) (x : ℕ → ℝ) (hx0 : 1 ≤ x 0) (hx : ∀ (n : ℕ), x (n + 1) = ↑(J + n) ^ 2 * x n) (C : ℝ) (hC : 1 ≤ C) (A : ℕ) : Summable fun (n : ℕ) => sourcePriorError J x n * sourceTheta J C x n ^ A

The parent-frequency error is summable with every horizon power.

theorem EulerPacketSourceScales.source_shear_gradient_bound (J : ℕ) (hJ : 3 ≤ J) (x : ℕ → ℝ) (hx : ∀ (n : ℕ), 0 ≤ x n) (n : ℕ) : sourceEpsilon J x n * sourceOlderGradient J x n ^ 2 ≤ 8 * Real.exp (-(1 / 2) * (x n / ↑(J + n) ^ 7) + 2 * (x n / ↑(J - 2 + n) ^ 9))

The source shear/older-gradient product has an explicit decaying exponential majorant at every normal stage after the two base exceptions.

theorem EulerPacketSourceScales.source_shear_error_summable (J : ℕ) (hJ : 3 ≤ J) (x : ℕ → ℝ) (hx0 : 1 ≤ x 0) (hx : ∀ (n : ℕ), x (n + 1) = ↑(J + n) ^ 2 * x n) (C : ℝ) (hC : 1 ≤ C) (A : ℕ) : Summable fun (n : ℕ) => sourceEpsilon J x n * sourceTheta J C x n * sourceOlderGradient J x n ^ 2 * sourceTheta J C x n ^ A

The change of the parent shear and older coefficients obeys every polynomial smallness regime required by the ray analysis.

theorem EulerPacketSourceScales.source_coefficient_error_summable (J : ℕ) (hJ : 3 ≤ J) (x : ℕ → ℝ) (hx0 : 1 ≤ x 0) (hx : ∀ (n : ℕ), x (n + 1) = ↑(J + n) ^ 2 * x n) (C c : ℝ) (hC : 1 ≤ C) (hc : 0 ≤ c) (A : ℕ) : Summable fun (n : ℕ) => sourceCoefficientError J C c x n * sourceTheta J C x n ^ A

The complete error specified by the logarithmic scales is summable after multiplication by any fixed horizon power.

theorem EulerPacketSourceScales.source_coefficient_error_eventually_small (J : ℕ) (hJ : 3 ≤ J) (x : ℕ → ℝ) (hx0 : 1 ≤ x 0) (hx : ∀ (n : ℕ), x (n + 1) = ↑(J + n) ^ 2 * x n) (C c K : ℝ) (hC : 1 ≤ C) (hc : 0 ≤ c) : ∀ᶠ (n : ℕ) in Filter.atTop, 1000000 * K * sourceCoefficientError J C c x n * sourceTheta J C x n ^ 40 ≤ 1

In particular the actual source scales eventually satisfy the quantitative Θ^40 guard needed by the complete ODE frame analysis.

Packet Source Time

theorem EulerPacketSourceTime.preceding_scale_identities {p q x X Y : ℝ} (hp : p ≠ 0) (hq : q ≠ 0) (hx : x = p ^ 2 * X) (hX : X = q ^ 2 * Y) : X / p ^ 5 = x / p ^ 7 ∧ Y / q ^ 5 = x / (p ^ 2 * q ^ 7)

The preceding two shear logarithms are exactly those obtained by substituting the quadratic recurrence into (37).

theorem EulerPacketSourceTime.epsilon_of_shear_bound {a L : ℝ} (ha : 0 ≤ a) (ha₂ : a ≤ 2) : √(a / Real.exp L) ≤ 2 * Real.exp (-L / 2)

A frame normalization a≤2 gives the explicit source epsilon bound.

noncomputable def EulerPacketSourceTime.sourceTimeWidth (J : ℕ) (x : ℕ → ℝ) (n : ℕ) : ℝ

The current time width in (37), after exact substitution of the scales.

Equations

• EulerPacketSourceTime.sourceTimeWidth J x n = 3 * ↑(J + n) ^ 2 * x n ^ 2 * Real.exp (-x n / (2 * ↑(J - 1 + n) ^ 7))

noncomputable def EulerPacketSourceTime.sourceNextTimeWidth (J : ℕ) (x : ℕ → ℝ) (n : ℕ) : ℝ

The following time width, using x_j=j²x_{j-1} twice.

Equations

• EulerPacketSourceTime.sourceNextTimeWidth J x n = 3 * (↑(J + n) + 1) ^ 2 * ↑(J + n) ^ 4 * x n ^ 2 * Real.exp (-x n / (2 * ↑(J + n) ^ 5))

noncomputable def EulerPacketSourceTime.sourceTimeRatio (J : ℕ) (x : ℕ → ℝ) (n : ℕ) : ℝ

The exact quotient of consecutive time widths.

Equations

• EulerPacketSourceTime.sourceTimeRatio J x n = (↑(J + n) + 1) ^ 2 * ↑(J + n) ^ 2 * Real.exp (-x n / (2 * ↑(J + n) ^ 5) + x n / (2 * ↑(J - 1 + n) ^ 7))

theorem EulerPacketSourceTime.source_time_ratio_identity (J : ℕ) (x : ℕ → ℝ) (n : ℕ) : sourceNextTimeWidth J x n = sourceTimeRatio J x n * sourceTimeWidth J x n

Exact cancellation computes the consecutive time-width quotient.

theorem EulerPacketSourceTime.source_time_ratio_summable (J : ℕ) (hJ : 3 ≤ J) (x : ℕ → ℝ) (hx0 : 1 ≤ x 0) (hx : ∀ (n : ℕ), x (n + 1) = ↑(J + n) ^ 2 * x n) : Summable (sourceTimeRatio J x)

Consecutive time-width ratios are summable, so they tend to zero.

theorem EulerPacketSourceTime.source_time_width_eventually_contracts (J : ℕ) (hJ : 3 ≤ J) (x : ℕ → ℝ) (hx0 : 1 ≤ x 0) (hx : ∀ (n : ℕ), x (n + 1) = ↑(J + n) ^ 2 * x n) : ∀ᶠ (n : ℕ) in Filter.atTop, sourceNextTimeWidth J x n ≤ sourceTimeWidth J x n / 2

The actual next time width is eventually at most half of the current width.

theorem EulerPacketSourceTime.source_extra_time_bound (J : ℕ) (hJ : 1 ≤ J) (x : ℕ → ℝ) (n : ℕ) {a : ℝ} (ha : 0 ≤ a) (ha₂ : a ≤ 2) : 2 * √(a * Real.exp (x n / ↑(J - 1 + n) ^ 7)) * sourceNextTimeWidth J x n ≤ 48 * ↑(J + n) ^ 6 * x n ^ 2 * Real.exp (-(1 / 2) * (x n / ↑(J + n) ^ 5) + 1 / 2 * (x n / ↑(J - 1 + n) ^ 7))

The extra normalized horizon length has the explicit polynomial/exponential bound asserted after (39).

theorem EulerPacketSourceTime.source_extra_time_summable (J : ℕ) (hJ : 3 ≤ J) (x : ℕ → ℝ) (hx0 : 1 ≤ x 0) (hx : ∀ (n : ℕ), x (n + 1) = ↑(J + n) ^ 2 * x n) (C : ℝ) (hC : 1 ≤ C) (A : ℕ) (a : ℕ → ℝ) (ha : ∀ (n : ℕ), 0 ≤ a n) (ha₂ : ∀ (n : ℕ), a n ≤ 2) : Summable fun (n : ℕ) => 2 * √(a n * Real.exp (x n / ↑(J - 1 + n) ^ 7)) * sourceNextTimeWidth J x n * EulerPacketSourceScales.sourceTheta J C x n ^ A

Every horizon power times the extra normalized length is summable.

theorem EulerPacketSourceTime.source_parent_shear_square_ratio_summable (J : ℕ) (hJ : 3 ≤ J) (x : ℕ → ℝ) (hx0 : 1 ≤ x 0) (hx : ∀ (n : ℕ), x (n + 1) = ↑(J + n) ^ 2 * x n) : Summable fun (n : ℕ) => Real.exp (2 * x n / ↑(J - 1 + n) ^ 7) / Real.exp (x n / ↑(J + n) ^ 5)

The parent-shear square is negligible relative to the newly chosen shear.

theorem EulerPacketSourceTime.source_good_interval_cost_summable (J : ℕ) (hJ : 3 ≤ J) (x : ℕ → ℝ) (hx0 : 1 ≤ x 0) (hx : ∀ (n : ℕ), x (n + 1) = ↑(J + n) ^ 2 * x n) : Summable fun (n : ℕ) => Real.exp (-x n / ↑(J + n) ^ 3) * Real.exp (x n / ↑(J + n) ^ 5) * Real.exp (x n / ↑(J - 1 + n) ^ 7)

The good-interval pressure costs of the source are summable.

noncomputable def EulerPacketSourceScaleBounds.monomialCost (J d B : ℕ) (a b c C : ℝ) (p q : ℕ) (x : ℕ → ℝ) (n : ℕ) : ℝ

Monomial cost, given by C * ((J + n : ℕ) : ℝ)^p * (x n)^q * exp (-b * (x n / ((J + n : ℕ) : ℝ)^a) + c * (x n / ((J - d + n : ℕ) : ℝ)^B)).

Equations

• EulerPacketSourceScaleBounds.monomialCost J d B a b c C p q x n = C * ↑(J + n) ^ p * x n ^ q * Real.exp (-b * (x n / ↑(J + n) ^ a) + c * (x n / ↑(J - d + n) ^ B))

theorem EulerPacketSourceScaleBounds.monomialCost_nonneg (J d B : ℕ) (a b c C : ℝ) (p q : ℕ) (x : ℕ → ℝ) (n : ℕ) (hC : 0 ≤ C) (hx : 0 ≤ x n) : 0 ≤ monomialCost J d B a b c C p q x n

theorem EulerPacketSourceScaleBounds.monomialCost_eq_exp (J d B : ℕ) (a b c C : ℝ) (p q : ℕ) (x : ℕ → ℝ) (n : ℕ) (hJ : 1 ≤ J) (hC : 0 < C) (hx : 0 < x n) : monomialCost J d B a b c C p q x n = Real.exp (-b * (x n / ↑(J + n) ^ a) + c * (x n / ↑(J - d + n) ^ B) + Real.log C + ↑p * Real.log ↑(J + n) + ↑q * Real.log (x n))

theorem EulerPacketSourceScaleBounds.theta_weighted_monomial_bound (J d B : ℕ) (a b c D C : ℝ) (p q A : ℕ) (x : ℕ → ℝ) (n : ℕ) (hJ : 1 ≤ J) (hC : 1 ≤ C) (hD : 0 ≤ D) (hx : ∀ (n : ℕ), 1 ≤ x n) : monomialCost J d B a b c D p q x n * EulerPacketSourceScales.sourceTheta J C x n ^ A ≤ monomialCost J d B a b c (D * (2 * C) ^ A) (p + 2 * A) (q + 2 * A) x n

theorem EulerPacketSourceScaleBounds.sourcePriorError_bound (J : ℕ) (hJ : 3 ≤ J) (x : ℕ → ℝ) (n : ℕ) (hx : 0 ≤ x n) : EulerPacketSourceScales.sourcePriorError J x n ≤ Real.exp (-(1 / 4) * (x n / ↑(J + n) ^ 4))

theorem EulerPacketSourceScaleBounds.sourceNeighborError_bound (J : ℕ) (hJ : 3 ≤ J) (c : ℝ) (hc : 0 ≤ c) (x : ℕ → ℝ) (n : ℕ) (hx : 0 ≤ x n) : EulerPacketSourceScales.sourceNeighborError J c x n ≤ Real.exp (-(x n / ↑(J + n) ^ (7 / 2)) + 2 * c * (x n / ↑(J - 1 + n) ^ 4))

theorem EulerPacketSourceScaleBounds.sourceCoefficientError_bound (J : ℕ) (hJ : 3 ≤ J) (C c : ℝ) (hC : 1 ≤ C) (hc : 0 ≤ c) (A : ℕ) (x : ℕ → ℝ) (hx : ∀ (n : ℕ), 1 ≤ x n) (n : ℕ) : EulerPacketSourceScales.sourceCoefficientError J C c x n * EulerPacketSourceScales.sourceTheta J C x n ^ A ≤ monomialCost J 2 9 7 (1 / 2) 2 (128 * (2 * C) ^ (A + 1)) (2 * (A + 1)) (2 * (A + 1)) x n + monomialCost J 0 5 4 (1 / 4) 0 (16 * (2 * C) ^ A) (2 * A) (2 * A) x n + monomialCost J 1 4 (7 / 2) 1 (2 * c) (16 * (2 * C) ^ A) (2 * A) (2 * A) x n

The complete coefficient error is controlled by three explicit costs, with exactly the preceding-stage powers and the real support exponent 7/2.

theorem EulerPacketSourceScaleBounds.sourceExtraTime_bound (J : ℕ) (hJ : 1 ≤ J) (C : ℝ) (hC : 1 ≤ C) (A : ℕ) (x : ℕ → ℝ) (hx : ∀ (n : ℕ), 1 ≤ x n) (n : ℕ) (a : ℝ) (ha : 0 ≤ a) (ha₂ : a ≤ 2) : 2 * √(a * Real.exp (x n / ↑(J - 1 + n) ^ 7)) * EulerPacketSourceTime.sourceNextTimeWidth J x n * EulerPacketSourceScales.sourceTheta J C x n ^ A ≤ monomialCost J 1 7 5 (1 / 2) (1 / 2) (48 * (2 * C) ^ A) (6 + 2 * A) (2 + 2 * A) x n

theorem EulerPacketSourceScaleBounds.sourceTimeRatio_bound (J : ℕ) (hJ : 1 ≤ J) (x : ℕ → ℝ) (n : ℕ) : EulerPacketSourceTime.sourceTimeRatio J x n ≤ monomialCost J 1 7 5 (1 / 2) (1 / 2) 4 4 0 x n

theorem EulerPacketSourceScaleBounds.sourceParentSquareRatio_eq (J : ℕ) (x : ℕ → ℝ) (n : ℕ) : Real.exp (2 * x n / ↑(J - 1 + n) ^ 7) / Real.exp (x n / ↑(J + n) ^ 5) = monomialCost J 1 7 5 1 2 1 0 0 x n

theorem EulerPacketSourceScaleBounds.sourceGoodCost_bound (J : ℕ) (hJ : 3 ≤ J) (x : ℕ → ℝ) (n : ℕ) (hx : 0 ≤ x n) : Real.exp (-x n / ↑(J + n) ^ 3) * Real.exp (x n / ↑(J + n) ^ 5) * Real.exp (x n / ↑(J - 1 + n) ^ 7) ≤ monomialCost J 1 5 3 1 2 1 0 0 x n

A common choice of the starting stage and base scale for the concrete coefficient, time-width, and pressure costs in the outer construction.

Packet Uniform Scale Choice

Packet Uniform Log Bounds

theorem EulerPacketUniformLogBounds.polynomial_log_bound {j X C p q : ℝ} (hj : 1 ≤ j) (hX : 1 ≤ X) : C + p * Real.log j + q * Real.log X ≤ (|C| + |p| + 2 * |q|) * j * √X

Every fixed polynomial logarithm is bounded by a simple product of the stage and the square root of the scale.

theorem EulerPacketUniformLogBounds.polynomial_logs_uniformly_absorbed (J A : ℕ) (hJ : 1 ≤ J) (hJA : 2 ^ (2 * A + 3) ≤ ↑J ^ 2) (x : ℕ → ℝ) (hx0 : 1 ≤ x 0) (hx : ∀ (n : ℕ), x (n + 1) = ↑(J + n) ^ 2 * x n) (C p q b : ℝ) (hb : 0 < b) (hlarge : (2 * (|C| + |p| + 2 * |q|) / b) ^ 2 * ↑J ^ (2 * A + 2) ≤ x 0) (n : ℕ) : C + p * Real.log ↑(J + n) + q * Real.log (x n) ≤ b / 2 * (x n / ↑(J + n) ^ A)

A single explicit lower bound on the initial scale absorbs the polynomial logarithms at every subsequent quadratic stage.

theorem EulerPacketUniformScaleChoice.exists_uniform_stage_choice (d B N : ℕ) (a c b : ℝ) (haB : a < ↑B) (hb : 0 < b) : ∃ (J : ℕ), 3 ≤ J ∧ d < J ∧ 2 ^ (2 * N + 3) ≤ ↑J ^ 2 ∧ ∀ (n : ℕ), c * (↑(J + n) ^ a / ↑(J - d + n) ^ B) ≤ b / 4

One sufficiently large initial stage makes every predecessor-log coefficient small, uniformly over all subsequent stages.

theorem EulerPacketUniformScaleChoice.uniform_source_exponent_bound (J d B N : ℕ) (hJ : 1 ≤ J) (hdJ : d < J) (hJN : 2 ^ (2 * N + 3) ≤ ↑J ^ 2) (x : ℕ → ℝ) (hx0 : 1 ≤ x 0) (hx : ∀ (n : ℕ), x (n + 1) = ↑(J + n) ^ 2 * x n) (a b c C p q : ℝ) (haN : a ≤ ↑N) (hb : 0 < b) (hcoeff : ∀ (n : ℕ), c * (↑(J + n) ^ a / ↑(J - d + n) ^ B) ≤ b / 4) (hlarge : (4 * (|C| + |p| + 2 * |q|) / b) ^ 2 * ↑J ^ (2 * N + 2) ≤ x 0) (n : ℕ) : -b * (x n / ↑(J + n) ^ a) + c * (x n / ↑(J - d + n) ^ B) + C + p * Real.log ↑(J + n) + q * Real.log (x n) ≤ -(b / 2) * (x n / ↑(J + n) ^ N)

For a stage chosen above, one explicit lower bound on the initial scale controls all logarithmic scale errors at once.

theorem EulerPacketUniformScaleChoice.uniform_source_cost_tsum_bound (J d B N : ℕ) (hJ : 1 ≤ J) (hdJ : d < J) (hJN : 2 ^ (2 * N + 3) ≤ ↑J ^ 2) (x : ℕ → ℝ) (hx0 : 1 ≤ x 0) (hx : ∀ (n : ℕ), x (n + 1) = ↑(J + n) ^ 2 * x n) (a b c C p q : ℝ) (haN : a ≤ ↑N) (hb : 0 < b) (hcoeff : ∀ (n : ℕ), c * (↑(J + n) ^ a / ↑(J - d + n) ^ B) ≤ b / 4) (hlarge : (4 * (|C| + |p| + 2 * |q|) / b) ^ 2 * ↑J ^ (2 * N + 2) ≤ x 0) : ∑' (n : ℕ), Real.exp (-b * (x n / ↑(J + n) ^ a) + c * (x n / ↑(J - d + n) ^ B) + C + p * Real.log ↑(J + n) + q * Real.log (x n)) ≤ Real.exp (-(b / 2) * (x 0 / ↑J ^ N)) / (1 - Real.exp (-(b / 2) * (x 0 / ↑J ^ N)))

The complete logarithmic source cost has a uniform geometric-series bound after choosing the stage and then the initial scale.

theorem EulerPacketUniformScaleChoice.source_uniform_small_sum_choice (d B N : ℕ) (a b c C p q : ℝ) (haB : a < ↑B) (haN : a ≤ ↑N) (hb : 0 < b) : ∃ (J : ℕ), 3 ≤ J ∧ ∀ (δ : ℝ), 0 < δ → ∃ (X₀ : ℝ), 1 ≤ X₀ ∧ ∀ (x : ℕ → ℝ), X₀ ≤ x 0 → (∀ (n : ℕ), x (n + 1) = ↑(J + n) ^ 2 * x n) → ∑' (n : ℕ), Real.exp (-b * (x n / ↑(J + n) ^ a) + c * (x n / ↑(J - d + n) ^ B) + C + p * Real.log ↑(J + n) + q * Real.log (x n)) ≤ δ

The source's order of parameter choice is valid: first one chooses the stage J, then the base scale x₀, and the whole infinite sum is arbitrarily small. This includes the real support exponent 7/2.

Packet Finite Scale Choice

theorem EulerPacketFiniteScaleChoice.finite_source_uniform_small_sum_choice {ι : Type u_1} [Finite ι] (d B N : ι → ℕ) (a b c C p q : ι → ℝ) (haB : ∀ (i : ι), a i < ↑(B i)) (haN : ∀ (i : ι), a i ≤ ↑(N i)) (hb : ∀ (i : ι), 0 < b i) : ∃ (J : ℕ), 3 ≤ J ∧ ∀ (δ : ℝ), 0 < δ → ∃ (X₀ : ℝ), 1 ≤ X₀ ∧ ∀ (x : ℕ → ℝ), X₀ ≤ x 0 → (∀ (n : ℕ), x (n + 1) = ↑(J + n) ^ 2 * x n) → ∀ (i : ι), ∑' (n : ℕ), Real.exp (-b i * (x n / ↑(J + n) ^ a i) + c i * (x n / ↑(J - d i + n) ^ B i) + C i + p i * Real.log ↑(J + n) + q i * Real.log (x n)) ≤ δ

Every finite collection of scale inequalities allows the same choices of J and then x₀. Thus the source's different coefficient, neighbor, time, and pressure-cost requirements can be imposed together.

structure EulerPacketSourceScaleChoice.CostSpec : Type

Cost spec data, collecting d, B, N, a, b, c and their compatibility conditions.

• d : ℕ

  D of CostSpec, of type ℕ.

• B : ℕ

  Bound parameter of CostSpec, of type ℕ.

• N : ℕ

  Truncation order of CostSpec, of type ℕ.

• a : ℝ

  A of CostSpec, of type ℝ.

• b : ℝ

  B of CostSpec, of type ℝ.

• c : ℝ

  C of CostSpec, of type ℝ.

• C : ℝ

  Bound coefficient of CostSpec, of type ℝ.

• p : ℕ

  P of CostSpec, of type ℕ.

• q : ℕ

  Q of CostSpec, of type ℕ.

• d_le_two : self.d ≤ 2
• a_nonneg : 0 ≤ self.a
• a_lt_B : self.a < ↑self.B
• a_le_N : self.a ≤ ↑self.N
• b_pos : 0 < self.b
• C_pos : 0 < self.C

noncomputable def EulerPacketSourceScaleChoice.CostSpec.cost (s : CostSpec) (J : ℕ) (x : ℕ → ℝ) : ℕ → ℝ

Cost, given by monomialCost J s.d s.B s.a s.b s.c s.C s.p s.q x.

Equations

• s.cost J x = EulerPacketSourceScaleBounds.monomialCost J s.d s.B s.a s.b s.c s.C s.p s.q x

theorem EulerPacketSourceScaleChoice.finite_uniform_choice {ι : Type u_1} [Finite ι] (s : ι → CostSpec) : ∃ (J : ℕ), 3 ≤ J ∧ ∀ (δ : ℝ), 0 < δ → ∃ (X₀ : ℝ), 8 ≤ X₀ ∧ ∀ (x : ℕ → ℝ), X₀ ≤ x 0 → (∀ (n : ℕ), x (n + 1) = ↑(J + n) ^ 2 * x n) → ∀ (i : ι), Summable ((s i).cost J x) ∧ ∑' (n : ℕ), (s i).cost J x n ≤ δ ∧ ∀ (n : ℕ), (s i).cost J x n ≤ δ

A finite list of literal exponential costs has summable, uniformly small terms and a small total, using one fixed stage and then one base scale.

inductive EulerPacketSourceScaleChoice.SourceCost : Type

Source cost data, collecting elems.

• shear : SourceCost
• prior : SourceCost
• neighbor : SourceCost
• extra : SourceCost
• width : SourceCost
• parent : SourceCost
• good : SourceCost

@[instance_reducible]

instance EulerPacketSourceScaleChoice.instDecidableEqSourceCost : DecidableEq SourceCost

Equations

• EulerPacketSourceScaleChoice.instDecidableEqSourceCost x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance EulerPacketSourceScaleChoice.instFintypeSourceCost : Fintype SourceCost

Equations

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

noncomputable def EulerPacketSourceScaleChoice.sourceCostSpec (C c : ℝ) (hC : 1 ≤ C) (A : ℕ) : SourceCost → CostSpec

Source cost spec used in packet source scale choice.

Equations

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

structure EulerPacketSourceScaleChoice.SmallSeries (f : ℕ → ℝ) (δ : ℝ) : Prop

Small series data, collecting nonneg, summable, total_le.

• nonneg (n : ℕ) : 0 ≤ f n
• summable : Summable f
• total_le : ∑' (n : ℕ), f n ≤ δ

theorem EulerPacketSourceScaleChoice.SmallSeries.term_le {f : ℕ → ℝ} {δ : ℝ} (h : SmallSeries f δ) (n : ℕ) : f n ≤ δ

theorem EulerPacketSourceScaleChoice.SmallSeries.weaken {f : ℕ → ℝ} {δ η : ℝ} (h : SmallSeries f δ) (hle : δ ≤ η) : SmallSeries f η

theorem EulerPacketSourceScaleChoice.SmallSeries.mono {f g : ℕ → ℝ} {δ : ℝ} (h : SmallSeries f δ) (hg : ∀ (n : ℕ), 0 ≤ g n) (hle : ∀ (n : ℕ), g n ≤ f n) : SmallSeries g δ

noncomputable def EulerPacketSourceScaleChoice.coefficientCost (J : ℕ) (C c : ℝ) (A : ℕ) (x : ℕ → ℝ) (n : ℕ) : ℝ

Coefficient cost, given by sourceCoefficientError J C c x n * sourceTheta J C x n^A.

Equations

• EulerPacketSourceScaleChoice.coefficientCost J C c A x n = EulerPacketSourceScales.sourceCoefficientError J C c x n * EulerPacketSourceScales.sourceTheta J C x n ^ A

noncomputable def EulerPacketSourceScaleChoice.extraTimeCost (J : ℕ) (C : ℝ) (A : ℕ) (x a : ℕ → ℝ) (n : ℕ) : ℝ

Extra time cost, given by 2*sqrt (a n*exp (x n/((J-1+n : ℕ) : ℝ)^7))*sourceNextTimeWidth J x n * sourceTheta J C x n^A.

Equations

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

noncomputable def EulerPacketSourceScaleChoice.parentSquareRatio (J : ℕ) (x : ℕ → ℝ) (n : ℕ) : ℝ

Parent square ratio, given by exp (2*x n/((J-1+n : ℕ) : ℝ)^7)/exp (x n/((J+n : ℕ) : ℝ)^5).

Equations

• EulerPacketSourceScaleChoice.parentSquareRatio J x n = Real.exp (2 * x n / ↑(J - 1 + n) ^ 7) / Real.exp (x n / ↑(J + n) ^ 5)

noncomputable def EulerPacketSourceScaleChoice.goodCost (J : ℕ) (x : ℕ → ℝ) (n : ℕ) : ℝ

Good cost, given by exp (-x n/((J+n : ℕ) : ℝ)^3)*exp (x n/((J+n : ℕ) : ℝ)^5) * exp (x n/((J-1+n : ℕ) : ℝ)^7).

Equations

• EulerPacketSourceScaleChoice.goodCost J x n = Real.exp (-x n / ↑(J + n) ^ 3) * Real.exp (x n / ↑(J + n) ^ 5) * Real.exp (x n / ↑(J - 1 + n) ^ 7)

structure EulerPacketSourceScaleChoice.UniformBounds (J : ℕ) (C c : ℝ) (A : ℕ) (x : ℕ → ℝ) (δ : ℝ) : Prop

Uniform bounds data, collecting coefficient, extraTime, width, parent, good.

• coefficient : SmallSeries (coefficientCost J C c A x) δ
• extraTime (a : ℕ → ℝ) : (∀ (n : ℕ), 0 ≤ a n) → (∀ (n : ℕ), a n ≤ 2) → SmallSeries (extraTimeCost J C A x a) δ
• width : SmallSeries (EulerPacketSourceTime.sourceTimeRatio J x) δ
• parent : SmallSeries (parentSquareRatio J x) δ
• good : SmallSeries (goodCost J x) δ

theorem EulerPacketSourceScaleChoice.source_uniform_choice (C c : ℝ) (hC : 1 ≤ C) (hc : 0 ≤ c) (A : ℕ) : ∃ (J : ℕ), 3 ≤ J ∧ ∀ (δ : ℝ), 0 < δ → ∃ (X₀ : ℝ), 8 ≤ X₀ ∧ ∀ (x : ℕ → ℝ), X₀ ≤ x 0 → (∀ (n : ℕ), x (n + 1) = ↑(J + n) ^ 2 * x n) → UniformBounds J C c A x δ

One fixed choice of the starting stage makes all the actual normal-stage coefficient, time, shear-separation and good-interval pressure series small. The initial scale is chosen afterwards, and every later stage is covered.

def EulerPacketSourceScaleChoice.scaleSequence (J : ℕ) (X : ℝ) : ℕ → ℝ

The sequence in (37), now constructed rather than supplied.

Equations

• EulerPacketSourceScaleChoice.scaleSequence J X 0 = X
• EulerPacketSourceScaleChoice.scaleSequence J X n.succ = ↑(J + n) ^ 2 * EulerPacketSourceScaleChoice.scaleSequence J X n

@[simp]

theorem EulerPacketSourceScaleChoice.scaleSequence_zero (J : ℕ) (X : ℝ) : scaleSequence J X 0 = X

theorem EulerPacketSourceScaleChoice.scaleSequence_succ (J : ℕ) (X : ℝ) (n : ℕ) : scaleSequence J X (n + 1) = ↑(J + n) ^ 2 * scaleSequence J X n

theorem EulerPacketSourceScaleChoice.explicit_sequence_uniform_choice (C c : ℝ) (hC : 1 ≤ C) (hc : 0 ≤ c) (A : ℕ) : ∃ (J : ℕ), 3 ≤ J ∧ ∀ (δ : ℝ), 0 < δ → ∃ (X₀ : ℝ), 8 ≤ X₀ ∧ ∀ (X : ℝ), X₀ ≤ X → UniformBounds J C c A (scaleSequence J X) δ

In particular the explicit sequence allows the same simultaneous choice; no recurrence or asymptotic conclusion remains as an input.

noncomputable def EulerPacketSourceScaleSequence.shear (J : ℕ) (X : ℝ) (n : ℕ) : ℝ

Shear, given by exp (scaleSequence J X n/((J+n : ℕ) : ℝ)^5).

Equations

• EulerPacketSourceScaleSequence.shear J X n = Real.exp (EulerPacketSourceScaleChoice.scaleSequence J X n / ↑(J + n) ^ 5)

noncomputable def EulerPacketSourceScaleSequence.frequency (J : ℕ) (X : ℝ) (n : ℕ) : ℝ

Frequency, given by exp (scaleSequence J X n/((J+n : ℕ) : ℝ)^2).

Equations

• EulerPacketSourceScaleSequence.frequency J X n = Real.exp (EulerPacketSourceScaleChoice.scaleSequence J X n / ↑(J + n) ^ 2)

noncomputable def EulerPacketSourceScaleSequence.spike (J : ℕ) (X : ℝ) (n : ℕ) : ℝ

Spike, given by exp (-scaleSequence J X n/((J+n : ℕ) : ℝ)^3).

Equations

• EulerPacketSourceScaleSequence.spike J X n = Real.exp (-EulerPacketSourceScaleChoice.scaleSequence J X n / ↑(J + n) ^ 3)

noncomputable def EulerPacketSourceScaleSequence.supportScale (J : ℕ) (X : ℝ) (n : ℕ) : ℝ

Support scale, given by exp (-scaleSequence J X n/((J+n : ℕ) : ℝ)^(7/2 : ℝ)).

Equations

• EulerPacketSourceScaleSequence.supportScale J X n = Real.exp (-EulerPacketSourceScaleChoice.scaleSequence J X n / ↑(J + n) ^ (7 / 2))

noncomputable def EulerPacketSourceScaleSequence.previousShear (J : ℕ) (X : ℝ) : ℕ → ℝ

Previous shear as an element of ℕ → ℝ | 0 => X^1000 | n+1 => shear J X n.

Equations

• EulerPacketSourceScaleSequence.previousShear J X 0 = X ^ 1000
• EulerPacketSourceScaleSequence.previousShear J X n.succ = EulerPacketSourceScaleSequence.shear J X n

noncomputable def EulerPacketSourceScaleSequence.previousFrequency (J D : ℕ) (X : ℝ) : ℕ → ℝ

Previous frequency as an element of ℕ → ℝ | 0 => X^D | n+1 => frequency J X n.

Equations

• EulerPacketSourceScaleSequence.previousFrequency J D X 0 = X ^ D
• EulerPacketSourceScaleSequence.previousFrequency J D X n.succ = EulerPacketSourceScaleSequence.frequency J X n

noncomputable def EulerPacketSourceScaleSequence.olderShear (J : ℕ) (X : ℝ) : ℕ → ℝ

Older shear as an element of ℕ → ℝ | 0 => 1 | n+1 => previousShear J X n.

Equations

• EulerPacketSourceScaleSequence.olderShear J X 0 = 1
• EulerPacketSourceScaleSequence.olderShear J X n.succ = EulerPacketSourceScaleSequence.previousShear J X n

noncomputable def EulerPacketSourceScaleSequence.timeWidth (J : ℕ) (X : ℝ) (n : ℕ) : ℝ

Time width, given by 3*scaleSequence J X (n+1)*scaleSequence J X n/sqrt (previousShear J X n).

Equations

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

theorem EulerPacketSourceScaleSequence.previousShear_pos (J : ℕ) {X : ℝ} (hX : 0 < X) (n : ℕ) : 0 < previousShear J X n

theorem EulerPacketSourceScaleSequence.previousFrequency_pos (J D : ℕ) {X : ℝ} (hX : 0 < X) (n : ℕ) : 0 < previousFrequency J D X n

theorem EulerPacketSourceScaleSequence.previousShear_succ_eq (J : ℕ) (hJ : 1 ≤ J) (X : ℝ) (n : ℕ) : previousShear J X (n + 1) = Real.exp (EulerPacketSourceScaleChoice.scaleSequence J X (n + 1) / ↑(J - 1 + (n + 1)) ^ 7)

theorem EulerPacketSourceScaleSequence.previousFrequency_succ_eq (J D : ℕ) (hJ : 1 ≤ J) (X : ℝ) (n : ℕ) : previousFrequency J D X (n + 1) = Real.exp (EulerPacketSourceScaleChoice.scaleSequence J X (n + 1) / ↑(J - 1 + (n + 1)) ^ 4)

theorem EulerPacketSourceScaleSequence.olderShear_succ_succ_eq (J : ℕ) (hJ : 2 ≤ J) (X : ℝ) (n : ℕ) : olderShear J X (n + 1 + 1) = Real.exp (EulerPacketSourceScaleChoice.scaleSequence J X (n + 1 + 1) / (↑(J - 1 + (n + 1 + 1)) ^ 2 * ↑(J - 2 + (n + 1 + 1)) ^ 7))

theorem EulerPacketSourceScaleSequence.eventually_pow_le_exp (D : ℕ) {r : ℝ} (hr : 0 < r) : ∀ᶠ (X : ℝ) in Filter.atTop, X ^ D ≤ Real.exp (X / r)

A fixed positive linear exponential eventually dominates each actual polynomial base shear or frequency.

theorem EulerPacketSourceScaleSequence.previousShear_le_normal (J : ℕ) (hJ : 1 ≤ J) (X : ℝ) (hbase : X ^ 1000 ≤ Real.exp (X / ↑(J - 1) ^ 7)) (n : ℕ) : previousShear J X n ≤ Real.exp (EulerPacketSourceScaleChoice.scaleSequence J X n / ↑(J - 1 + n) ^ 7)

theorem EulerPacketSourceScaleSequence.previousFrequency_le_normal (J D : ℕ) (hJ : 1 ≤ J) (X : ℝ) (hbase : X ^ D ≤ Real.exp (X / ↑(J - 1) ^ 4)) (n : ℕ) : previousFrequency J D X n ≤ Real.exp (EulerPacketSourceScaleChoice.scaleSequence J X n / ↑(J - 1 + n) ^ 4)

theorem EulerPacketSourceScaleSequence.olderShear_le_normal (J : ℕ) (hJ : 3 ≤ J) (X : ℝ) (hX : 0 ≤ X) (hbase : X ^ 1000 ≤ Real.exp (X / ↑(J - 1) ^ 7)) (n : ℕ) : 1 + olderShear J X n ≤ EulerPacketSourceScales.sourceOlderGradient J (EulerPacketSourceScaleChoice.scaleSequence J X) n

theorem EulerPacketSourceScaleSequence.timeWidth_pos (J : ℕ) (hJ : 1 ≤ J) {X : ℝ} (hX : 0 < X) (n : ℕ) : 0 < timeWidth J X n

theorem EulerPacketSourceScaleSequence.timeWidth_succ_eq (J : ℕ) (X : ℝ) (n : ℕ) : timeWidth J X (n + 1) = EulerPacketSourceTime.sourceNextTimeWidth J (EulerPacketSourceScaleChoice.scaleSequence J X) n

theorem EulerPacketSourceScaleSequence.sourceTimeWidth_eq (J : ℕ) (X : ℝ) (n : ℕ) : EulerPacketSourceTime.sourceTimeWidth J (EulerPacketSourceScaleChoice.scaleSequence J X) n = 3 * EulerPacketSourceScaleChoice.scaleSequence J X (n + 1) * EulerPacketSourceScaleChoice.scaleSequence J X n / √(Real.exp (EulerPacketSourceScaleChoice.scaleSequence J X n / ↑(J - 1 + n) ^ 7))

theorem EulerPacketSourceScaleSequence.sourceTimeWidth_le (J : ℕ) (hJ : 1 ≤ J) (X : ℝ) (hX : 0 < X) (hbase : X ^ 1000 ≤ Real.exp (X / ↑(J - 1) ^ 7)) (n : ℕ) : EulerPacketSourceTime.sourceTimeWidth J (EulerPacketSourceScaleChoice.scaleSequence J X) n ≤ timeWidth J X n

The actual polynomial-base time width is no smaller than the normal-form one, once the explicit polynomial/exponential comparison holds.