The geometry error for the literal scale sequences, including the initial polynomial shear and frequency. Comparison with the normal-form costs is proved here, rather than imposed at the two exceptional starting stages.

noncomputable def EulerPacketSourceScaleActual.epsilon (J : ℕ) (X a : ℝ) (n : ℕ) : ℝ

Epsilon, given by sqrt (a/previousShear J X n).

Equations

• EulerPacketSourceScaleActual.epsilon J X a n = √(a / EulerPacketSourceScaleSequence.previousShear J X n)

noncomputable def EulerPacketSourceScaleActual.priorError (J D : ℕ) (X : ℝ) (n : ℕ) : ℝ

Prior error, given by previousFrequency J D X n ^ (-(1/4 : ℝ)).

Equations

• EulerPacketSourceScaleActual.priorError J D X n = EulerPacketSourceScaleSequence.previousFrequency J D X n ^ (-(1 / 4))

noncomputable def EulerPacketSourceScaleActual.neighborError (J D : ℕ) (X c : ℝ) (n : ℕ) : ℝ

Neighbor error, given by supportScale J X n * previousFrequency J D X n^c * previousShear J X n^c.

Equations

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

noncomputable def EulerPacketSourceScaleActual.geometryError (J D : ℕ) (C c X : ℝ) (a : ℕ → ℝ) (n : ℕ) : ℝ

Geometry error as an element of ℝ.

Equations

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

noncomputable def EulerPacketSourceScaleActual.baseErrorCost (J D : ℕ) (C X : ℝ) : ℝ

Base error cost, given by 16*(128*X^(-500 : ℝ)*sourceTheta J C (scaleSequence J X) 0+X^(-(D:ℝ)/4)) * sourceTheta J C (scaleSequence J X) 0^60.

Equations

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

noncomputable def EulerPacketSourceScaleActual.geometryErrorCost (J D : ℕ) (C c X : ℝ) (a : ℕ → ℝ) (n : ℕ) : ℝ

Geometry error cost, given by geometryError J D C c X a n * sourceTheta J C (scaleSequence J X) n^60.

Equations

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

theorem EulerPacketSourceScaleActual.epsilon_succ_le (J : ℕ) (hJ : 1 ≤ J) (X a : ℝ) (ha : 0 ≤ a) (ha₂ : a ≤ 2) (n : ℕ) : epsilon J X a (n + 1) ≤ EulerPacketSourceScales.sourceEpsilon J (EulerPacketSourceScaleChoice.scaleSequence J X) (n + 1)

theorem EulerPacketSourceScaleActual.epsilon_zero_le (J : ℕ) {X a : ℝ} (hX : 0 < X) (ha : 0 ≤ a) (ha₂ : a ≤ 2) : epsilon J X a 0 ≤ 2 * X ^ (-500)

theorem EulerPacketSourceScaleActual.priorError_succ_eq (J D : ℕ) (hJ : 1 ≤ J) (X : ℝ) (n : ℕ) : priorError J D X (n + 1) = EulerPacketSourceScales.sourcePriorError J (EulerPacketSourceScaleChoice.scaleSequence J X) (n + 1)

theorem EulerPacketSourceScaleActual.priorError_zero_eq (J D : ℕ) {X : ℝ} (hX : 0 < X) : priorError J D X 0 = X ^ (-↑D / 4)

theorem EulerPacketSourceScaleActual.neighborError_le (J D : ℕ) (hJ : 1 ≤ J) (X c : ℝ) (hX : 0 < X) (hc : 0 ≤ c) (hbaseH : X ^ 1000 ≤ Real.exp (X / ↑(J - 1) ^ 7)) (hbaseK : X ^ D ≤ Real.exp (X / ↑(J - 1) ^ 4)) (n : ℕ) : neighborError J D X c n ≤ EulerPacketSourceScales.sourceNeighborError J c (EulerPacketSourceScaleChoice.scaleSequence J X) n

theorem EulerPacketSourceScaleActual.geometryError_nonneg (J D : ℕ) (C c X : ℝ) (a : ℕ → ℝ) (n : ℕ) (hC : 0 ≤ C) (hX : 0 < X) : 0 ≤ geometryError J D C c X a n

theorem EulerPacketSourceScaleActual.geometryError_succ_le (J D : ℕ) (hJ : 3 ≤ J) (C c X : ℝ) (hC : 1 ≤ C) (hX : 1 ≤ X) (hc : 0 ≤ c) (a : ℕ → ℝ) (ha : ∀ (n : ℕ), 0 ≤ a n) (ha₂ : ∀ (n : ℕ), a n ≤ 2) (hbaseH : X ^ 1000 ≤ Real.exp (X / ↑(J - 1) ^ 7)) (hbaseK : X ^ D ≤ Real.exp (X / ↑(J - 1) ^ 4)) (n : ℕ) : geometryError J D C c X a (n + 1) ≤ 16 * EulerPacketSourceScales.sourceCoefficientError J C c (EulerPacketSourceScaleChoice.scaleSequence J X) (n + 1)

theorem EulerPacketSourceScaleActual.geometryError_zero_le (J D : ℕ) (hJ : 3 ≤ J) (C c X : ℝ) (hC : 1 ≤ C) (hX : 1 ≤ X) (hc : 0 ≤ c) (a : ℕ → ℝ) (ha : 0 ≤ a 0) (ha₂ : a 0 ≤ 2) (hbaseH : X ^ 1000 ≤ Real.exp (X / ↑(J - 1) ^ 7)) (hbaseK : X ^ D ≤ Real.exp (X / ↑(J - 1) ^ 4)) : geometryError J D C c X a 0 ≤ 16 * (128 * X ^ (-500) * EulerPacketSourceScales.sourceTheta J C (EulerPacketSourceScaleChoice.scaleSequence J X) 0 + X ^ (-↑D / 4)) + EulerPacketSourceScales.sourceCoefficientError J C c (EulerPacketSourceScaleChoice.scaleSequence J X) 0

theorem EulerPacketSourceScaleActual.geometryErrorCost_bound (J D : ℕ) (hJ : 3 ≤ J) (C c X : ℝ) (hC : 1 ≤ C) (hX : 1 ≤ X) (hc : 0 ≤ c) (a : ℕ → ℝ) (ha : ∀ (n : ℕ), 0 ≤ a n) (ha₂ : ∀ (n : ℕ), a n ≤ 2) (hbaseH : X ^ 1000 ≤ Real.exp (X / ↑(J - 1) ^ 7)) (hbaseK : X ^ D ≤ Real.exp (X / ↑(J - 1) ^ 4)) (n : ℕ) : geometryErrorCost J D C c X a n ≤ 16 * EulerPacketSourceScaleChoice.coefficientCost J C c 60 (EulerPacketSourceScaleChoice.scaleSequence J X) n + if n = 0 then baseErrorCost J D C X else 0

theorem EulerPacketSourceScaleActual.baseErrorCost_nonneg (J D : ℕ) (C X : ℝ) (hC : 0 ≤ C) (hX : 0 ≤ X) : 0 ≤ baseErrorCost J D C X

theorem EulerPacketSourceScaleActual.baseErrorCost_tendsto_zero (J D : ℕ) (hJ : 1 ≤ J) (hD : 1000 ≤ D) (C : ℝ) (hC : 1 ≤ C) : Filter.Tendsto (baseErrorCost J D C) Filter.atTop (nhds 0)

The two genuinely exceptional polynomial terms are small with the specified D₀=1000 and any base frequency power D≥1000.

structure EulerPacketSourceScaleActual.ActualBounds (J D : ℕ) (C c X δ : ℝ) : Prop

Actual bounds data, collecting normal, initial_shear, initial_frequency, coefficient.

• normal : EulerPacketSourceScaleChoice.UniformBounds J C c 60 (EulerPacketSourceScaleChoice.scaleSequence J X) δ
• initial_shear : X ^ 1000 ≤ Real.exp (X / ↑(J - 1) ^ 7)
• initial_frequency : X ^ D ≤ Real.exp (X / ↑(J - 1) ^ 4)
• coefficient (a : ℕ → ℝ) : (∀ (n : ℕ), 0 ≤ a n) → (∀ (n : ℕ), a n ≤ 2) → EulerPacketSourceScaleChoice.SmallSeries (geometryErrorCost J D C c X a) δ

theorem EulerPacketSourceScaleActual.actual_uniform_choice (D : ℕ) (hD : 1000 ≤ D) (C c : ℝ) (hC : 1 ≤ C) (hc : 0 ≤ c) : ∃ (J : ℕ), 3 ≤ J ∧ ∀ (δ : ℝ), 0 < δ → ∃ (X₀ : ℝ), 8 ≤ X₀ ∧ ∀ (X : ℝ), X₀ ≤ X → ActualBounds J D C c X δ

The actual sequence, with both polynomial starting scales, has one choice of J followed by x₀ making every geometry error uniformly and summably small. This is uniform over the allowed frame coefficient a.